mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-04 13:21:22 +00:00
Code Activity

fix #5262

Browse source
This commit is contained in:
Nikolaj Bjorner 2021-05-17 15:51:03 -07:00
parent 8384f38eb5
commit 55f8ad068f
1 changed files with 4 additions and 2 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/qe/mbp/mbp_arith.cpp
View file

@ -194,17 +194,19 @@ namespace mbp {
else if (m.is_ite(t, t1, t2, t3)) { else if (m.is_ite(t, t1, t2, t3)) {
val = eval(t1); val = eval(t1);
SASSERT(m.is_true(val) || m.is_false(val));
TRACE("qe", tout << mk_pp(t1, m) << " := " << val << "\n";); TRACE("qe", tout << mk_pp(t1, m) << " := " << val << "\n";);
if (m.is_true(val)) { if (m.is_true(val)) {
linearize(mbo, eval, mul, t2, c, fmls, ts, tids); linearize(mbo, eval, mul, t2, c, fmls, ts, tids);
fmls.push_back(t1); fmls.push_back(t1);
} }
else { else if (m.is_false(val)) {
expr_ref not_t1(mk_not(m, t1), m); expr_ref not_t1(mk_not(m, t1), m);
fmls.push_back(not_t1); fmls.push_back(not_t1);
linearize(mbo, eval, mul, t3, c, fmls, ts, tids); linearize(mbo, eval, mul, t3, c, fmls, ts, tids);
} }
else {
throw default_exception("mbp evaluation didn't produce a truth value");
}
} }
else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && !mul1.is_zero()) { else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && !mul1.is_zero()) {
rational r; rational r;