From d9100437ce377bf185cb0b3f9b2da8e79ca9ce60 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Tue, 26 Jun 2018 11:33:54 -0400
Subject: [PATCH] Weakness of the lemma independent of the pob

Lemma inherits its weakness score from the pob. However,
pob's weakness might be reset or changed for some other reason.

To avoid affecting the lemma, the weakness is copied on
construction.
---
 src/muz/spacer/spacer_context.cpp | 9 ++++++---
 src/muz/spacer/spacer_context.h   | 4 ++--
 2 files changed, 8 insertions(+), 5 deletions(-)

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 {