From 0e6aaf02113eb2bc0f21b21148e17cfaf895aa18 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Thu, 7 Jan 2016 20:05:49 -0800
Subject: [PATCH] Issue #407 build break

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp |  4 ++--
 src/ast/seq_decl_plugin.cpp       |  4 +++-
 src/smt/theory_seq.cpp            | 16 +++++-----------
 3 files changed, 10 insertions(+), 14 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index d85060f1d..d94e54935 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -1064,13 +1064,13 @@ bool seq_rewriter::reduce_eq(expr_ref_vector& ls, expr_ref_vector& rs, expr_ref_
     if (lchange) {
         if (head1 > 0) {
             for (unsigned i = 0; i < szl; ++i) {
-                ls[i] = ls[i + head1];
+                ls[i] = ls[i + head1].get();
             }
         }
         ls.shrink(szl);
         if (head2 > 0) {
             for (unsigned i = 0; i < szr; ++i) {
-                rs[i] = rs[i + head2];
+                rs[i] = rs[i + head2].get();
             }
         }
         rs.shrink(szr);
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 9c8a085e8..165e24eac 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -666,5 +666,7 @@ void seq_util::str::get_concat(expr* e, expr_ref_vector& es) const {
         get_concat(e1, es);
         e = e2;
     }    
-    es.push_back(e);
+    if (!is_empty(e)) {
+        es.push_back(e);
+    }
 }
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index a51e32d90..4bc867717 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -1422,21 +1422,15 @@ bool theory_seq::canonize(expr* e, expr_ref_vector& es, dependency*& eqs) {
             canonize(e1, es, eqs);
             e3 = e2;
             change = true;
-            continue;
         }       
-        if (m_util.str.is_empty(e3)) {
+        else if (m_util.str.is_empty(e3)) {
             return true;
         }
-
-        expr_ref e4 = expand(e3, eqs);
-        change |= e4 != e3;
-        if (m_util.str.is_concat(e4) || m_util.str.is_empty(e4)) {
-            e3 = e4;
-            continue;
-        }
         else {
-            es.push_back(e4);
-            break;
+            expr_ref e4 = expand(e3, eqs);
+            change |= e4 != e3;
+            m_util.str.get_concat(e4, es);
+            break;        
         }
     }
     return change;