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 #3040: soudness bug in dom-simplify

Browse source
This commit is contained in:
Nuno Lopes 2020-02-19 13:02:45 +00:00
parent 006caea5ba
commit 1ac365ca74
1 changed files with 4 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

10
src/tactic/core/dom_simplify_tactic.cpp
View file

@ -524,19 +524,17 @@ public:
bool assert_expr(expr * t, bool sign) override { bool assert_expr(expr * t, bool sign) override {
expr* tt; expr* tt;
if (m.is_false(t) || (m.is_not(t, tt) && m.is_true(tt))) if (m.is_not(t, tt))
return assert_expr(tt, !sign);
if (m.is_false(t))
return sign; return sign;
if (m.is_true(t))
if (m.is_true(t) || (m.is_not(t, tt) && m.is_false(tt)))
return !sign; return !sign;
m_scoped_substitution.push(); m_scoped_substitution.push();
if (!sign) { if (!sign) {
update_substitution(t, nullptr); update_substitution(t, nullptr);
} }
else if (m.is_not(t, tt)) {
update_substitution(tt, nullptr);
}
else { else {
expr_ref nt(m.mk_not(t), m); expr_ref nt(m.mk_not(t), m);
update_substitution(nt, nullptr); update_substitution(nt, nullptr);