From 7759d05efee280bd2360584cab43ec33a1d328ba Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Mon, 19 Mar 2018 23:09:07 -0400
Subject: [PATCH] fix use-after-free

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index ec554df7b..5a39659e8 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -803,8 +803,20 @@ namespace smt {
         context & ctx = get_context();
         while (can_propagate()) {
             TRACE("str", tout << "propagating..." << std::endl;);
-            for (auto const& el : m_basicstr_axiom_todo) {
-                instantiate_basic_string_axioms(el);
+            while(true) {
+                // this can potentially recursively activate itself
+                unsigned start_count = m_basicstr_axiom_todo.size();
+                ptr_vector<enode> axioms_tmp(m_basicstr_axiom_todo);
+                for (auto const& el : axioms_tmp) {
+                    instantiate_basic_string_axioms(el);
+                }
+                unsigned end_count = m_basicstr_axiom_todo.size();
+                if (end_count > start_count) {
+                    TRACE("str", tout << "new basic string axiom terms added -- checking again" << std::endl;);
+                    continue;
+                } else {
+                    break;
+                }
             }
             m_basicstr_axiom_todo.reset();
             TRACE("str", tout << "reset m_basicstr_axiom_todo" << std::endl;);