From 6a3ce301b748280f6bb8c1eef959382848b83bf8 Mon Sep 17 00:00:00 2001
From: Murphy Berzish <murphy.berzish@gmail.com>
Date: Tue, 3 Apr 2018 12:51:03 -0400
Subject: [PATCH] fix collection error

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

diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 21b6e7b26..811b66798 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -1854,6 +1854,9 @@ namespace smt {
             std::pair<expr*, zstring> key1(ex->get_arg(0), regexStr);
             // skip Z3str's map check, because we already check if we set up axioms on this term
             regex_in_bool_map[key1] = ex;
+            if (!regex_in_var_reg_str_map.contains(ex->get_arg(0))) {
+                regex_in_var_reg_str_map.insert(ex->get_arg(0), std::set<zstring>());
+            }
             regex_in_var_reg_str_map[ex->get_arg(0)].insert(regexStr);
         }
 
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index d68d99abc..e9607585f 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -399,7 +399,7 @@ protected:
     obj_hashtable<expr> regex_terms;
     obj_map<expr, ptr_vector<expr> > regex_terms_by_string; // S --> [ (str.in.re S *) ]
     obj_map<expr, svector<regex_automaton_under_assumptions> > regex_automaton_assumptions; // RegEx --> [ aut+assumptions ]
-    std::map<expr*, nfa> regex_nfa_cache; // Regex term --> NFA
+    obj_map<expr, nfa> regex_nfa_cache; // Regex term --> NFA
     obj_hashtable<expr> regex_terms_with_path_constraints; // set of string terms which have had path constraints asserted in the current scope
     obj_hashtable<expr> regex_terms_with_length_constraints; // set of regex terms which had had length constraints asserted in the current scope
     obj_map<expr, expr*> regex_term_to_length_constraint; // (str.in.re S R) -> (length constraint over S wrt. R)