From 4634d1daed5a173b5bca26995dba51256bad521f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 Jun 2018 20:37:39 -0700
Subject: [PATCH] selective expansion of strings for canonizer to fix #1690
 regression

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

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 2b2c35466..91da5a078 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2251,9 +2251,6 @@ bool theory_seq::internalize_term(app* term) {
         e = ctx.mk_enode(term, false, m.is_bool(term), true);
     }
     mk_var(e);
-    if (m_util.str.is_string(term)) {
-        add_elim_string_axiom(term);
-    }
     return true;
 }
 
@@ -2901,12 +2898,16 @@ expr_ref theory_seq::expand(expr* e, dependency*& eqs) {
 expr_ref theory_seq::try_expand(expr* e, dependency*& eqs){
     expr_ref result(m);
     expr_dep ed;
+    zstring s;
     if (m_rep.find_cache(e, ed)) {
         if (e != ed.first) {
             eqs = m_dm.mk_join(eqs, ed.second);
         }
         result = ed.first;
     }
+    else if (m_util.str.is_string(e, s) && s.length() > 0) {
+        result = add_elim_string_axiom(e);
+    }
     else {
         m_expand_todo.push_back(e);
     }
@@ -2929,7 +2930,7 @@ expr_ref theory_seq::expand1(expr* e0, dependency*& eqs) {
     }
     else if (m_util.str.is_empty(e) || m_util.str.is_string(e)) {
         result = e;
-    }
+    }    
     else if (m_util.str.is_prefix(e, e1, e2)) {
         arg1 = try_expand(e1, deps);
         arg2 = try_expand(e2, deps);
@@ -3286,12 +3287,12 @@ void theory_seq::add_replace_axiom(expr* r) {
     tightest_prefix(s, x);
 }
 
-void theory_seq::add_elim_string_axiom(expr* n) {
+expr_ref theory_seq::add_elim_string_axiom(expr* n) {
     zstring s;
     TRACE("seq", tout << mk_pp(n, m) << "\n";);
     VERIFY(m_util.str.is_string(n, s));
     if (s.length() == 0) {
-        return;
+        return expr_ref(n, m);
     }
     expr_ref result(m_util.str.mk_unit(m_util.str.mk_char(s, s.length()-1)), m);
     for (unsigned i = s.length()-1; i-- > 0; ) {
@@ -3300,6 +3301,7 @@ void theory_seq::add_elim_string_axiom(expr* n) {
     add_axiom(mk_eq(n, result, false));
     m_rep.update(n, result, nullptr);
     m_new_solution = true;
+    return result;
 }
 
 
diff --git a/src/smt/theory_seq.h b/src/smt/theory_seq.h
index b6b553dec..3cacf3326 100644
--- a/src/smt/theory_seq.h
+++ b/src/smt/theory_seq.h
@@ -504,7 +504,7 @@ namespace smt {
         void add_int_string(expr* e);
         bool check_int_string();
 
-        void add_elim_string_axiom(expr* n);
+        expr_ref add_elim_string_axiom(expr* n);
         void add_at_axiom(expr* n);
         void add_in_re_axiom(expr* n);
         void add_itos_axiom(expr* n);