From dfbd285daefb394741d5e5052f9c6fba1f6f3b04 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 6 Jul 2018 22:02:48 -0700 Subject: [PATCH] avoid rewriting if reduces to tautology Signed-off-by: Nikolaj Bjorner --- src/smt/theory_lra.cpp | 6 ++++-- 1 file changed, 4 insertions(+), 2 deletions(-) diff --git a/src/smt/theory_lra.cpp b/src/smt/theory_lra.cpp index b105def2c..9315e75ac 100644 --- a/src/smt/theory_lra.cpp +++ b/src/smt/theory_lra.cpp @@ -1373,8 +1373,10 @@ public: expr_ref atom1(m); proof_ref atomp(m); ctx().get_rewriter()(atom, atom1, atomp); - atom = to_app(atom1); - TRACE("arith", tout << atom << "\n"; + if (!m.is_false(atom1) && !m.is_true(atom1)) { + atom = to_app(atom1); + } + TRACE("arith", tout << t << ": " << atom << "\n"; m_solver->print_term(term, tout << "bound atom: "); tout << " <= " << k << "\n";); ctx().internalize(atom, true); ctx().mark_as_relevant(atom.get());