From ca4ae171ea95d39fd836972789db09cdbbb7c82f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 21 Mar 2017 07:40:35 -0600
Subject: [PATCH] remove unsound simplification in prefix #949

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 17 +++++++++++------
 src/smt/theory_seq.cpp            |  7 +++++--
 2 files changed, 16 insertions(+), 8 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 26918261e..b7f99298c 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -676,6 +676,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
     bool isc2 = m_util.str.is_string(b, s2);
     if (isc1 && isc2) {
         result = m().mk_bool_val(s1.prefixof(s2));
+        TRACE("seq", tout << result << "\n";);
         return BR_DONE;
     }
     if (m_util.str.is_empty(a)) {
@@ -689,6 +690,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
     expr_ref_vector as(m()), bs(m());
 
     if (a1 != b1 && isc1 && isc2) {
+        TRACE("seq", tout << s1 << " " << s2 << "\n";);
         if (s1.length() <= s2.length()) {
             if (s1.prefixof(s2)) {
                 if (a == a1) {
@@ -733,26 +735,27 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
     m_util.str.get_concat(a, as);
     m_util.str.get_concat(b, bs);
     unsigned i = 0;
-    bool all_values = true;    
     expr_ref_vector eqs(m());
     for (; i < as.size() && i < bs.size(); ++i) {
         expr* a = as[i].get(), *b = bs[i].get();
         if (a == b) {
             continue;
         }
-        all_values &= m().is_value(a) && m().is_value(b);
-        if (all_values) {
-            result = m().mk_false();
-            return BR_DONE;
-        }
         if (m_util.str.is_unit(a) && m_util.str.is_unit(b)) {
             eqs.push_back(m().mk_eq(a, b));
             continue;
         }
+        if (m().is_value(a) && m().is_value(b) && m_util.str.is_string(a) && m_util.str.is_string(b)) {
+            TRACE("seq", tout << mk_pp(a, m()) << " != " << mk_pp(b, m()) << "\n";);
+            result = m().mk_false();
+            return BR_DONE;
+        }
+
         break;
     }
     if (i == as.size()) {
         result = mk_and(eqs);
+        TRACE("seq", tout << result << "\n";);
         if (m().is_true(result)) {
             return BR_DONE;
         }
@@ -764,6 +767,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
             eqs.push_back(m().mk_eq(m_util.str.mk_empty(m().get_sort(a)), as[j].get()));
         }
         result = mk_and(eqs);
+        TRACE("seq", tout << result << "\n";);
         return BR_REWRITE3;
     }
     if (i > 0) {
@@ -771,6 +775,7 @@ br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
         a = m_util.str.mk_concat(as.size() - i, as.c_ptr() + i);
         b = m_util.str.mk_concat(bs.size() - i, bs.c_ptr() + i); 
         result = m_util.str.mk_prefix(a, b);
+        TRACE("seq", tout << result << "\n";);
         return BR_DONE;
     }
     else {
diff --git a/src/smt/theory_seq.cpp b/src/smt/theory_seq.cpp
index d5251c56b..daf5e3702 100644
--- a/src/smt/theory_seq.cpp
+++ b/src/smt/theory_seq.cpp
@@ -2719,7 +2719,9 @@ bool theory_seq::can_propagate() {
 
 expr_ref theory_seq::canonize(expr* e, dependency*& eqs) {
     expr_ref result = expand(e, eqs);
+    TRACE("seq", tout << mk_pp(e, m) << " expands to " << result << "\n";);
     m_rewrite(result);
+    TRACE("seq", tout << mk_pp(e, m) << " rewrites to " << result << "\n";);
     return result;
 }
 
@@ -4469,10 +4471,11 @@ bool theory_seq::canonizes(bool sign, expr* e) {
     context& ctx = get_context();
     dependency* deps = 0;
     expr_ref cont = canonize(e, deps);
-    TRACE("seq", tout << mk_pp(e, m) << " -> " << cont << "\n";);
+    TRACE("seq", tout << mk_pp(e, m) << " -> " << cont << "\n";
+          if (deps) display_deps(tout, deps););
     if ((m.is_true(cont) && !sign) ||
         (m.is_false(cont) && sign)) {
-        TRACE("seq", display(tout););
+        TRACE("seq", display(tout); tout << ctx.get_assignment(ctx.get_literal(e)) << "\n";);
         propagate_lit(deps, 0, 0, ctx.get_literal(e));
         return true;
     }