diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index c0a65cfb7..1c7da4031 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4168,10 +4168,9 @@ namespace smt { break; case FC_CONTINUE: return FC_CONTINUE; - break; } if (m_final_check_idx == old_idx) { - if (level >= max_level) + if (level >= max_level || result == FC_DONE || can_propagate()) break; ++level; }