From 7c924c49f679605f062b15bd92005e550cbc48f6 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Wed, 27 Jun 2018 16:40:49 -0400
Subject: [PATCH] Do not evaluate quantified formulas in a model

---
 src/muz/spacer/spacer_context.cpp | 11 ++++++++++-
 1 file changed, 10 insertions(+), 1 deletion(-)

diff --git a/src/muz/spacer/spacer_context.cpp b/src/muz/spacer/spacer_context.cpp
index 575c9993b..8eee087e6 100644
--- a/src/muz/spacer/spacer_context.cpp
+++ b/src/muz/spacer/spacer_context.cpp
@@ -1184,7 +1184,16 @@ expr_ref pred_transformer::get_origin_summary (model &mdl,
     }
 
     // bail out of if the model is insufficient
-    if (!mdl.is_true(summary)) return expr_ref(m);
+    // (skip quantified lemmas cause we can't validate them in the model)
+    // TBD: for quantified lemmas use current instances
+    flatten_and(summary);
+    for (auto *s : summary) {
+        if (!is_quantifier(s) && !mdl.is_true(s)) {
+            TRACE("spacer", tout << "Summary not true in the model: "
+                  << mk_pp(s, m) << "\n";);
+            return expr_ref(m);
+        }
+    }
 
     // -- pick an implicant
     expr_ref_vector lits(m);