From d4e476d764692927929a3c98d4b03236f82bc62d Mon Sep 17 00:00:00 2001
From: Arie Gurfinkel <arie.gurfinkel@uwaterloo.ca>
Date: Sun, 11 Nov 2018 09:06:36 -0500
Subject: [PATCH] Work around unexpected behaviour in generalizer

---
 src/muz/spacer/spacer_generalizers.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

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)) {