From 3c692a37ebead7a2714211bb4d7225e33a8805b7 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Sat, 13 May 2017 16:13:32 -0400
Subject: [PATCH] fix consistency check involving strings with escape
 characters

---
 src/smt/theory_str.cpp | 10 ++++++++--
 1 file changed, 8 insertions(+), 2 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 76a26eacf..54cfe5d8a 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -5914,8 +5914,14 @@ namespace smt {
         app * n2_curr = to_app(n2);
 
         // case 0: n1_curr is const string, n2_curr is const string
-        if (u.str.is_string(n1_curr) && u.str.is_string(n2_curr)) {
-            if (n1_curr != n2_curr) {
+        zstring n1_curr_str, n2_curr_str;
+        if (u.str.is_string(n1_curr, n1_curr_str) && u.str.is_string(n2_curr, n2_curr_str)) {
+            TRACE("str", tout << "checking string constants: n1=" << n1_curr_str << ", n2=" << n2_curr_str << std::endl;);
+            if (n1_curr_str == n2_curr_str) {
+                // TODO(mtrberzi) potential correction: if n1_curr != n2_curr,
+                // assert that these two terms are in fact equal, because they ought to be
+                return true;
+            } else {
                 return false;
             }
         }