mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-06-06 22:23:22 +00:00
Code Activity

minor code simplification

Browse source
This commit is contained in:
Nuno Lopes 2020-02-06 09:01:16 +00:00
parent 459df32211
commit 8279b406ab
1 changed files with 5 additions and 5 deletions
Download patch file Download diff file Expand all files Collapse all files

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

@ -518,11 +518,11 @@ public:
bool assert_expr(expr * t, bool sign) override { bool assert_expr(expr * t, bool sign) override {
expr* tt; expr* tt;
if ((!sign && m.is_false(t)) || if (m.is_false(t) || (m.is_not(t, tt) && m.is_true(tt)))
(sign && m.is_true(t)) || return sign;
(!sign && m.is_not(t, tt) && m.is_true(tt)) ||
(sign && m.is_not(t, tt) && m.is_false(tt))) if (m.is_true(t) || (m.is_not(t, tt) && m.is_false(tt)))
return false; return !sign;
m_scoped_substitution.push(); m_scoped_substitution.push();
if (!sign) { if (!sign) {