diff --git a/src/smt/theory_datatype.cpp b/src/smt/theory_datatype.cpp index 147067d61..da18460f4 100644 --- a/src/smt/theory_datatype.cpp +++ b/src/smt/theory_datatype.cpp @@ -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