mirror of
https://github.com/Z3Prover/z3
synced 2025-04-08 10:25:18 +00:00
Work around unexpected behaviour in generalizer
This commit is contained in:
parent
6cc6ffcde2
commit
d4e476d764
|
@ -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)) {
|
||||
|
|
Loading…
Reference in a new issue