From 8279b406abb2e51c94c7ea89f0d84d019ece162b Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 6 Feb 2020 09:01:16 +0000 Subject: [PATCH] minor code simplification --- src/tactic/core/dom_simplify_tactic.cpp | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/src/tactic/core/dom_simplify_tactic.cpp b/src/tactic/core/dom_simplify_tactic.cpp index 1a5089c0a..fc8acee4f 100644 --- a/src/tactic/core/dom_simplify_tactic.cpp +++ b/src/tactic/core/dom_simplify_tactic.cpp @@ -518,11 +518,11 @@ public: bool assert_expr(expr * t, bool sign) override { expr* tt; - if ((!sign && m.is_false(t)) || - (sign && m.is_true(t)) || - (!sign && m.is_not(t, tt) && m.is_true(tt)) || - (sign && m.is_not(t, tt) && m.is_false(tt))) - return false; + if (m.is_false(t) || (m.is_not(t, tt) && m.is_true(tt))) + return sign; + + if (m.is_true(t) || (m.is_not(t, tt) && m.is_false(tt))) + return !sign; m_scoped_substitution.push(); if (!sign) {