From e1e0813d0b9f4dcd214ef0dcd9ef1815854dc1e1 Mon Sep 17 00:00:00 2001 From: Simmo Saan Date: Fri, 20 Oct 2023 12:07:29 +0300 Subject: [PATCH] Use threshold widening in Freiburg nondet_inc_with_ghosts --- tests/regression/46-apron2/67-nondet_inc_with_ghosts.c | 4 ++-- tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c | 4 ++-- 2 files changed, 4 insertions(+), 4 deletions(-) diff --git a/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c b/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c index cfbab7f922..2fc073db05 100644 --- a/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c +++ b/tests/regression/46-apron2/67-nondet_inc_with_ghosts.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening #include #include @@ -19,7 +19,7 @@ void* inc() __VERIFIER_atomic_end(); __VERIFIER_atomic_begin(); - assert(x >= g); // TODO + assert(x >= g); __VERIFIER_atomic_end(); } diff --git a/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c b/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c index 3d41428a59..380821add9 100644 --- a/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c +++ b/tests/regression/46-apron2/68-nondet_inc_with_ghosts-2.c @@ -1,4 +1,4 @@ -// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none +// PARAM: --enable ana.sv-comp.functions --set ana.activated[+] apron --set ana.relation.privatization mutex-meet --set sem.int.signed_overflow assume_none --enable ana.apron.threshold_widening #include #include @@ -16,7 +16,7 @@ void* inc() __VERIFIER_atomic_end(); __VERIFIER_atomic_begin(); - assert(x >= g); // TODO + assert(x >= g); __VERIFIER_atomic_end(); return 0; }