mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-25 10:05:32 +00:00
Code Activity

fix #7629

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-04-23 15:22:44 -07:00
parent 7641393f8a
commit f6fbeda9d7
3 changed files with 7 additions and 7 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/smt/smt_context.cpp
View file

@ -3014,7 +3014,7 @@ namespace smt {
bool was_consistent = !inconsistent(); bool was_consistent = !inconsistent();
try { try {
internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope
} catch (cancel_exception&) { } catch (oom_exception&) {
throw default_exception("Resource limits hit in push"); throw default_exception("Resource limits hit in push");
} }
if (!m.inc()) if (!m.inc())
@ -3629,7 +3629,7 @@ namespace smt {
try { try {
internalize_assertions(); internalize_assertions();
} catch (cancel_exception&) { } catch (oom_exception&) {
return l_undef; return l_undef;
} }
expr_ref_vector theory_assumptions(m); expr_ref_vector theory_assumptions(m);
@ -3702,7 +3702,7 @@ namespace smt {
add_theory_assumptions(asms); add_theory_assumptions(asms);
TRACE("unsat_core_bug", tout << asms << '\n';); TRACE("unsat_core_bug", tout << asms << '\n';);
init_assumptions(asms); init_assumptions(asms);
} catch (cancel_exception&) { } catch (oom_exception&) {
return l_undef; return l_undef;
} }
TRACE("before_search", display(tout);); TRACE("before_search", display(tout););
@ -3729,7 +3729,7 @@ namespace smt {
// introducing proxies: if (!validate_assumptions(asms)) return l_undef; // introducing proxies: if (!validate_assumptions(asms)) return l_undef;
for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef; for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef;
init_assumptions(asms); init_assumptions(asms);
} catch (cancel_exception&) { } catch (oom_exception&) {
return l_undef; return l_undef;
} }
for (auto const& clause : clauses) init_clause(clause); for (auto const& clause : clauses) init_clause(clause);

4
src/smt/smt_context.h
View file

@ -63,8 +63,8 @@ namespace smt {
class model_generator; class model_generator;
class context; class context;
struct cancel_exception : public std::exception { struct oom_exception : public z3_error {
char const * what() const noexcept override { return "smt-canceled"; } oom_exception() : z3_error(ERR_MEMOUT) {}
}; };
struct enode_pp { struct enode_pp {

2
src/smt/smt_internalizer.cpp
View file

@ -354,7 +354,7 @@ namespace smt {
*/ */
void context::internalize(expr * n, bool gate_ctx) { void context::internalize(expr * n, bool gate_ctx) {
if (memory::above_high_watermark()) if (memory::above_high_watermark())
throw cancel_exception(); throw oom_exception();
internalize_deep(n); internalize_deep(n);
internalize_rec(n, gate_ctx); internalize_rec(n, gate_ctx);
} }