From e09964096ea718a388d496fc227faccaf36c4b0e Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Fri, 1 May 2026 16:15:36 -0700 Subject: [PATCH] add continue as an option to breaking loop at level Signed-off-by: Nikolaj Bjorner --- src/smt/smt_context.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index ec7209c93..7b0a8d5ee 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4172,7 +4172,7 @@ namespace smt { return FC_CONTINUE; } if (m_final_check_idx == old_idx) { - if (level >= max_level || result == FC_DONE || can_propagate()) + if (level >= max_level || result == FC_DONE || result == FC_CONTINUE || can_propagate()) break; ++level; // Re-evaluate at the higher level: clear the give-up state