Corrected verdict of hard.c (from PR #808) and added its correct version

c/nla-digbench/hard.yml

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

c/nla-digbench/hard2.c

@@ -0,0 +1,55 @@
+/*
+  hardware integer division program, by Manna
+  returns q==A//B
+  */
+
+extern void __VERIFIER_error() __attribute__((__noreturn__));
+extern int __VERIFIER_nondet_int(void);
+extern void __VERIFIER_assume(int expression);
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        __VERIFIER_error();
+    }
+    return;
+}
+
+int main() {
+    int A, B;
+    int r, d, p, q;
+    A = __VERIFIER_nondet_int();
+    B = 1;
+
+    r = A;
+    d = B;
+    p = 1;
+    q = 0;
+
+    while (1) {
+        __VERIFIER_assert(q == 0);
+        __VERIFIER_assert(r == A);
+        __VERIFIER_assert(d == B * p);
+        if (!(r >= d)) break;
+
+        d = 2 * d;
+        p = 2 * p;
+    }
+
+    while (1) {
+        __VERIFIER_assert(A == q*B + r);
+        __VERIFIER_assert(d == B*p);
+
+        if (!(p != 1)) break;
+
+        d = d / 2;
+        p = p / 2;
+        if (r >= d) {
+            r = r - d;
+            q = q + p;
+        }
+    }
+
+    __VERIFIER_assert(A == d*q + r);
+    __VERIFIER_assert(B == d);    
+    return 0;
+}

c/nla-digbench/hard2.yml

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