From 6f6c8d76eb3f9a4aa258d3c3d3a1176dcdc465b9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 6 May 2020 09:45:38 -0700
Subject: [PATCH] fix #4216

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/smt_consequences.cpp | 17 +++++++++++------
 src/smt/theory_arith_eq.h    | 13 ++++++-------
 2 files changed, 17 insertions(+), 13 deletions(-)

diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index 62f0f2f1f..7cb642d62 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -100,6 +100,14 @@ namespace smt {
 
     void context::justify(literal lit, index_set& s) {
         (void)m;
+        auto add_antecedent = [&](literal l) {
+            CTRACE("context", !m_antecedents.contains(l.var()), 
+                   tout << "untracked literal: " << l << " " 
+                   << mk_pp(bool_var2expr(l.var()), m) << "\n";);
+            if (m_antecedents.contains(l.var())) {
+                s |= m_antecedents[l.var()];
+            }
+        };
         b_justification js = get_justification(lit.var());
         switch (js.get_kind()) {
         case b_justification::CLAUSE: {
@@ -107,13 +115,13 @@ namespace smt {
             if (!cls) break;
             for (literal lit2 : *cls) {
                 if (lit2.var() != lit.var()) {
-                    s |= m_antecedents.find(lit2.var());
+                    add_antecedent(lit2);
                 }
             }
             break;
         }
         case b_justification::BIN_CLAUSE: {
-            s |= m_antecedents.find(js.get_literal().var());
+            add_antecedent(js.get_literal());
             break;
             }
         case b_justification::AXIOM: {
@@ -123,10 +131,7 @@ namespace smt {
             literal_vector literals;
             m_conflict_resolution->justification2literals(js.get_justification(), literals);
             for (unsigned j = 0; j < literals.size(); ++j) {
-                if (!m_antecedents.contains(literals[j].var())) {
-                    TRACE("context", tout << literals[j] << " " << mk_pp(bool_var2expr(literals[j].var()), m) << "\n";);
-                }
-                s |= m_antecedents.find(literals[j].var());
+                add_antecedent(literals[j]);
             }
             break;
         }
diff --git a/src/smt/theory_arith_eq.h b/src/smt/theory_arith_eq.h
index 9ab4b8da1..054573417 100644
--- a/src/smt/theory_arith_eq.h
+++ b/src/smt/theory_arith_eq.h
@@ -248,7 +248,7 @@ namespace smt {
                     //
                     // x1 <= k1 x1 >= k1, x2 <= x1 + k2 x2 >= x1 + k2
                     // 
-                    TRACE("arith_eq_propagation", tout << "fixed\n";);
+                    TRACE("arith_eq", tout << "fixed\n";);
                     lower(x2)->push_justification(ante, numeral::zero(), proofs_enabled());
                     upper(x2)->push_justification(ante, numeral::zero(), proofs_enabled());
                     m_stats.m_fixed_eqs++;
@@ -350,14 +350,13 @@ namespace smt {
                     antecedents.num_params(), antecedents.params("eq-propagate")));
         TRACE("arith_eq", tout << "detected equality: #" << _x->get_owner_id() << " = #" << _y->get_owner_id() << "\n";
               display_var(tout, x);
-              display_var(tout, y););
-        TRACE("arith_eq_propagation",
-              for (unsigned i = 0; i <  lits.size(); ++i) {
-                  ctx.display_detailed_literal(tout, lits[i]);
+              display_var(tout, y); 
+              for (literal lit : lits) {
+                  ctx.display_detailed_literal(tout, lit);
                   tout << "\n";
               } 
-              for (unsigned i = 0; i < eqs.size(); ++i) {
-                  tout << mk_pp(eqs[i].first->get_owner(), m) << " = " << mk_pp(eqs[i].second->get_owner(), m) << "\n";
+              for (auto const& p : eqs) {
+                  tout << mk_pp(p.first->get_owner(), m) << " = " << mk_pp(p.second->get_owner(), m) << "\n";
               } 
               tout << " ==> ";
               tout << mk_pp(_x->get_owner(), m) << " = " << mk_pp(_y->get_owner(), m) << "\n";