From f8c13792a355f5af3505c77e6f9cf883794910ad Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Wed, 30 Sep 2015 09:45:00 -0400
Subject: [PATCH] mark the position of the bug I found so I can recall it later
 in process_concat_eq_type1() line 1048

---
 src/smt/theory_str.cpp | 35 +++++++++++++++++++++++------------
 src/smt/theory_str.h   |  2 ++
 2 files changed, 25 insertions(+), 12 deletions(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 440aaeb9f..aad15bec8 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1045,6 +1045,7 @@ void theory_str::process_concat_eq_type1(expr * concatAst1, expr * concatAst2) {
 
             expr_ref m_plus_t2(m_autil.mk_add(mk_strlen(m), mk_strlen(t2)), mgr);
 
+            // TODO here is the bug: these EQs should be GTs
             and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(x), m_plus_t2));
             and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(x), mk_strlen(m)));
             and_item[pos++] = ctx.mk_eq_atom(or_item[option], ctx.mk_eq_atom(mk_strlen(n), mk_strlen(y)));
@@ -1724,6 +1725,7 @@ void theory_str::init_search_eh() {
      * This is done to find equalities between terms, etc. that we otherwise
      * might not get a chance to see.
      */
+    /*
     expr_ref_vector assignments(m);
     ctx.get_assignments(assignments);
     for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) {
@@ -1745,6 +1747,7 @@ void theory_str::init_search_eh() {
                     << ": expr ignored" << std::endl;);
         }
     }
+    */
 
     TRACE("t_str", tout << "search started" << std::endl;);
     search_started = true;
@@ -1755,12 +1758,16 @@ void theory_str::new_eq_eh(theory_var x, theory_var y) {
     TRACE("t_str", tout << "new eq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " = " <<
                                   mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;);
     handle_equality(get_enode(x)->get_owner(), get_enode(y)->get_owner());
+
+    TRACE("t_str_detail", dump_assignments(););
 }
 
 void theory_str::new_diseq_eh(theory_var x, theory_var y) {
     //TRACE("t_str_detail", tout << "new diseq: v#" << x << " != v#" << y << std::endl;);
     TRACE("t_str", tout << "new diseq: " << mk_ismt2_pp(get_enode(x)->get_owner(), get_manager()) << " != " <<
                                   mk_ismt2_pp(get_enode(y)->get_owner(), get_manager()) << std::endl;);
+
+    TRACE("t_str_detail", dump_assignments(););
 }
 
 void theory_str::relevant_eh(app * n) {
@@ -1779,7 +1786,7 @@ void theory_str::push_scope_eh() {
 void theory_str::pop_scope_eh(unsigned num_scopes) {
     TRACE("t_str", tout << "pop " << num_scopes << std::endl;);
     context & ctx = get_context();
-    unsigned sLevel = ctx.get_scope_level();
+    int sLevel = ctx.get_scope_level();
     std::map<expr*, std::stack<T_cut *> >::iterator varItor = cut_var_map.begin();
     while (varItor != cut_var_map.end()) {
         while ((varItor->second.size() > 0) && (varItor->second.top()->level != 0) && (varItor->second.top()->level >= sLevel)) {
@@ -1794,21 +1801,25 @@ void theory_str::pop_scope_eh(unsigned num_scopes) {
     }
 }
 
+void theory_str::dump_assignments() {
+	ast_manager & m = get_manager();
+	context & ctx = get_context();
+	TRACE("t_str_detail",
+	tout << "dumping all assignments:" << std::endl;
+	expr_ref_vector assignments(m);
+	ctx.get_assignments(assignments);
+	for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) {
+		expr * ex = *i;
+		tout << mk_ismt2_pp(ex, m) << std::endl;
+	}
+	);
+}
+
 final_check_status theory_str::final_check_eh() {
-    ast_manager & m = get_manager();
-    context & ctx = get_context();
     // TODO
     TRACE("t_str", tout << "final check" << std::endl;);
 
-    TRACE("t_str_detail",
-        tout << "dumping all assignments:" << std::endl;
-        expr_ref_vector assignments(m);
-        ctx.get_assignments(assignments);
-        for (expr_ref_vector::iterator i = assignments.begin(); i != assignments.end(); ++i) {
-            expr * ex = *i;
-            tout << mk_ismt2_pp(ex, m) << std::endl;
-        }
-    );
+    TRACE("t_str_detail", dump_assignments(););
 
     return FC_DONE;
 }
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 5d0ec96db..930c8e9c8 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -136,6 +136,8 @@ namespace smt {
 
         bool new_eq_check(expr * lhs, expr * rhs);
         void group_terms_by_eqc(expr * n, std::set<expr*> & concats, std::set<expr*> & vars, std::set<expr*> & consts);
+
+        void dump_assignments();
     public:
         theory_str(ast_manager & m);
         virtual ~theory_str();