From 47e75827ee6122e99f7631c92d21d3beae3db924 Mon Sep 17 00:00:00 2001
From: "Christoph M. Wintersteiger" <cwinter@microsoft.com>
Date: Tue, 31 May 2016 16:22:48 +0100
Subject: [PATCH] theory_fpa refactoring

---
 src/smt/theory_fpa.cpp | 11 ++++++-----
 1 file changed, 6 insertions(+), 5 deletions(-)

diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 215260607..6038867aa 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -132,13 +132,13 @@ namespace smt {
             m_converter.reset();
             m_rw.reset();
             m_th_rw.reset();
+            m_is_initialized = false;
         }
 
         SASSERT(m_trail_stack.get_num_scopes() == 0);
         SASSERT(m_conversions.empty());
-        SASSERT(m_is_added_to_model.empty());                
-    }
-
+        SASSERT(m_is_added_to_model.empty());        
+    }    
     void theory_fpa::init(context * ctx) {
         smt::theory::init(ctx);
         m_is_initialized = true;
@@ -710,10 +710,11 @@ namespace smt {
         pop_scope_eh(m_trail_stack.get_num_scopes());
         m_converter.reset();
         m_rw.reset();
-        m_th_rw.reset();
+        m_th_rw.reset();        
         m_trail_stack.pop_scope(m_trail_stack.get_num_scopes());        
+        if (m_factory) dealloc(m_factory); m_factory = 0;
         ast_manager & m = get_manager();
-        dec_ref_map_key_values(m, m_conversions);        
+        dec_ref_map_key_values(m, m_conversions);
         dec_ref_collection_values(m, m_is_added_to_model);
         theory::reset_eh();
     }