diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 308b07d1a..bbb06f719 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -2366,11 +2366,6 @@ void context::updt_params() {
     }
 }
 
-void context::display_certificate(std::ostream& out) const {
-    proof_ref pr = get_proof();
-    out << pr;
-}
-
 void context::reset()
 {
     TRACE("spacer", tout << "\n";);
@@ -2507,7 +2502,7 @@ void context::add_cover(int level, func_decl* p, expr* property, bool bg)
 }
 
 void context::add_invariant (func_decl *p, expr *property)
-{add_cover (infty_level(), p, property, true);}
+{add_cover (infty_level(), p, property, use_bg_invs());}
 
 expr_ref context::get_reachable(func_decl *p) {
     pred_transformer* pt = nullptr;
@@ -2747,7 +2742,7 @@ lbool context::solve(unsigned from_lvl)
     if (m_last_result == l_true) {
         m_stats.m_cex_depth = get_cex_depth ();
     }
- 
+
     if (m_params.print_statistics ()) {
         statistics st;
         collect_statistics (st);
@@ -2931,10 +2926,6 @@ expr_ref context::get_answer()
     }
 }
 
-/**
-   \brief Retrieve satisfying assignment with explanation.
-*/
-expr_ref context::mk_sat_answer() {return get_ground_sat_answer();}
 
 
 expr_ref context::mk_unsat_answer() const
@@ -2957,8 +2948,7 @@ proof_ref context::get_ground_refutation() {
     ground_sat_answer_op op(*this);
     return op(*m_query);
 }
-expr_ref context::get_ground_sat_answer()
-{
+expr_ref context::get_ground_sat_answer() const {
     if (m_last_result != l_true) {
         IF_VERBOSE(0, verbose_stream()
                    << "Sat answer unavailable when result is false\n";);
@@ -3086,6 +3076,20 @@ expr_ref context::get_ground_sat_answer()
     return expr_ref(m.mk_and(cex.size(), cex.c_ptr()), m);
 }
 
+void context::display_certificate(std::ostream &out) const {
+    switch(m_last_result) {
+    case l_false:
+        out << mk_pp(mk_unsat_answer(), m);
+        break;
+    case l_true:
+        out << mk_pp(mk_sat_answer(), m);
+        break;
+    case l_undef:
+        out << "unknown";
+        break;
+    }
+}
+
 ///this is where everything starts
 lbool context::solve_core (unsigned from_lvl)
 {
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 8dd13cf63..494de1c23 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -1007,7 +1007,10 @@ class context {
                          const vector<bool>& reach_pred_used,
                          pob_ref_buffer &out);
 
-    expr_ref mk_sat_answer();
+    /**
+       \brief Retrieve satisfying assignment with explanation.
+    */
+    expr_ref mk_sat_answer() const {return get_ground_sat_answer();}
     expr_ref mk_unsat_answer() const;
     unsigned get_cex_depth ();
 
@@ -1083,7 +1086,7 @@ public:
      * get bottom-up (from query) sequence of ground predicate instances
      * (for e.g. P(0,1,0,0,3)) that together form a ground derivation to query
      */
-    expr_ref get_ground_sat_answer ();
+    expr_ref get_ground_sat_answer () const;
     proof_ref get_ground_refutation();
     void get_rules_along_trace (datalog::rule_ref_vector& rules);
 
diff --git a/src/muz/spacer/spacer_generalizers.cpp b/src/muz/spacer/spacer_generalizers.cpp
index 6f9758337..9d2c00c33 100644
--- a/src/muz/spacer/spacer_generalizers.cpp
+++ b/src/muz/spacer/spacer_generalizers.cpp
@@ -107,8 +107,7 @@ void lemma_bool_inductive_generalizer::operator()(lemma_ref &lemma) {
             expand_literals(m, extra_lits);
             SASSERT(extra_lits.size() > 0);
             bool found = false;
-            if (extra_lits.get(0) != lit) {
-                SASSERT(extra_lits.size() > 1);
+            if (extra_lits.get(0) != lit && extra_lits.size() > 1) {
                 for (unsigned j = 0, sz = extra_lits.size(); !found && j < sz; ++j) {
                     cube[i] = extra_lits.get(j);
                     if (pt.check_inductive(lemma->level(), cube, uses_level, weakness)) {