From 1ac365ca7429421b4318576d18ccd6a8c5aaa20a Mon Sep 17 00:00:00 2001
From: Nuno Lopes <nlopes@microsoft.com>
Date: Wed, 19 Feb 2020 13:02:45 +0000
Subject: [PATCH] fix #3040: soudness bug in dom-simplify
---
src/tactic/core/dom_simplify_tactic.cpp | 10 ++++------
1 file changed, 4 insertions(+), 6 deletions(-)
diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp
index 5b602148c..cdf910bc3 100644
--- a/src/tactic/core/dom_simplify_tactic.cpp
+++ b/src/tactic/core/dom_simplify_tactic.cpp
@@ -524,19 +524,17 @@ public:
bool assert_expr(expr * t, bool sign) override {
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;
-
- if (m.is_true(t) || (m.is_not(t, tt) && m.is_false(tt)))
+ if (m.is_true(t))
return !sign;
m_scoped_substitution.push();
if (!sign) {
update_substitution(t, nullptr);
}
- else if (m.is_not(t, tt)) {
- update_substitution(tt, nullptr);
- }
else {
expr_ref nt(m.mk_not(t), m);
update_substitution(nt, nullptr);