mirror of
https://github.com/Z3Prover/z3
synced 2025-04-16 13:58:45 +00:00
n/a
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
a1e4fc3e98
commit
7db1132c33
|
@ -1987,9 +1987,9 @@ namespace sat {
|
|||
void lookahead::propagate_binary(literal l) {
|
||||
literal_vector const& lits = m_binary[l.index()];
|
||||
TRACE("sat", tout << l << " => " << lits << "\n";);
|
||||
unsigned sz = lits.size();
|
||||
for (unsigned i = 0; !inconsistent() && i < sz; ++i) {
|
||||
assign(lits[i]);
|
||||
for (literal l : lits) {
|
||||
if (inconsistent()) break;
|
||||
assign(l);
|
||||
}
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue