mirror of
https://github.com/Z3Prover/z3
synced 2025-04-13 12:28:44 +00:00
parent
3bd340af44
commit
0b856638e9
|
@ -754,10 +754,12 @@ namespace sat {
|
|||
}
|
||||
add_unit(~lit, null_literal);
|
||||
if (!propagate(~lit)) {
|
||||
IF_VERBOSE(0, verbose_stream() << "unsat\n");
|
||||
IF_VERBOSE(2, verbose_stream() << "unsat\n");
|
||||
m_is_unsat = true;
|
||||
return;
|
||||
}
|
||||
if (m_unsat_stack.empty())
|
||||
return;
|
||||
goto reflip;
|
||||
}
|
||||
|
||||
|
|
Loading…
Reference in a new issue