mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
Sat update
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
parent
d3b30968fa
commit
2c208e1d10
|
@ -3291,6 +3291,9 @@ namespace sat {
|
||||||
literal lit = *it;
|
literal lit = *it;
|
||||||
if (value(lit) != l_undef) {
|
if (value(lit) != l_undef) {
|
||||||
++num_fixed;
|
++num_fixed;
|
||||||
|
if (value(lit) == l_true && lvl(lit) == 1) {
|
||||||
|
VERIFY(extract_fixed_consequences(lit, assumptions, unfixed_vars, conseq));
|
||||||
|
}
|
||||||
continue;
|
continue;
|
||||||
}
|
}
|
||||||
push();
|
push();
|
||||||
|
|
Loading…
Reference in a new issue