mirror of
https://github.com/Z3Prover/z3
synced 2025-04-15 13:28:47 +00:00
fix #4796
This commit is contained in:
parent
98db260a93
commit
36e9412252
|
@ -2198,8 +2198,6 @@ namespace smt {
|
||||||
}
|
}
|
||||||
else {
|
else {
|
||||||
SASSERT(is_quantifier(curr));
|
SASSERT(is_quantifier(curr));
|
||||||
SASSERT(is_lambda(curr));
|
|
||||||
//UNREACHABLE(); // can't happen, the quantifier is supposed to be flat.
|
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
}
|
}
|
||||||
|
|
Loading…
Reference in a new issue