From f91af026758dad6c8f92d430fef0669694fd2f41 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Thu, 17 Oct 2019 14:13:02 -0400
Subject: [PATCH] z3str3: set up axioms on string terms that are added during
 the search

---
 src/smt/theory_str.cpp | 17 ++++++++++++++++-
 src/smt/theory_str.h   |  3 +++
 2 files changed, 19 insertions(+), 1 deletion(-)

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index bf3a2a1b3..8d5c18214 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -8160,6 +8160,16 @@ namespace smt {
         sort * rhs_sort = m.get_sort(rhs);
         sort * str_sort = u.str.mk_string_sort();
 
+        // Pick up new terms added during the search (e.g. recursive function expansion).
+        if (!existing_toplevel_exprs.contains(lhs)) {
+            existing_toplevel_exprs.insert(lhs);
+            set_up_axioms(lhs);
+        }
+        if (!existing_toplevel_exprs.contains(rhs)) {
+            existing_toplevel_exprs.insert(rhs);
+            set_up_axioms(rhs);
+        }
+
         if (lhs_sort != str_sort || rhs_sort != str_sort) {
             TRACE("str", tout << "skip equality: not String sort" << std::endl;);
             return;
@@ -8615,7 +8625,12 @@ namespace smt {
     }
 
     void theory_str::assign_eh(bool_var v, bool is_true) {
-        TRACE("str", tout << "assert: v" << v << " #" << get_context().bool_var2expr(v)->get_id() << " is_true: " << is_true << std::endl;);
+        expr * e = get_context().bool_var2expr(v);
+        TRACE("str", tout << "assert: v" << v << " " << mk_pp(e, get_manager()) << " is_true: " << is_true << std::endl;);
+        if (!existing_toplevel_exprs.contains(e)) {
+            existing_toplevel_exprs.insert(e);
+            set_up_axioms(e);
+        }
     }
 
     void theory_str::push_scope_eh() {
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index 1d6e71204..6a6c1a437 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -346,6 +346,9 @@ protected:
     // include an occurrence of the term for which axioms are being generated
     obj_hashtable<expr> axiomatized_terms;
 
+    // hashtable of all top-level exprs for which set_up_axioms() has been called
+    obj_hashtable<expr> existing_toplevel_exprs;
+
     int tmpStringVarCount;
     int tmpXorVarCount;
     int tmpLenTestVarCount;