3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-08 10:25:18 +00:00

fix in occurs_check (early exit)

This commit is contained in:
Simon Cruanes 2018-04-07 01:25:19 -05:00
parent ac881d949d
commit 66b85e000b

View file

@ -463,7 +463,7 @@ namespace smt {
if (d->m_constructor) {
for (enode * arg : enode::args(d->m_constructor)) {
if (oc_cycle_free(arg)) {
return false;
continue;
}
if (oc_on_stack(arg)) {
// arg was explored before app, and is still on the stack: cycle