From c456795acdffcf5ada19c10303487fe0686cd2f1 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 7 Feb 2017 17:14:11 -0500
Subject: [PATCH] temporarily remove finite model finding from theory_str

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 097cfcb15..b3f2bc478 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -6968,6 +6968,7 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) {
         return;
     }
 
+    /* // temporarily disabled, we are borrowing these testers for something else
     if (m_params.m_FiniteOverlapModels && !finite_model_test_varlists.empty()) {
         // TODO NEXT
         if (finite_model_test_varlists.contains(lhs)) {
@@ -6976,6 +6977,7 @@ void theory_str::handle_equality(expr * lhs, expr * rhs) {
             finite_model_test(rhs, lhs); return;
         }
     }
+    */
 
     if (free_var_attempt(lhs, rhs) || free_var_attempt(rhs, lhs)) {
         return;