mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 18:31:49 +00:00
Code Activity

fix(spacer): bug in assign_bounds to Farkas conversion

Browse source 
The fix is to remove a hack that used a theory rewriter to simplify
the conversion. Now the conversion happens less often than possible.
Will need more thinking to fix properly.

The unsoundness at this point would cause SPACER to generate lemmas
that do not block a proof obligation and then get stuck in an infinite loop
blocking and generating the same lemma.
This commit is contained in:
Arie Gurfinkel 2020-06-18 21:17:45 -04:00
parent 38d4418f94
commit 07a1aea689
1 changed files with 8 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

9
src/muz/spacer/spacer_proof_utils.cpp
View file

@ -293,13 +293,17 @@ namespace spacer {
for (unsigned i = 1, sz = parents.size(); i < sz; ++i) {
app *p = to_app(m.get_fact(parents.get(i)));
rational const &r = params[i+1].get_rational();
TRACE("spacer.fkab", tout << "Adding to LCB: " << mk_pp(p, m) << "\n";);
lcb.add_lit(p, r);
}
expr_ref lit0(m);
lit0 = m.get_fact(parents.get(0));
// put lit0 into canonical form
rw(lit0);
// XXX this might simplify a coefficient of a variable leading to unsoundness.
// XXX For example, it will simplify 4*x >= 0 into x >= 0
//rw(lit0);
TRACE("spacer.fkab",
tout << "lit0 is: " << lit0 << "\n"
<< "LCB is: " << lcb() << "\n";);
@ -345,11 +349,13 @@ namespace spacer {
v.size(), v.c_ptr());
SASSERT(is_arith_lemma(m, pf));
TRACE("spacer.fkab", tout << mk_pp(pf, m) << "\n";);
DEBUG_CODE(
proof_checker pc(m);
expr_ref_vector side(m);
ENSURE(pc.check(pf, side)););
return pf;
}
@ -396,6 +402,7 @@ namespace spacer {
func_decl *d = p->get_decl();
if (is_assign_bounds_lemma(m, p)) {
TRACE("spacer.fkab", tout << mk_pp(p, m) << "\n";);
th_lemma = mk_fk_from_ab(m, hyps,
d->get_num_parameters(),
d->get_parameters());