mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 05:48:44 +00:00
Code Activity

avoid rewriting if reduces to tautology

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2018-07-06 22:02:48 -07:00
parent dc932a93e2
commit dfbd285dae
1 changed files with 4 additions and 2 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

6
src/smt/theory_lra.cpp
View file

@ -1373,8 +1373,10 @@ public:
expr_ref atom1(m); expr_ref atom1(m);
proof_ref atomp(m); proof_ref atomp(m);
ctx().get_rewriter()(atom, atom1, atomp); ctx().get_rewriter()(atom, atom1, atomp);
atom = to_app(atom1); if (!m.is_false(atom1) && !m.is_true(atom1)) {
TRACE("arith", tout << atom << "\n"; atom = to_app(atom1);
}
TRACE("arith", tout << t << ": " << atom << "\n";
m_solver->print_term(term, tout << "bound atom: "); tout << " <= " << k << "\n";); m_solver->print_term(term, tout << "bound atom: "); tout << " <= " << k << "\n";);
ctx().internalize(atom, true); ctx().internalize(atom, true);
ctx().mark_as_relevant(atom.get()); ctx().mark_as_relevant(atom.get());