From 9f0eb367b17ca7082cb174ca660fee16b3028cdd Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Fri, 4 Aug 2017 16:12:32 -0400
Subject: [PATCH] ground lemmas during propagation when qlemmas are disabled

When asserting quantified lemmas are disabled, ground a lemma
explicitly during propagate to make sure that it is ground using our
local set of skolem constants.
---
 src/muz/spacer/spacer_context.cpp |  2 +-
 src/muz/spacer/spacer_util.cpp    | 28 ++++++++++++++--------------
 2 files changed, 15 insertions(+), 15 deletions(-)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 4a61688f8..1ab15ae34 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -769,7 +769,7 @@ bool pred_transformer::is_invariant(unsigned level, expr* lemma,
     expr_ref_vector conj(m), aux(m);
     expr_ref glemma(m);
 
-    if (false && is_quantifier(lemma)) {
+    if (!get_context().use_qlemmas() && is_quantifier(lemma)) {
         SASSERT(is_forall(lemma));
         app_ref_vector tmp(m);
         ground_expr(to_quantifier(lemma)->get_expr (), glemma, tmp);
diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index 8b8da8a69..1156b2f9e 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -1166,21 +1166,21 @@ void mk_epp::rw(expr *e, expr_ref &out)
     arw(e, out);
 }
 
-    void ground_expr (expr *e, expr_ref &out, app_ref_vector &vars)
-    {
-         expr_free_vars fv;
-         ast_manager &m = out.get_manager ();
-         fv (e);
-         if (vars.size () < fv.size ())
-    { vars.resize(fv.size()); }
-         for (unsigned i = 0, sz = fv.size (); i < sz; ++i) {
-             SASSERT (fv[i]);
-             std::string str = "zk!" + datalog::to_string(sz - 1 - i);
-             vars [i] = m.mk_const (symbol(str.c_str()), fv [i]);
-         }
-         var_subst vs(m);
-         vs (e, vars.size (), (expr**) vars.c_ptr (), out);
+void ground_expr(expr *e, expr_ref &out, app_ref_vector &vars) {
+    expr_free_vars fv;
+    ast_manager &m = out.get_manager();
+
+    fv(e);
+    if (vars.size() < fv.size()) {
+        vars.resize(fv.size());
     }
+    for (unsigned i = 0, sz = fv.size(); i < sz; ++i) {
+        sort *s = fv[i] ? fv[i] : m.mk_bool_sort();
+        vars[i] = mk_zk_const(m, i, s);
+        var_subst vs(m, false);
+        vs(e, vars.size(), (expr * *) vars.c_ptr(), out);
+    }
+}
 
 
     struct index_term_finder {