sosy-lab/sv-benchmarks

Incorrectly labeled benchmarks in nla-digibench-scaling

mchalupa opened this issue · 4 comments

mchalupa commented

Benchmarks nla-digibench-scaling/divbin_unwindbound{10, 20, 50, 100}.yml should be labeled false(unreach-call), as witnessed by the following counterexamples:

diff --git a/c/nla-digbench-scaling/divbin_unwindbound10.i b/c/nla-digbench-scaling/divbin_un
windbound10.i
index 94a6bc46c8..4e182d9b65 100644
--- a/c/nla-digbench-scaling/divbin_unwindbound10.i
+++ b/c/nla-digbench-scaling/divbin_unwindbound10.i
@@ -26,8 +26,8 @@ int counter = 0;
 int main() {
   unsigned A, B;
   unsigned q, r, b;
-    A = __VERIFIER_nondet_unsigned_int();
-    B = __VERIFIER_nondet_unsigned_int();
+    A = 3968860678;
+    B = 1603972161;
     assume_abort_if_not(B < (0x7fffffff * 2U + 1U)/2);
     assume_abort_if_not(B >= 1);
     q = 0;
diff --git a/c/nla-digbench-scaling/divbin_unwindbound100.i b/c/nla-digbench-scaling/divbin_u
nwindbound100.i
index 09401c079a..565325f193 100644
--- a/c/nla-digbench-scaling/divbin_unwindbound100.i
+++ b/c/nla-digbench-scaling/divbin_unwindbound100.i
@@ -26,8 +26,8 @@ int counter = 0;
 int main() {
   unsigned A, B;
   unsigned q, r, b;
-    A = __VERIFIER_nondet_unsigned_int();
-    B = __VERIFIER_nondet_unsigned_int();
+    A = 3489603569;
+    B = 1541052197;
     assume_abort_if_not(B < (0x7fffffff * 2U + 1U)/2);
     assume_abort_if_not(B >= 1);
     q = 0;
diff --git a/c/nla-digbench-scaling/divbin_unwindbound20.i b/c/nla-digbench-scaling/divbin_unwindbound20.i
index 24c7026b34..b37e70cbc3 100644
--- a/c/nla-digbench-scaling/divbin_unwindbound20.i
+++ b/c/nla-digbench-scaling/divbin_unwindbound20.i
@@ -26,8 +26,8 @@ int counter = 0;
 int main() {
   unsigned A, B;
   unsigned q, r, b;
-    A = __VERIFIER_nondet_unsigned_int();
-    B = __VERIFIER_nondet_unsigned_int();
+    A = 3352618105;
+    B = 1600823033;
     assume_abort_if_not(B < (0x7fffffff * 2U + 1U)/2);
     assume_abort_if_not(B >= 1);
    q = 0;
diff --git a/c/nla-digbench-scaling/divbin_unwindbound50.i b/c/nla-digbench-scaling/divbin_unwindbound50.i
index 4eafca2d84..8ebf02f558 100644
--- a/c/nla-digbench-scaling/divbin_unwindbound50.i
+++ b/c/nla-digbench-scaling/divbin_unwindbound50.i
@@ -26,8 +26,8 @@ int counter = 0;
 int main() {
   unsigned A, B;
   unsigned q, r, b;
-    A = __VERIFIER_nondet_unsigned_int();
-    B = __VERIFIER_nondet_unsigned_int();
+    A = 3267711591;
+    B = 1576931915;
     assume_abort_if_not(B < (0x7fffffff * 2U + 1U)/2);
     assume_abort_if_not(B >= 1);
     q = 0;
MartinSpiessl commented

I am pretty sure you are correct. I will prepare a PR with fixes for that today if time allows it.

mchalupa commented

If the fix is just to relabel the benchmarks, I can do that. But I am not sure how to proceed if you'd like to also add the fixed versions.

MartinSpiessl commented

The main obstacle here is to not just fix the verdict in the yml files, but actually make generate.py reflect the changed verdicts and generate the yml files accordingly. But here it was quite easy because we already hat a similar case, I just created the PR at #1242

I also checked your counterexamples and was able to confirm them.

mchalupa commented

The PR was merged, so I'm closing this issue.

  • 👍1