From 3b546b2348fec5a19f708746ee268bc701d00023 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Sun, 20 Aug 2023 10:34:28 +0100 Subject: [PATCH] smt_context: we can't assert that the resource limits were exceeded on cancel_exception It happens sometimes that e.g. the internalizer goes above the soft memory limit But since it's only by a small amount, when the exception propagates back to the context, some stuff has been freed already and we are not longer above the memory threshold Just delete these asserts --- src/smt/smt_context.cpp | 3 --- 1 file changed, 3 deletions(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 7895287ef..64c7bbf2e 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -3565,7 +3565,6 @@ namespace smt { try { internalize_assertions(); } catch (cancel_exception&) { - VERIFY(resource_limits_exceeded()); return l_undef; } expr_ref_vector theory_assumptions(m); @@ -3637,7 +3636,6 @@ namespace smt { TRACE("unsat_core_bug", tout << asms << '\n';); init_assumptions(asms); } catch (cancel_exception&) { - VERIFY(resource_limits_exceeded()); return l_undef; } TRACE("before_search", display(tout);); @@ -3664,7 +3662,6 @@ namespace smt { for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef; init_assumptions(asms); } catch (cancel_exception&) { - VERIFY(resource_limits_exceeded()); return l_undef; } for (auto const& clause : clauses) init_clause(clause);