From 4f131ebba7f3dbd48abbe4c90d9e908aee3e728e Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 14 Jun 2016 16:42:46 -0400
Subject: [PATCH] prevent infinite loop of axiom generation. working StartsWith

---
 src/smt/theory_str.cpp | 12 ++++++++++++
 src/smt/theory_str.h   |  5 +++++
 2 files changed, 17 insertions(+)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index b87881ea6..7bdc9f197 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -601,6 +601,7 @@ void theory_str::propagate() {
         for (unsigned i = 0; i < m_axiom_StartsWith_todo.size(); ++i) {
             instantiate_axiom_StartsWith(m_axiom_StartsWith_todo[i]);
         }
+        m_axiom_StartsWith_todo.reset();
     }
 }
 
@@ -754,6 +755,11 @@ void theory_str::instantiate_axiom_CharAt(enode * e) {
     ast_manager & m = get_manager();
 
     app * expr = e->get_owner();
+    if (axiomatized_terms.contains(expr)) {
+        TRACE("t_str_detail", tout << "already set up CharAt axiom for " << mk_pp(expr, m) << std::endl;);
+        return;
+    }
+    axiomatized_terms.insert(expr);
 
     TRACE("t_str_detail", tout << "instantiate CharAt axiom for " << mk_pp(expr, m) << std::endl;);
 
@@ -790,7 +796,13 @@ void theory_str::instantiate_axiom_CharAt(enode * e) {
 void theory_str::instantiate_axiom_StartsWith(enode * e) {
     context & ctx = get_context();
     ast_manager & m = get_manager();
+
     app * expr = e->get_owner();
+    if (axiomatized_terms.contains(expr)) {
+        TRACE("t_str_detail", tout << "already set up StartsWith axiom for " << mk_pp(expr, m) << std::endl;);
+        return;
+    }
+    axiomatized_terms.insert(expr);
 
     TRACE("t_str_detail", tout << "instantiate StartsWith axiom for " << mk_pp(expr, m) << std::endl;);
 
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 6c332dbd4..6debaad71 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -110,6 +110,11 @@ namespace smt {
         ptr_vector<enode> m_axiom_CharAt_todo;
         ptr_vector<enode> m_axiom_StartsWith_todo;
 
+        // hashtable of all exprs for which we've already set up term-specific axioms --
+        // this prevents infinite recursive descent with respect to axioms that
+        // include an occurrence of the term for which axioms are being generated
+        obj_hashtable<expr> axiomatized_terms;
+
         int tmpStringVarCount;
         int tmpXorVarCount;
         int tmpLenTestVarCount;