diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index a8ee01cff..8d0a4f627 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1122,7 +1122,13 @@ lemma::lemma(pob_ref const &p) :
     m_bindings(m), m_lvl(p->level()),
     m_pob(p), m_new_pob(m_pob) {SASSERT(m_pob);}
 
-lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) : lemma(p) {
+lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) :
+    m_ref_count(0), 
+    m(p->get_ast_manager()),
+    m_body(m), m_cube(m),
+    m_bindings(m), m_lvl(p->level()),
+    m_pob(p), m_new_pob(m_pob)
+{
     update_cube(p, cube);
     set_level(lvl);
 }
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index f27ece97c..78541130c 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -119,7 +119,7 @@ public:
     lemma(ast_manager &manager, expr * fml, unsigned lvl);
     lemma(pob_ref const &p);
     lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl);
-    lemma(const lemma &other) = delete;
+//    lemma(const lemma &other) = delete;
 
     ast_manager &get_ast_manager() {return m;}
     expr *get_expr();
@@ -648,7 +648,7 @@ public:
 
     unsigned max_level () {return m_max_level;}
     unsigned min_depth () {return m_min_depth;}
-    unsigned size () {return m_obligations.size ();}
+    size_t size () {return m_obligations.size ();}
 
 };