summaryrefslogtreecommitdiffstats
diff options
context:
space:
mode:
authorAlan Mishchenko <alanmi@berkeley.edu>2015-05-04 17:42:19 -0700
committerAlan Mishchenko <alanmi@berkeley.edu>2015-05-04 17:42:19 -0700
commit3e1c831b2d58329153e2decacf50dd5be9309858 (patch)
treef59291467f6b4d65b103d93208f1752a89318a46
parenta90700c7537e85fd5178a5f41d82cbad35234fcf (diff)
downloadabc-3e1c831b2d58329153e2decacf50dd5be9309858.tar.gz
abc-3e1c831b2d58329153e2decacf50dd5be9309858.tar.bz2
abc-3e1c831b2d58329153e2decacf50dd5be9309858.zip
Bug fix in QBF solver.
-rw-r--r--src/sat/bsat/satSolver.h4
1 files changed, 4 insertions, 0 deletions
diff --git a/src/sat/bsat/satSolver.h b/src/sat/bsat/satSolver.h
index ebc555d9..d328e6d5 100644
--- a/src/sat/bsat/satSolver.h
+++ b/src/sat/bsat/satSolver.h
@@ -294,11 +294,15 @@ static inline int sat_solver_add_buffer( sat_solver * pSat, int iVarA, int iVarB
Lits[0] = toLitCond( iVarA, 0 );
Lits[1] = toLitCond( iVarB, !fCompl );
Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
+ if ( Cid == 0 )
+ return 0;
assert( Cid );
Lits[0] = toLitCond( iVarA, 1 );
Lits[1] = toLitCond( iVarB, fCompl );
Cid = sat_solver_addclause( pSat, Lits, Lits + 2 );
+ if ( Cid == 0 )
+ return 0;
assert( Cid );
return 2;
}