From 981e521b18648c0f1408fc02e77082d7ab1915eb Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Mon, 18 Dec 2017 12:06:10 -0500
Subject: [PATCH] Cleanup lemma definition

exposes a potential bug. See comments in code.
---
 src/muz/spacer/spacer_context.cpp | 11 +++++++----
 src/muz/spacer/spacer_context.h   |  6 ++++--
 2 files changed, 11 insertions(+), 6 deletions(-)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index ac5dc7477..9d1aafc9a 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1177,7 +1177,7 @@ void pred_transformer::inherit_properties(pred_transformer& other)
 lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) :
     m_ref_count(0), m(manager),
     m_body(body, m), m_cube(m),
-    m_bindings(m), m_zks(m), m_lvl(lvl),
+    m_zks(m), m_bindings(m), m_lvl(lvl),
     m_pob(nullptr), m_new_pob(false) {
     SASSERT(m_body);
     normalize(m_body, m_body);
@@ -1186,17 +1186,17 @@ lemma::lemma (ast_manager &manager, expr * body, unsigned lvl) :
 lemma::lemma(pob_ref const &p) :
     m_ref_count(0), m(p->get_ast_manager()),
     m_body(m), m_cube(m),
-    m_bindings(m), m_zks(m), m_lvl(p->level()),
+    m_zks(m), m_bindings(m), m_lvl(p->level()),
     m_pob(p), m_new_pob(m_pob) {SASSERT(m_pob); m_pob->get_skolems(m_zks);}
 
 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_zks(m), m_lvl(p->level()),
+    m_zks(m), m_bindings(m), m_lvl(p->level()),
     m_pob(p), m_new_pob(m_pob)
 {
-    m_pob->get_skolems(m_zks);
+    if (m_pob) {m_pob->get_skolems(m_zks);}
     update_cube(p, cube);
     set_level(lvl);
 }
@@ -1229,6 +1229,9 @@ void lemma::mk_expr_core() {
                                      names.c_ptr(),
                                      m_body, 15, symbol(m_body->get_id()));
             if (m_new_pob) {
+                // XXX This assertion will fail when a lemma is
+                // XXX generalized with additional quantified variables
+                SASSERT(m_pob->get_binding().size() == m_zks.size());
                 add_binding(m_pob->get_binding());
             }
         }
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 708497460..b90d84793 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -110,8 +110,8 @@ class lemma {
     ast_manager &m;
     expr_ref m_body;
     expr_ref_vector m_cube;
-    app_ref_vector m_bindings;
     app_ref_vector m_zks;
+    app_ref_vector m_bindings;
     unsigned m_lvl;
     pob_ref m_pob;
     bool m_new_pob;
@@ -134,7 +134,9 @@ public:
     pob_ref &get_pob() {return m_pob;}
     inline unsigned weakness();
 
-    void set_skolems(app_ref_vector &zks) { m_zks.append(zks); }
+    void add_skolems(app_ref_vector &zks) {m_zks.append(zks);}
+    void add_skolem(app *zk) {m_zks.push_back(zk);}
+
     unsigned level () const {return m_lvl;}
     void set_level (unsigned lvl) {m_lvl = lvl;}
     app_ref_vector& get_bindings() {return m_bindings;}