From 18cd47dcd02c92a5805b1ccb04b4879d06273aa1 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Sun, 12 Jun 2016 20:14:57 -0400
Subject: [PATCH] add flag for bailing out during a final check infinite loop
 in theory_str also adds more debugging to free variable gen

---
 src/smt/theory_str.cpp | 28 +++++++++++++++++++++++++++-
 src/smt/theory_str.h   |  8 ++++++++
 2 files changed, 35 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 02db2132a..aaeb9ccce 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -31,11 +31,13 @@ theory_str::theory_str(ast_manager & m):
         opt_AggressiveLengthTesting(true),
         opt_AggressiveValueTesting(true),
         opt_EagerStringConstantLengthAssertions(true),
+        opt_VerifyFinalCheckProgress(true),
         /* Internal setup */
         search_started(false),
         m_autil(m),
         m_strutil(m),
         sLevel(0),
+        finalCheckProgressIndicator(false),
         m_trail(m),
         tmpStringVarCount(0),
 		tmpXorVarCount(0),
@@ -125,6 +127,9 @@ void theory_str::initialize_charset() {
 }
 
 void theory_str::assert_axiom(expr * e) {
+    if (opt_VerifyFinalCheckProgress) {
+        finalCheckProgressIndicator = true;
+    }
     if (get_manager().is_true(e)) return;
     TRACE("t_str_detail", tout << "asserting " << mk_ismt2_pp(e, get_manager()) << std::endl;);
     context & ctx = get_context();
@@ -4501,6 +4506,10 @@ final_check_status theory_str::final_check_eh() {
     context & ctx = get_context();
     ast_manager & m = get_manager();
 
+    if (opt_VerifyFinalCheckProgress) {
+        finalCheckProgressIndicator = false;
+    }
+
     TRACE("t_str", tout << "final check" << std::endl;);
     TRACE("t_str_detail", dump_assignments(););
 
@@ -4655,7 +4664,19 @@ final_check_status theory_str::final_check_eh() {
 
     constValue = NULL;
 
-    // TODO this would be a great place to print debugging information
+    {
+        TRACE("t_str_detail", tout << "free var map (# " << freeVar_map.size() << "):" << std::endl;
+        for (std::map<expr*, int>::iterator freeVarItor1 = freeVar_map.begin(); freeVarItor1 != freeVar_map.end(); freeVarItor1++) {
+            expr * freeVar = freeVarItor1->first;
+            rational lenValue;
+            bool lenValue_exists = get_len_value(freeVar, lenValue);
+            // TODO get_bound_strlen()
+            tout << mk_pp(freeVar, m) << " [depCnt = " << freeVarItor1->second << ", length = "
+                    << (lenValue_exists ? lenValue.to_string() : "?")
+                    << "]" << std::endl;
+        }
+        );
+    }
 
     // TODO process_concat_eq_unroll()
     /*
@@ -4712,6 +4733,11 @@ final_check_status theory_str::final_check_eh() {
     }
     */
 
+    if (opt_VerifyFinalCheckProgress && !finalCheckProgressIndicator) {
+        TRACE("t_str", tout << "BUG: no progress in final check, giving up!!" << std::endl;);
+        m.raise_exception("no progress in theory_str final check");
+    }
+
     return FC_CONTINUE; // since by this point we've added axioms
 }
 
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 2b8077a13..562f49004 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -83,11 +83,19 @@ namespace smt {
          */
         bool opt_EagerStringConstantLengthAssertions;
 
+        /*
+         * If VerifyFinalCheckProgress is set to true, continuing after final check is invoked
+         * without asserting any new axioms is considered a bug and will throw an exception.
+         */
+        bool opt_VerifyFinalCheckProgress;
+
         bool search_started;
         arith_util m_autil;
         str_util m_strutil;
         int sLevel;
 
+        bool finalCheckProgressIndicator;
+
         // TODO make sure that all generated expressions are saved into the trail
         expr_ref_vector m_trail; // trail for generated terms