mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-11-24 22:51:28 +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 7395152632
commit 662e4293a5
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>
void arith_base<num_t>::invariant() {
if (m.limit().is_canceled())
return;
for (unsigned v = 0; v < ctx.num_bool_vars(); ++v) {
auto ineq = get_ineq(v);
if (ineq)
@ -2620,10 +2622,10 @@ namespace sls {
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 (m.rlimit().is_canceled())
// return;
if (m.limit().is_canceled())
return;
report_error(verbose_stream(), v);
TRACE(arith, report_error(tout, v));
UNREACHABLE();