From 2b8f165cc47e197dfc7a6aef0849c2af0c067018 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Fri, 2 Sep 2016 19:04:20 -0400
Subject: [PATCH] patch UNSAT to UNKNOWN in cmd_context for theory_str

---
 src/smt/smt_context.cpp | 20 ++++++++++++++++++++
 src/smt/theory_str.h    |  2 ++
 2 files changed, 22 insertions(+)

diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp
index 046e2028e..251cf3b9b 100644
--- a/src/smt/smt_context.cpp
+++ b/src/smt/smt_context.cpp
@@ -37,6 +37,7 @@ Revision History:
 #include"model_pp.h"
 #include"ast_smt2_pp.h"
 #include"ast_translation.h"
+#include"theory_str.h"
 
 namespace smt {
 
@@ -3086,6 +3087,25 @@ namespace smt {
         if (r == l_true && get_cancel_flag()) {
             r = l_undef;
         }
+
+        // PATCH for theory_str:
+        // UNSAT + overlapping variables => UNKNOWN
+        if (r == l_false) {
+            ptr_vector<theory>::iterator it  = m_theory_set.begin();
+            ptr_vector<theory>::iterator end = m_theory_set.end();
+            for (; it != end; ++it) {
+                theory * th = *it;
+                if (strcmp(th->get_name(), "strings") == 0) {
+                    theory_str * str = (theory_str*)th;
+                    if (str->overlapping_variables_detected()) {
+                        TRACE("t_str", tout << "WARNING: overlapping variables detected, UNSAT changed to UNKNOWN!" << std::endl;);
+                        r = l_undef;
+                    }
+                    break;
+                }
+            }
+        }
+
         return r;
     }
 
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index ba132a579..1fad18293 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -457,6 +457,8 @@ namespace smt {
 
         virtual char const * get_name() const { return "strings"; }
         virtual void display(std::ostream & out) const;
+
+        bool overlapping_variables_detected() const { return loopDetected; }
     protected:
         virtual bool internalize_atom(app * atom, bool gate_ctx);
         virtual bool internalize_term(app * term);