mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-07 09:55:19 +00:00
Code Activity

fix #6996

Browse source
This commit is contained in:
Nikolaj Bjorner 2023-11-16 18:58:12 -08:00
parent 36382ccb57
commit 1b6c7d6541
1 changed files with 8 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -277,8 +277,14 @@ namespace mbp {
extract_coefficients(mbo, eval, ts0, tids, coeffs); extract_coefficients(mbo, eval, ts0, tids, coeffs);
mbo.add_divides(coeffs, c0, mul1); mbo.add_divides(coeffs, c0, mul1);
} }
else else if (a.is_to_real(t))
throw default_exception("mbp to-real");
else if (a.is_to_int(t))
throw default_exception("mbp to-int");
else {
TRACE("qe", tout << "insert mul " << mk_pp(t, m) << "\n");
insert_mul(t, mul, ts); insert_mul(t, mul, ts);
}
} }
bool is_numeral(expr* t, rational& r) { bool is_numeral(expr* t, rational& r) {
@ -387,8 +393,7 @@ namespace mbp {
return false; return false;
}; };
for (auto& kv : tids) { for (auto& [e, v] : tids) {
expr* e = kv.m_key;
if (is_arith(e) && !is_pure(e) && !var_mark.is_marked(e)) if (is_arith(e) && !is_pure(e) && !var_mark.is_marked(e))
mark_rec(fmls_mark, e); mark_rec(fmls_mark, e);
} }