mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

remove extra assume-eqs

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-10-15 12:30:24 -07:00
parent b2efa592ce
commit 6553382ec8
1 changed files with 3 additions and 7 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/smt/theory_lra.cpp
View file

@ -1635,7 +1635,7 @@ public:
switch (is_sat) { switch (is_sat) {
case l_true: case l_true:
TRACE("arith", display(tout)); TRACE("arith", display(tout));
switch (check_lia()) { switch (check_lia()) {
case FC_DONE: case FC_DONE:
break; break;
@ -1647,7 +1647,6 @@ public:
st = FC_CONTINUE; st = FC_CONTINUE;
break; break;
} }
switch (check_nla()) { switch (check_nla()) {
case FC_DONE: case FC_DONE:
@ -1658,7 +1657,7 @@ public:
TRACE("arith", tout << "check-nra giveup\n";); TRACE("arith", tout << "check-nra giveup\n";);
st = FC_GIVEUP; st = FC_GIVEUP;
break; break;
} }
if (assume_eqs()) { if (assume_eqs()) {
++m_stats.m_assume_eqs; ++m_stats.m_assume_eqs;
@ -1970,9 +1969,6 @@ public:
} }
if (!check_idiv_bounds()) if (!check_idiv_bounds())
return FC_CONTINUE; return FC_CONTINUE;
if (assume_eqs())
return FC_CONTINUE;
return FC_DONE; return FC_DONE;
} }
@ -2027,7 +2023,7 @@ public:
add_lemmas(); add_lemmas();
return FC_CONTINUE; return FC_CONTINUE;
case l_true: case l_true:
return assume_eqs()? FC_CONTINUE: FC_DONE; return FC_DONE;
default: default:
return FC_GIVEUP; return FC_GIVEUP;
} }