From 6a0b70ee5cb3664fafee08068626b9a68778bf78 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Mon, 18 Jun 2018 20:42:53 -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 | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index 91da5a078..03bf81d45 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2898,14 +2898,13 @@ 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) {
+    else if (m_util.str.is_string(e)) {
         result = add_elim_string_axiom(e);
     }
     else {