diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index a8a904aa1..64d047d73 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1166,6 +1166,10 @@ expr_ref pred_transformer::get_origin_summary (model_evaluator_util &mev,
         summary[i] = v;
     }
 
+    // bail out of if the model is insufficient
+    if (!mev.is_true(summary))
+        return expr_ref(m);
+
     // -- pick an implicant
     expr_ref_vector lits(m);
     compute_implicant_literals (mev, summary, lits);
@@ -3722,6 +3726,10 @@ bool context::create_children(pob& n, datalog::rule const& r,
         expr_ref sum(m);
         sum = pt.get_origin_summary (mev, prev_level(n.level()),
                                      j, reach_pred_used[j], &aux);
+        if (!sum) {
+            dealloc(deriv);
+            return false;
+        }
         deriv->add_premise (pt, j, sum, reach_pred_used[j], aux);
     }
 
diff --git a/src/muz/spacer/spacer_context.h b/src/muz/spacer/spacer_context.h
index 402cb63cc..fcd396a62 100644
--- a/src/muz/spacer/spacer_context.h
+++ b/src/muz/spacer/spacer_context.h
@@ -350,9 +350,6 @@ class pred_transformer {
 
     };
 
-    typedef obj_map<datalog::rule const, expr*> rule2expr;
-    typedef obj_map<datalog::rule const, ptr_vector<app> > rule2apps;
-    typedef obj_map<expr, datalog::rule const*> expr2rule;
     manager&                     pm;                // spacer::manager
     ast_manager&                 m;                 // ast_manager
     context&                     ctx;               // spacer::context