summaryrefslogtreecommitdiffstats
path: root/src/sat/bsat/satSolver.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/sat/bsat/satSolver.h')
-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;
}