From eeba30a27756f64c1dcdbbe239d738d6427a1458 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 19 Jun 2018 10:56:45 -0700
Subject: [PATCH] fix #1677

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

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 3b81a35dc..d5fe54fae 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -712,12 +712,30 @@ unsigned theory_seq::find_branch_start(unsigned k) {
     return 0;
 }
 
-bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs) {
+expr_ref_vector theory_seq::expand_strings(expr_ref_vector const& es) {
+    expr_ref_vector ls(m);
+    for (expr* e : es) {
+        zstring s;
+        if (m_util.str.is_string(e, s)) {
+            for (unsigned i = 0; i < s.length(); ++i) {
+                ls.push_back(m_util.str.mk_unit(m_util.str.mk_char(s, i)));
+            }
+        }
+        else {
+            ls.push_back(e);
+        }
+    }
+    return ls;
+}
+
+bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& _ls, expr_ref_vector const& _rs) {
+    expr_ref_vector ls = expand_strings(_ls);
+    expr_ref_vector rs = expand_strings(_rs);
 
     if (ls.empty()) {
         return false;
     }
-    expr* l = ls[0];
+    expr* l = ls.get(0);
 
     if (!is_var(l)) {
         return false;
@@ -735,9 +753,9 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
     }
     for (; start < rs.size(); ++start) {
         unsigned j = start;
-        SASSERT(!m_util.str.is_concat(rs[j]));
-        SASSERT(!m_util.str.is_string(rs[j]));
-        if (l == rs[j]) {
+        SASSERT(!m_util.str.is_concat(rs.get(j)));
+        SASSERT(!m_util.str.is_string(rs.get(j)));
+        if (l == rs.get(j)) {
             return false;
         }
         if (!can_be_equal(ls.size() - 1, ls.c_ptr() + 1, rs.size() - j - 1, rs.c_ptr() + j + 1)) {
@@ -752,8 +770,11 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
     }
 
     bool all_units = true;
-    for (unsigned j = 0; all_units && j < rs.size(); ++j) {
-        all_units &= m_util.str.is_unit(rs[j]);
+    for (expr* r : rs) {
+        if (!m_util.str.is_unit(r)) {
+            all_units = false;
+            break;
+        }
     }
     if (all_units) {
         context& ctx = get_context();
@@ -765,20 +786,20 @@ bool theory_seq::find_branch_candidate(unsigned& start, dependency* dep, expr_re
                 lits.push_back(~mk_eq(l, v0, false));
             }
         }
-        for (unsigned i = 0; i < lits.size(); ++i) {
-            switch (ctx.get_assignment(lits[i])) {
+        for (literal lit : lits) {
+            switch (ctx.get_assignment(lit)) {
             case l_true:  break;
             case l_false: start = 0; return true;
-            case l_undef: ctx.force_phase(~lits[i]); start = 0; return true;
+            case l_undef: ctx.force_phase(~lit); start = 0; return true;
             }
         }
         set_conflict(dep, lits);
         TRACE("seq", 
               tout << "start: " << start << "\n";
-              for (unsigned i = 0; i < lits.size(); ++i) {
-                  ctx.display_literal_verbose(tout << lits[i] << ": ", lits[i]); 
+              for (literal lit : lits) {
+                  ctx.display_literal_verbose(tout << lit << ": ", lit); 
                   tout << "\n";
-                  ctx.display(tout, ctx.get_justification(lits[i].var()));
+                  ctx.display(tout, ctx.get_justification(lit.var()));
                   tout << "\n";
               });
         return true;
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index 3cacf3326..2f7cfd2b3 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -447,6 +447,7 @@ namespace smt {
         void insert_branch_start(unsigned k, unsigned s);
         unsigned find_branch_start(unsigned k);
         bool find_branch_candidate(unsigned& start, dependency* dep, expr_ref_vector const& ls, expr_ref_vector const& rs);
+        expr_ref_vector expand_strings(expr_ref_vector const& es);
         bool can_be_equal(unsigned szl, expr* const* ls, unsigned szr, expr* const* rs) const;
         lbool assume_equality(expr* l, expr* r);