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