From 66b85e000b419ba414939eeb9fa4e146bbebdfd0 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 7 Apr 2018 01:25:19 -0500 Subject: [PATCH] fix in occurs_check (early exit) --- src/smt/theory_datatype.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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