diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 40569295b..172aff40f 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -463,7 +463,8 @@ lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) :
     m_ref_count(0), m(manager),
     m_body(body, m), m_cube(m),
     m_zks(m), m_bindings(m), m_lvl(lvl), m_init_lvl(m_lvl),
-    m_pob(nullptr), m_ctp(nullptr), m_external(false), m_bumped(0) {
+    m_pob(nullptr), m_ctp(nullptr), m_external(false),
+    m_bumped(0), m_weakness(UINT_MAX) {
     SASSERT(m_body);
     normalize(m_body, m_body);
 }
@@ -472,7 +473,8 @@ lemma::lemma(pob_ref const &p) :
     m_ref_count(0), m(p->get_ast_manager()),
     m_body(m), m_cube(m),
     m_zks(m), m_bindings(m), m_lvl(p->level()), m_init_lvl(m_lvl),
-    m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0) {
+    m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0),
+    m_weakness(p->weakness()) {
     SASSERT(m_pob);
     m_pob->get_skolems(m_zks);
     add_binding(m_pob->get_binding());
@@ -483,7 +485,8 @@ lemma::lemma(pob_ref const &p, expr_ref_vector &cube, unsigned lvl) :
     m(p->get_ast_manager()),
     m_body(m), m_cube(m),
     m_zks(m), m_bindings(m), m_lvl(p->level()), m_init_lvl(m_lvl),
-    m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0)
+    m_pob(p), m_ctp(nullptr), m_external(false), m_bumped(0),
+    m_weakness(p->weakness())
 {
     if (m_pob) {
         m_pob->get_skolems(m_zks);
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 37b035b98..87beb472e 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -128,6 +128,7 @@ class lemma {
     model_ref m_ctp; // counter-example to pushing
     bool m_external;
     unsigned m_bumped;
+    unsigned m_weakness;
 
     void mk_expr_core();
     void mk_cube_core();
@@ -154,7 +155,7 @@ public:
 
     bool has_pob() {return m_pob;}
     pob_ref &get_pob() {return m_pob;}
-    inline unsigned weakness();
+    unsigned weakness() {return m_weakness;}
 
     void add_skolem(app *zk, app* b);
 
@@ -690,7 +691,6 @@ struct pob_ref_gt :
         {return gt (n1.get (), n2.get ());}
 };
 
-inline unsigned lemma::weakness() {return m_pob ? m_pob->weakness() : UINT_MAX;}
 /**
  */
 class derivation {