From eb2d7d3e81c9f83a41e51d6de027d966e2ac21f1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 23 Apr 2020 22:35:33 -0700
Subject: [PATCH] fix #4079

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/smt/seq_eq_solver.cpp    | 23 ++++++-----------------
 src/smt/smt_consequences.cpp | 23 +++++++++++------------
 src/smt/smt_context.cpp      |  4 ++--
 3 files changed, 19 insertions(+), 31 deletions(-)

diff --git a/src/smt/seq_eq_solver.cpp b/src/smt/seq_eq_solver.cpp
index fe21bf2b3..911852034 100644
--- a/src/smt/seq_eq_solver.cpp
+++ b/src/smt/seq_eq_solver.cpp
@@ -750,10 +750,10 @@ void theory_seq::branch_unit_variable(dependency* dep, expr* X, expr_ref_vector
 bool theory_seq::branch_ternary_variable1() {
     int start = get_context().get_random_value();
     for (unsigned i = 0; i < m_eqs.size(); ++i) {
-        eq const& e = m_eqs[(i + start) % m_eqs.size()];
-        if (branch_ternary_variable(e) || branch_ternary_variable2(e)) {
+        if (branch_ternary_variable(m_eqs[(i + start) % m_eqs.size()]))
+            return true;
+        if (branch_ternary_variable2(m_eqs[(i + start) % m_eqs.size()])) 
             return true;
-        }
     }
     return false;
 }
@@ -917,20 +917,10 @@ bool theory_seq::branch_ternary_variable(eq const& e, bool flag1) {
     expr_ref y1ysZ = mk_concat(y1ys, Z);
     if (indexes.empty()) {
         return false;
-#if 0
-        TRACE("seq", display_equation(tout << "one case\n", e);
-              tout << "xs: " << xs << "\n";
-              tout << "ys: " << ys << "\n";);
-        literal_vector lits;
-        dependency* dep = e.dep();
-        propagate_eq(dep, lits, x, y1ysZ, true);
-        propagate_eq(dep, lits, y2, ZxsE, true);
-#endif
     }
 
     literal ge = m_ax.mk_ge(mk_len(y2), xs.size());
     dependency* dep = e.dep();
-    literal_vector lits;
     switch (ctx.get_assignment(ge)) {
     case l_undef:
         TRACE("seq", tout << "rec case init\n";);
@@ -940,12 +930,11 @@ bool theory_seq::branch_ternary_variable(eq const& e, bool flag1) {
     case l_true:
         TRACE("seq", tout << "true branch\n";);
         TRACE("seq", display_equation(tout, e););
-        lits.push_back(ge);
-        propagate_eq(dep, lits, x, y1ysZ, true);
-        propagate_eq(dep, lits, y2, ZxsE, true);
+        propagate_eq(dep, ge, x, y1ysZ, true);
+        propagate_eq(dep, ge, y2, ZxsE, true);
         break;
     default:
-        return branch_ternary_variable_base(e.dep(), indexes, x, xs, y1, ys, y2);
+        return branch_ternary_variable_base(dep, indexes, x, xs, y1, ys, y2);
     }
     return true;
 }
diff --git a/src/smt/smt_consequences.cpp b/src/smt/smt_consequences.cpp
index f92382e3d..f40becae2 100644
--- a/src/smt/smt_consequences.cpp
+++ b/src/smt/smt_consequences.cpp
@@ -347,15 +347,16 @@ namespace smt {
         unsigned chunk_size = 100; 
         
         while (!m_var2val.empty()) {
-            obj_map<expr,expr*>::iterator it = m_var2val.begin(), end = m_var2val.end();
             unsigned num_vars = 0;
-            for (; it != end && num_vars < chunk_size; ++it) {
+            for (auto const& kv : m_var2val) {
+                if (num_vars >= chunk_size)
+                    break;
                 if (get_cancel_flag()) {
                     if (pushed) pop(1);
                     return l_undef;
                 }
-                expr* e = it->m_key;
-                expr* val = it->m_value;
+                expr* e = kv.m_key;
+                expr* val = kv.m_value;
                 literal lit = mk_diseq(e, val);
                 mark_as_relevant(lit);
                 if (get_assignment(lit) != l_undef) {
@@ -364,14 +365,12 @@ namespace smt {
                 ++num_vars;
                 push_scope();
                 assign(lit, b_justification::mk_axiom(), true);
-                if (!propagate()) {
-                    if (!resolve_conflict() || inconsistent()) {
-                        TRACE("context", tout << "inconsistent\n";);
-                        SASSERT(inconsistent());
-                        m_conflict = null_b_justification;
-                        m_not_l = null_literal;
-                        SASSERT(m_search_lvl == get_search_level());
-                    }
+                if (!propagate() && (!resolve_conflict() || inconsistent())) {
+                    TRACE("context", tout << "inconsistent\n";);
+                    SASSERT(inconsistent());
+                    m_conflict = null_b_justification;
+                    m_not_l = null_literal;
+                    SASSERT(m_search_lvl == get_search_level());                    
                 }
             }
             SASSERT(!inconsistent());
diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 89bc839f3..eba9ecb1a 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -1891,7 +1891,7 @@ namespace smt {
         m_region.push_scope();
         m_scopes.push_back(scope());
         scope & s = m_scopes.back();
-        TRACE("context", tout << "push " << m_scope_lvl << "\n";);
+        // TRACE("context", tout << "push " << m_scope_lvl << "\n";);
 
         m_relevancy_propagator->push();
         s.m_assigned_literals_lim    = m_assigned_literals.size();
@@ -2335,7 +2335,7 @@ namespace smt {
             if (m.has_trace_stream() && !m_is_auxiliary)
                 m.trace_stream() << "[pop] " << num_scopes << " " << m_scope_lvl << "\n";
 
-            TRACE("context", tout << "backtracking: " << num_scopes << " from " << m_scope_lvl << "\n";);
+            // TRACE("context", tout << "backtracking: " << num_scopes << " from " << m_scope_lvl << "\n";);
             TRACE("pop_scope_detail", display(tout););
             SASSERT(num_scopes > 0);
             SASSERT(num_scopes <= m_scope_lvl);