From 4a2eb909bfb96fceb6b61b3bee4a3b15b5f31eb9 Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Sat, 9 Jun 2018 10:34:05 -0700
Subject: [PATCH] Re-fixing a bug in compute_implicant_literals()

---
 src/muz/spacer/spacer_util.cpp | 8 ++++++++
 1 file changed, 8 insertions(+)

diff --git a/src/muz/spacer/spacer_util.cpp b/src/muz/spacer/spacer_util.cpp
index 876a6528a..da946e211 100644
--- a/src/muz/spacer/spacer_util.cpp
+++ b/src/muz/spacer/spacer_util.cpp
@@ -603,6 +603,14 @@ namespace {
 
     void compute_implicant_literals (model_evaluator_util &mev, expr_ref_vector &formula,
                                      expr_ref_vector &res) {
+        // flatten the formula and remove all trivial literals
+
+        // TBD: not clear why there is a dependence on it (other than
+        // not handling of Boolean constants by implicant_picker), however,
+        // it was a source of a problem on a benchmark
+        flatten_and(formula);
+        if (formula.empty()) {return;}
+
         implicant_picker ipick (mev);
         ipick (formula, res);
     }