mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2026-05-02 16:43:45 +00:00
Code Activity

check cancelation in invariant checker

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2025-11-23 09:09:55 -08:00
parent 64439a8134
commit 9fcede1285
1 changed files with 5 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

8
src/ast/sls/sls_arith_base.cpp
View file

@ -2588,6 +2588,8 @@ namespace sls {
template<typename num_t> template<typename num_t>
void arith_base<num_t>::invariant() { void arith_base<num_t>::invariant() {
if (m.limit().is_canceled())
return;
for (unsigned v = 0; v < ctx.num_bool_vars(); ++v) { for (unsigned v = 0; v < ctx.num_bool_vars(); ++v) {
auto ineq = get_ineq(v); auto ineq = get_ineq(v);
if (ineq) if (ineq)
@ -2620,10 +2622,10 @@ namespace sls {
display(out, ad) << "\n"; display(out, ad) << "\n";
} }
}; };
for (var_t v = 0; v < m_vars.size(); ++v) { for (var_t v = 0; v < m_vars.size(); ++v) {
if (!eval_is_correct(v)) { if (!eval_is_correct(v)) {
// if (m.rlimit().is_canceled()) if (m.limit().is_canceled())
// return; return;
report_error(verbose_stream(), v); report_error(verbose_stream(), v);
TRACE(arith, report_error(tout, v)); TRACE(arith, report_error(tout, v));
UNREACHABLE(); UNREACHABLE();