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

fix #7517

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-01-20 19:04:36 -08:00
parent fb5834268e
commit a3f7541719
1 changed files with 0 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -39,7 +39,6 @@ namespace mbp {
bool m_check_purified = true; // check that variables are properly pure bool m_check_purified = true; // check that variables are properly pure
bool m_apply_projection = false; bool m_apply_projection = false;
imp(ast_manager& m) : imp(ast_manager& m) :
m(m), a(m) {} m(m), a(m) {}
@ -275,10 +274,6 @@ 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 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 { else {
TRACE("qe", tout << "insert mul " << mk_pp(t, m) << "\n"); TRACE("qe", tout << "insert mul " << mk_pp(t, m) << "\n");
insert_mul(t, mul, ts); insert_mul(t, mul, ts);