The assertion in the divbin program is violable hence changed the

verdict of the program. Also adding the corrected program divbin2 with
verifiable assertion.

c/nla-digbench/divbin.yml

@@ -2,4 +2,4 @@ format_version: '1.0'
 input_files: 'divbin.i'
 properties:
   - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+    expected_verdict: false

c/nla-digbench/divbin2.c

@@ -0,0 +1,48 @@
+/*
+  A division algorithm, by Kaldewaij
+  returns A//B
+*/
+
+#include <limits.h>
+
+extern void __VERIFIER_error() __attribute__((__noreturn__));
+extern unsigned __VERIFIER_nondet_unsigned_int(void);
+extern void __VERIFIER_assume(int expression);
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        __VERIFIER_error();
+    }
+    return;
+}
+
+int main() {
+  unsigned A, B;
+  unsigned q, r, b;
+    A = __VERIFIER_nondet_unsigned_int();
+    B = 1;
+
+    q = 0;
+    r = A;
+    b = B;
+
+    while (1) {
+        if (!(r >= b)) break;
+        b = 2 * b;
+    }
+
+    while (1) {
+        __VERIFIER_assert(A == q * b + r);
+        if (!(b != B)) break;
+
+        q = 2 * q;
+        b = b / 2;
+        if (r >= b) {
+            q = q + 1;
+            r = r - b;
+        }
+    }
+
+    __VERIFIER_assert(A == q * b + r);
+    return 0;
+}

c/nla-digbench/divbin2.i

@@ -0,0 +1,35 @@
+extern void __VERIFIER_error() __attribute__((__noreturn__));
+extern unsigned __VERIFIER_nondet_unsigned_int(void);
+extern void __VERIFIER_assume(int expression);
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        __VERIFIER_error();
+    }
+    return;
+}
+int main() {
+  unsigned A, B;
+  unsigned q, r, b;
+    A = __VERIFIER_nondet_unsigned_int();
+    B = 1;
+    q = 0;
+    r = A;
+    b = B;
+    while (1) {
+        if (!(r >= b)) break;
+        b = 2 * b;
+    }
+    while (1) {
+        __VERIFIER_assert(A == q * b + r);
+        if (!(b != B)) break;
+        q = 2 * q;
+        b = b / 2;
+        if (r >= b) {
+            q = q + 1;
+            r = r - b;
+        }
+    }
+    __VERIFIER_assert(A == q * b + r);
+    return 0;
+}

c/nla-digbench/divbin2.yml

@@ -0,0 +1,5 @@
+format_version: '1.0'
+input_files: 'divbin2.i'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true