Commit 3e1c831b by Alan Mishchenko

Bug fix in QBF solver.

parent a90700c7
......@@ -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;
}
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment