diff --git a/src/smt/theory_fpa.cpp b/src/smt/theory_fpa.cpp
index 65a66cf80..0cd803cc0 100644
--- a/src/smt/theory_fpa.cpp
+++ b/src/smt/theory_fpa.cpp
@@ -142,7 +142,8 @@ namespace smt {
         m_trail_stack(*this),
         m_fpa_util(m_converter.fu()),
         m_bv_util(m_converter.bu()),
-        m_arith_util(m_converter.au())
+        m_arith_util(m_converter.au()),
+        m_is_initialized(false)
     {
         params_ref p;
         p.set_bool("arith_lhs", true);
@@ -151,10 +152,24 @@ namespace smt {
 
     theory_fpa::~theory_fpa()
     {
-        ast_manager & m = get_manager();
-        dec_ref_map_values(m, m_conversions);
-        dec_ref_map_values(m, m_wraps);
-        dec_ref_map_values(m, m_unwraps);
+        if (m_is_initialized) {
+            ast_manager & m = get_manager();
+            dec_ref_map_values(m, m_conversions);
+            dec_ref_map_values(m, m_wraps);
+            dec_ref_map_values(m, m_unwraps);
+        }
+        else {
+            SASSERT(m_conversions.empty());
+            SASSERT(m_wraps.empty());
+            SASSERT(m_unwraps.empty());
+        }
+
+        m_is_initialized = false;
+    }
+
+    void theory_fpa::init(context * ctx) {
+        smt::theory::init(ctx);
+        m_is_initialized = true;
     }
 
     app * theory_fpa::fpa_value_proc::mk_value(model_generator & mg, ptr_vector<expr> & values) {
diff --git a/src/smt/theory_fpa.h b/src/smt/theory_fpa.h
index 9db6a88a9..1b0fc6c54 100644
--- a/src/smt/theory_fpa.h
+++ b/src/smt/theory_fpa.h
@@ -148,6 +148,7 @@ namespace smt {
         obj_map<sort, func_decl*> m_wraps;
         obj_map<sort, func_decl*> m_unwraps;
         obj_map<expr, expr*>      m_conversions;
+        bool                      m_is_initialized;
 
         virtual final_check_status final_check_eh();
         virtual bool internalize_atom(app * atom, bool gate_ctx);
@@ -169,9 +170,11 @@ namespace smt {
         virtual void finalize_model(model_generator & mg);
 
     public:
-        theory_fpa(ast_manager& m);
+        theory_fpa(ast_manager & m);
         virtual ~theory_fpa();
 
+        virtual void init(context * ctx);
+
         virtual void display(std::ostream & out) const;
 
     protected: