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

reduce-args: fix unsoundness 2: f(v + 2), where b is quantified

Browse source
This commit is contained in:
Nuno Lopes 2016-03-17 13:27:07 +00:00
parent aed4619066
commit facb421398
1 changed files with 3 additions and 3 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/tactic/core/reduce_args_tactic.cpp
View file

@ -96,10 +96,10 @@ struct reduce_args_tactic::imp {
expr *lhs, *rhs; expr *lhs, *rhs;
if (bv.is_bv_add(e, lhs, rhs) && bv.is_numeral(lhs)) { if (bv.is_bv_add(e, lhs, rhs) && bv.is_numeral(lhs)) {
base = rhs; base = rhs;
return true; } else {
base = e;
} }
base = e; return !is_var(base);
return !is_var(e);
} }
static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) { static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) {