diff --git a/src/smt/theory_str.cpp b/src/smt/theory_str.cpp
index 0a3089c62..60b365d20 100644
--- a/src/smt/theory_str.cpp
+++ b/src/smt/theory_str.cpp
@@ -77,6 +77,9 @@ namespace smt {
 
     theory_str::~theory_str() {
         m_trail_stack.reset();
+        for (eautomaton * aut : regex_automata) {
+            dealloc(aut);
+        }
         regex_automata.clear();
     }
 
@@ -10559,6 +10562,7 @@ namespace smt {
                             if ( (current_assignment == l_true && aut.get_polarity())
                                     || (current_assignment == l_false && !aut.get_polarity())) {
                                 aut_inter = m_mk_aut.mk_product(aut_inter, aut.get_automaton());
+                                m_automata.push_back(aut_inter);
                             } else {
                                 // need to complement first
                                 expr_ref rc(u.re.mk_complement(aut.get_regex_term()), m);
@@ -10567,6 +10571,7 @@ namespace smt {
                                 // TODO is there any way to build a complement automaton from an existing one?
                                 // this discards length information
                                 aut_inter = m_mk_aut.mk_product(aut_inter, aut_c);
+                                m_automata.push_back(aut_inter);
                             }
                             used_intersect_constraints.push_back(aut);
                             if (aut_inter->is_empty()) {
diff --git a/src/smt/theory_str.h b/src/smt/theory_str.h
index e9607585f..419084091 100644
--- a/src/smt/theory_str.h
+++ b/src/smt/theory_str.h
@@ -395,6 +395,7 @@ protected:
     obj_map<expr, std::set<zstring> > regex_in_var_reg_str_map;
 
     // regex automata
+    scoped_ptr_vector<eautomaton> m_automata;
     ptr_vector<eautomaton> regex_automata;
     obj_hashtable<expr> regex_terms;
     obj_map<expr, ptr_vector<expr> > regex_terms_by_string; // S --> [ (str.in.re S *) ]