Skip to content

Commit f6fbeda

Browse files
fix #7629
1 parent 7641393 commit f6fbeda

File tree

3 files changed

+7
-7
lines changed

3 files changed

+7
-7
lines changed

src/smt/smt_context.cpp

+4-4
Original file line numberDiff line numberDiff line change
@@ -3014,7 +3014,7 @@ namespace smt {
30143014
bool was_consistent = !inconsistent();
30153015
try {
30163016
internalize_assertions(); // internalize assertions before invoking m_asserted_formulas.push_scope
3017-
} catch (cancel_exception&) {
3017+
} catch (oom_exception&) {
30183018
throw default_exception("Resource limits hit in push");
30193019
}
30203020
if (!m.inc())
@@ -3629,7 +3629,7 @@ namespace smt {
36293629

36303630
try {
36313631
internalize_assertions();
3632-
} catch (cancel_exception&) {
3632+
} catch (oom_exception&) {
36333633
return l_undef;
36343634
}
36353635
expr_ref_vector theory_assumptions(m);
@@ -3702,7 +3702,7 @@ namespace smt {
37023702
add_theory_assumptions(asms);
37033703
TRACE("unsat_core_bug", tout << asms << '\n';);
37043704
init_assumptions(asms);
3705-
} catch (cancel_exception&) {
3705+
} catch (oom_exception&) {
37063706
return l_undef;
37073707
}
37083708
TRACE("before_search", display(tout););
@@ -3729,7 +3729,7 @@ namespace smt {
37293729
// introducing proxies: if (!validate_assumptions(asms)) return l_undef;
37303730
for (auto const& clause : clauses) if (!validate_assumptions(clause)) return l_undef;
37313731
init_assumptions(asms);
3732-
} catch (cancel_exception&) {
3732+
} catch (oom_exception&) {
37333733
return l_undef;
37343734
}
37353735
for (auto const& clause : clauses) init_clause(clause);

src/smt/smt_context.h

+2-2
Original file line numberDiff line numberDiff line change
@@ -63,8 +63,8 @@ namespace smt {
6363
class model_generator;
6464
class context;
6565

66-
struct cancel_exception : public std::exception {
67-
char const * what() const noexcept override { return "smt-canceled"; }
66+
struct oom_exception : public z3_error {
67+
oom_exception() : z3_error(ERR_MEMOUT) {}
6868
};
6969

7070
struct enode_pp {

src/smt/smt_internalizer.cpp

+1-1
Original file line numberDiff line numberDiff line change
@@ -354,7 +354,7 @@ namespace smt {
354354
*/
355355
void context::internalize(expr * n, bool gate_ctx) {
356356
if (memory::above_high_watermark())
357-
throw cancel_exception();
357+
throw oom_exception();
358358
internalize_deep(n);
359359
internalize_rec(n, gate_ctx);
360360
}

0 commit comments

Comments
 (0)