mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-15 10:26:16 +00:00
Code Activity

fix #3409 - force model completion so that variables simplified away during pre-rpocessing are evaluated nevertheless

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2020-03-19 11:17:59 -07:00
parent 65e1d08457
commit 2ad1cc95c1
1 changed files with 3 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

6
src/qe/qe_arith.cpp
View file

@ -67,7 +67,7 @@ namespace qe {
CTRACE("qe", !m.is_true(val), tout << mk_pp(lit, m) << " := " << val << "\n";); CTRACE("qe", !m.is_true(val), tout << mk_pp(lit, m) << " := " << val << "\n";);
SASSERT(m.canceled() || m.is_true(val));); SASSERT(m.canceled() || m.is_true(val)););
if (!m.inc()) if (!m.limit().inc())
return false; return false;
TRACE("opt", tout << mk_pp(lit, m) << " " << a.is_lt(lit) << " " << a.is_gt(lit) << "\n";); TRACE("opt", tout << mk_pp(lit, m) << " " << a.is_lt(lit) << " " << a.is_gt(lit) << "\n";);
@ -311,7 +311,7 @@ namespace qe {
} }
model_evaluator eval(model); model_evaluator eval(model);
TRACE("qe", tout << model;); TRACE("qe", tout << model;);
// eval.set_model_completion(true); eval.set_model_completion(true);
opt::model_based_opt mbo; opt::model_based_opt mbo;
obj_map<expr, unsigned> tids; obj_map<expr, unsigned> tids;
@ -564,7 +564,7 @@ namespace qe {
if (!tids.find(v, id)) { if (!tids.find(v, id)) {
rational r; rational r;
expr_ref val = eval(v); expr_ref val = eval(v);
a.is_numeral(val, r); VERIFY(a.is_numeral(val, r));
id = mbo.add_var(r, a.is_int(v)); id = mbo.add_var(r, a.is_int(v));
tids.insert(v, id); tids.insert(v, id);
} }