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

fix issues reported in #4525

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-06-21 17:43:05 -07:00
parent 02f34ea4b1
commit 6a54c0bc04
2 changed files with 12 additions and 5 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

8
src/qe/qe_arith.cpp
View file

@ -209,7 +209,9 @@ namespace qe {
else if (a.is_mod(t, t1, t2) && is_numeral(t2, mul1) && !mul1.is_zero()) {
rational r;
val = eval(t);
VERIFY(a.is_numeral(val, r));
if (!a.is_numeral(val, r)) {
throw default_exception("mbp evaluation didn't produce an integer");
}
c += mul*r;
// t1 mod mul1 == r
rational c0(-r), mul0(1);
@ -347,8 +349,8 @@ namespace qe {
expr_ref val = eval(v);
if (!m.inc())
return vector<def>();
VERIFY(a.is_numeral(val, r));
if (!a.is_numeral(val, r))
throw default_exception("evaluation did not produce a numeral");
TRACE("qe", tout << mk_pp(v, m) << " " << val << "\n";);
tids.insert(v, mbo.add_var(r, a.is_int(v)));
}

9
src/qe/qe_lite.cpp
View file

@ -2238,11 +2238,16 @@ class qe_lite::impl {
if (is_forall(q)) {
result = push_not(result);
}
result = m.update_quantifier(
expr_ref tmp(m);
tmp = m.update_quantifier(
q,
q->get_num_patterns(), new_patterns,
q->get_num_no_patterns(), new_no_patterns, result);
m_imp.m_rewriter(result, result, result_pr);
m_imp.m_rewriter(tmp, result, result_pr);
if (m.proofs_enabled()) {
result_pr = m.mk_transitivity(m.mk_rewrite(q, tmp), result_pr);
}
return true;
}
};