diff --git a/c/nla-digbench/bresenham-ll.c b/c/nla-digbench/bresenham-ll.c
new file mode 100644
index 00000000000..7108c158a73
--- /dev/null
+++ b/c/nla-digbench/bresenham-ll.c
@@ -0,0 +1,51 @@
+/*
+  Bresenham's line drawing algorithm 
+  from Srivastava et al.'s paper From Program Verification to Program Synthesis in POPL '10 
+*/
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "bresenham-ll.c", 7, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    int X, Y;
+    long long x, y, v, xy, yx;
+    X = __VERIFIER_nondet_int();
+    Y = __VERIFIER_nondet_int();
+    v = ((long long) 2 * Y) - X;         // cast required to avoid int overflow
+    y = 0;
+    x = 0;
+
+    while (1) {
+        yx = (long long) Y*x;
+        xy = (long long) X*y;
+	__VERIFIER_assert( 2*yx - 2*xy - X + (long long) 2*Y - v == 0);
+        if (!(x <= X))
+            break;
+        // out[x] = y
+
+        if (v < 0) {
+            v = v + (long long) 2 * Y;
+        } else {
+            v = v + 2 * ((long long) Y - X);
+            y++;
+        }
+        x++;
+    }
+    xy = (long long) x*y;
+    yx = (long long) Y*x;
+    __VERIFIER_assert(2*yx - 2*xy - X + (long long) 2*Y - v + 2*y == 0);
+
+    return 0;
+}
diff --git a/c/nla-digbench/bresenham-ll.yml b/c/nla-digbench/bresenham-ll.yml
new file mode 100644
index 00000000000..a2bf97a37d3
--- /dev/null
+++ b/c/nla-digbench/bresenham-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'bresenham-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/bresenham.yml b/c/nla-digbench/bresenham.yml
index ed4d3a814ff..dd5522e8bb4 100644
--- a/c/nla-digbench/bresenham.yml
+++ b/c/nla-digbench/bresenham.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'bresenham.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/cohencu-ll.c b/c/nla-digbench/cohencu-ll.c
new file mode 100644
index 00000000000..623e359436a
--- /dev/null
+++ b/c/nla-digbench/cohencu-ll.c
@@ -0,0 +1,55 @@
+/*
+Printing consecutive cubes, by Cohen
+http://www.cs.upc.edu/~erodri/webpage/polynomial_invariants/cohencu.htm
+*/
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "cohencu-ll.c", 8, "reach_error"); }
+extern unsigned short __VERIFIER_nondet_unsigned_short(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    short a;
+    long long n, x, y, z;
+    a = __VERIFIER_nondet_unsigned_short();
+
+    n = 0;
+    x = 0;
+    y = 1;
+    z = 6;
+
+    while (1) {
+        __VERIFIER_assert(z == 6 * n + 6);
+        __VERIFIER_assert(y == 3 * n * n + 3 * n + 1);
+        __VERIFIER_assert(x == n * n * n);
+	__VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
+	__VERIFIER_assert((z*z) - 12*y - 6*z + 12 == 0);
+        if (!(n <= a))
+            break;
+
+        n = n + 1;
+        x = x + y;
+        y = y + z;
+        z = z + 6;
+    }
+
+    __VERIFIER_assert(z == 6*n + 6);
+    __VERIFIER_assert(6*a*x - x*z + 12*x == 0);
+    __VERIFIER_assert(a*z - 6*a - 2*y + 2*z - 10 == 0);
+    __VERIFIER_assert(2*y*y - 3*x*z - 18*x - 10*y + 3*z - 10 == 0);
+    __VERIFIER_assert(z*z - 12*y - 6*z + 12 == 0);
+    __VERIFIER_assert(y*z - 18*x - 12*y + 2*z - 6 == 0);
+    
+    return 0;
+}
diff --git a/c/nla-digbench/cohencu-ll.yml b/c/nla-digbench/cohencu-ll.yml
new file mode 100644
index 00000000000..5937f3ab89c
--- /dev/null
+++ b/c/nla-digbench/cohencu-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'cohencu-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/cohencu.yml b/c/nla-digbench/cohencu.yml
index 53a4e4719c9..4c3fac08909 100644
--- a/c/nla-digbench/cohencu.yml
+++ b/c/nla-digbench/cohencu.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'cohencu.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/cohendiv-ll.c b/c/nla-digbench/cohendiv-ll.c
new file mode 100644
index 00000000000..110f0852196
--- /dev/null
+++ b/c/nla-digbench/cohendiv-ll.c
@@ -0,0 +1,64 @@
+/*
+  Cohen's integer division
+  returns x % y
+  http://www.cs.upc.edu/~erodri/webpage/polynomial_invariants/cohendiv.htm
+*/
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "cohendiv-ll.c", 8, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+	{reach_error();}
+    }
+    return;
+}
+
+int main() {
+    int x, y;
+    long long q, r, a, b;
+
+    x = __VERIFIER_nondet_int();
+    y = __VERIFIER_nondet_int();
+
+    assume_abort_if_not(y >= 1);
+
+    q = 0;
+    r = x;
+    a = 0;
+    b = 0;
+
+    while (1) {
+	__VERIFIER_assert(b == y*a);
+	__VERIFIER_assert(x == q*y + r);
+    
+	if (!(r >= y))
+	    break;
+	a = 1;
+	b = y;
+
+	while (1) {            
+	    __VERIFIER_assert(b == y*a);
+	    __VERIFIER_assert(x == q*y + r);
+	    __VERIFIER_assert(r >= 0);
+
+	    if (!(r >= 2 * b))
+		break;
+	    
+	    __VERIFIER_assert(r >= 2 * y * a);
+	    
+	    a = 2 * a;
+	    b = 2 * b;
+	}
+	r = r - b;
+	q = q + a;
+    }
+    
+    __VERIFIER_assert(x == q*y + r);
+    return 0;
+}
diff --git a/c/nla-digbench/cohendiv-ll.yml b/c/nla-digbench/cohendiv-ll.yml
new file mode 100644
index 00000000000..7e271fd0ac1
--- /dev/null
+++ b/c/nla-digbench/cohendiv-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'cohendiv-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/cohendiv.yml b/c/nla-digbench/cohendiv.yml
index a4a67993370..0b709cfa5a7 100644
--- a/c/nla-digbench/cohendiv.yml
+++ b/c/nla-digbench/cohendiv.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'cohendiv.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/dijkstra-u.c b/c/nla-digbench/dijkstra-u.c
new file mode 100644
index 00000000000..5d33e9ef06c
--- /dev/null
+++ b/c/nla-digbench/dijkstra-u.c
@@ -0,0 +1,60 @@
+/* Compute the floor of the square root, by Dijkstra */
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "dijkstra-u.c", 5, "reach_error"); }
+extern unsigned int __VERIFIER_nondet_unsigned_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    unsigned int n, p, q, r, h;
+
+    n = __VERIFIER_nondet_unsigned_int();
+    assume_abort_if_not(n < 4294967295 / 4);  // Avoid non-terminating loop
+
+    p = 0;
+    q = 1;
+    r = n;
+    h = 0;
+    while (1) {
+        if (!(q <= n))
+            break;
+
+        q = 4 * q;
+    }
+    //q == 4^n
+
+    while (1) {
+        __VERIFIER_assert(r < 2 * p + q);
+        __VERIFIER_assert(p*p + r*q == n*q);
+        __VERIFIER_assert(h * h * h - 12 * h * n * q + 16 * n * p * q - h * q * q - 4 * p * q * q + 12 * h * q * r - 16 * p * q * r == 0);
+        __VERIFIER_assert(h * h * n - 4 * h * n * p + 4 * (n * n) * q - n * q * q - h * h * r + 4 * h * p * r - 8 * n * q * r + q * q * r + 4 * q * r * r == 0);
+        __VERIFIER_assert(h * h * p - 4 * h * n * q + 4 * n * p * q - p * q * q + 4 * h * q * r - 4 * p * q * r == 0);
+        __VERIFIER_assert(p * p - n * q + q * r == 0);
+
+        if (!(q != 1))
+            break;
+
+        q = q / 4;
+        h = p + q;
+        p = p / 2;
+        if (r >= h) {
+            p = p + q;
+            r = r - h;
+        }
+    }
+    __VERIFIER_assert(h*h*h - 12*h*n + 16*n*p + 12*h*r - 16*p*r - h - 4*p == 0);
+    __VERIFIER_assert(p*p - n + r == 0);
+    __VERIFIER_assert(h*h*p - 4*h*n + 4*n*p + 4*h*r - 4*p*r - p == 0);
+    return 0;
+}
diff --git a/c/nla-digbench/dijkstra-u.yml b/c/nla-digbench/dijkstra-u.yml
new file mode 100644
index 00000000000..778f24281ea
--- /dev/null
+++ b/c/nla-digbench/dijkstra-u.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'dijkstra-u.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/dijkstra.yml b/c/nla-digbench/dijkstra.yml
index 951133962b8..8e5ca28c748 100644
--- a/c/nla-digbench/dijkstra.yml
+++ b/c/nla-digbench/dijkstra.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'dijkstra.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/egcd-ll.c b/c/nla-digbench/egcd-ll.c
new file mode 100644
index 00000000000..9de63719046
--- /dev/null
+++ b/c/nla-digbench/egcd-ll.c
@@ -0,0 +1,57 @@
+/* extended Euclid's algorithm */
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "egcd-ll.c", 4, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    long long a, b, p, q, r, s;
+    int x, y;
+    x = __VERIFIER_nondet_int();
+    y = __VERIFIER_nondet_int();
+    assume_abort_if_not(x >= 1);
+    assume_abort_if_not(y >= 1);
+
+    a = x;
+    b = y;
+    p = 1;
+    q = 0;
+    r = 0;
+    s = 1;
+
+    while (1) {
+        __VERIFIER_assert(1 == p * s - r * q);
+        __VERIFIER_assert(a == y * r + x * p);
+        __VERIFIER_assert(b == x * q + y * s);
+
+        if (!(a != b))
+            break;
+
+        if (a > b) {
+            a = a - b;
+            p = p - q;
+            r = r - s;
+        } else {
+            b = b - a;
+            q = q - p;
+            s = s - r;
+        }
+    }
+    
+    __VERIFIER_assert(a - b == 0);    
+    __VERIFIER_assert(p*x + r*y - b == 0);
+    __VERIFIER_assert(q*r - p*s + 1 == 0);
+    __VERIFIER_assert(q*x + s*y - b == 0);
+    return 0;
+}
diff --git a/c/nla-digbench/egcd-ll.yml b/c/nla-digbench/egcd-ll.yml
new file mode 100644
index 00000000000..ac23cec7601
--- /dev/null
+++ b/c/nla-digbench/egcd-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'egcd-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/egcd.yml b/c/nla-digbench/egcd.yml
index 18bcc4d1c14..f5578de8a87 100644
--- a/c/nla-digbench/egcd.yml
+++ b/c/nla-digbench/egcd.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'egcd.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/egcd2-ll.c b/c/nla-digbench/egcd2-ll.c
new file mode 100644
index 00000000000..e3272e21d3b
--- /dev/null
+++ b/c/nla-digbench/egcd2-ll.c
@@ -0,0 +1,72 @@
+/* extended Euclid's algorithm */
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "egcd2-ll.c", 4, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    int x, y;
+    long long a, b, p, q, r, s, c, k, xy, yy;
+    x = __VERIFIER_nondet_int();
+    y = __VERIFIER_nondet_int();
+    assume_abort_if_not(x >= 1);
+    assume_abort_if_not(y >= 1);
+
+    a = x;
+    b = y;
+    p = 1;
+    q = 0;
+    r = 0;
+    s = 1;
+    c = 0;
+    k = 0;
+    xy = (long long) x * y;
+    yy = (long long) y * y;
+    assume_abort_if_not(xy < 2147483647);
+    assume_abort_if_not(yy < 2147483647);
+
+    while (1) {
+        if (!(b != 0))
+            break;
+        c = a;
+        k = 0;
+
+        while (1) {
+            __VERIFIER_assert(a == k * b + c);
+            __VERIFIER_assert(a == y*r + x*p);
+            __VERIFIER_assert(b == x * q + y * s);
+	    __VERIFIER_assert(q*xy + s*yy - q*x - b*y - s*y + b == 0);
+            if (!(c >= b))
+                break;
+            c = c - b;
+            k = k + 1;
+        }
+
+        a = b;
+        b = c;
+
+        long long temp;
+        temp = p;
+        p = q;
+        q = temp - q * k;
+        temp = r;
+        r = s;
+        s = temp - s * k;
+    }
+    
+
+    __VERIFIER_assert(q*x + s*y == 0);
+    __VERIFIER_assert(p*x + r*y == a);
+    return a;
+}
diff --git a/c/nla-digbench/egcd2-ll.yml b/c/nla-digbench/egcd2-ll.yml
new file mode 100644
index 00000000000..6a1463a5dcd
--- /dev/null
+++ b/c/nla-digbench/egcd2-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'egcd2-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/egcd2.yml b/c/nla-digbench/egcd2.yml
index 265abc4b2d3..6fc43a5a26c 100644
--- a/c/nla-digbench/egcd2.yml
+++ b/c/nla-digbench/egcd2.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'egcd2.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/egcd3-ll.c b/c/nla-digbench/egcd3-ll.c
new file mode 100644
index 00000000000..e088e457b74
--- /dev/null
+++ b/c/nla-digbench/egcd3-ll.c
@@ -0,0 +1,74 @@
+/* extended Euclid's algorithm */
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "egcd3-ll.c", 4, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    int x, y;
+    long long a, b, p, q, r, s;
+    x = __VERIFIER_nondet_int();
+    y = __VERIFIER_nondet_int();
+    assume_abort_if_not(x >= 1);
+    assume_abort_if_not(y >= 1);
+
+    a = x;
+    b = y;
+    p = 1;
+    q = 0;
+    r = 0;
+    s = 1;
+
+    while (1) {
+        if (!(b != 0))
+            break;
+        long long c, k;
+        c = a;
+        k = 0;
+
+        while (1) {
+            if (!(c >= b))
+                break;
+            long long d, v;
+            d = 1;
+            v = b;
+
+            while (1) {
+                __VERIFIER_assert(a == y * r + x * p);
+                __VERIFIER_assert(b == x * q + y * s);
+                __VERIFIER_assert(a == k * b + c);
+                __VERIFIER_assert(v == b * d);
+
+                if (!(c >= 2 * v))
+                    break;
+                d = 2 * d;
+                v = 2 * v;
+            }
+            c = c - v;
+            k = k + d;
+        }
+
+        a = b;
+        b = c;
+        long long temp;
+        temp = p;
+        p = q;
+        q = temp - q * k;
+        temp = r;
+        r = s;
+        s = temp - s * k;
+    }
+    __VERIFIER_assert(p*x - q*x + r*y - s*y  == a);
+    return 0;
+}
diff --git a/c/nla-digbench/egcd3-ll.yml b/c/nla-digbench/egcd3-ll.yml
new file mode 100644
index 00000000000..fc3cf5825cb
--- /dev/null
+++ b/c/nla-digbench/egcd3-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'egcd3-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/egcd3.yml b/c/nla-digbench/egcd3.yml
index 1a52ecd457c..9868651a03b 100644
--- a/c/nla-digbench/egcd3.yml
+++ b/c/nla-digbench/egcd3.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'egcd3.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/fermat1-ll.c b/c/nla-digbench/fermat1-ll.c
new file mode 100644
index 00000000000..2d82b5c0e90
--- /dev/null
+++ b/c/nla-digbench/fermat1-ll.c
@@ -0,0 +1,57 @@
+/* program computing a divisor for factorisation, by Knuth 4.5.4 Alg C ? */
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "fermat1-ll.c", 5, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    int A, R;
+    long long u, v, r;
+    A = __VERIFIER_nondet_int();
+    R = __VERIFIER_nondet_int();
+    assume_abort_if_not((((long long) R - 1) * ((long long) R - 1)) < A);
+    //assume_abort_if_not(A <= R * R);
+    assume_abort_if_not(A % 2 == 1);
+
+    u = ((long long) 2 * R) + 1;
+    v = 1;
+    r = ((long long) R * R) - A;
+
+
+    while (1) {
+        __VERIFIER_assert(4*(A+r) == u*u - v*v - 2*u + 2*v);
+        if (!(r != 0))
+            break;
+
+        while (1) {
+	    __VERIFIER_assert(4*(A+r) == u*u - v*v - 2*u + 2*v);
+            if (!(r > 0))
+                break;
+            r = r - v;
+            v = v + 2;
+        }
+
+        while (1) {
+	    __VERIFIER_assert(4*(A+r) == u*u - v*v - 2*u + 2*v);
+            if (!(r < 0))
+                break;
+            r = r + u;
+            u = u + 2;
+        }
+    }
+
+    __VERIFIER_assert(((long long) 4*A) == u*u - v*v - 2*u + 2*v);
+    return 0;
+}
diff --git a/c/nla-digbench/fermat1-ll.yml b/c/nla-digbench/fermat1-ll.yml
new file mode 100644
index 00000000000..f451035aa04
--- /dev/null
+++ b/c/nla-digbench/fermat1-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'fermat1-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/fermat1.yml b/c/nla-digbench/fermat1.yml
index 3365be06fa0..c2e26a62d21 100644
--- a/c/nla-digbench/fermat1.yml
+++ b/c/nla-digbench/fermat1.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'fermat1.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/fermat2-ll.c b/c/nla-digbench/fermat2-ll.c
new file mode 100644
index 00000000000..07a885afab6
--- /dev/null
+++ b/c/nla-digbench/fermat2-ll.c
@@ -0,0 +1,49 @@
+/* program computing a divisor for factorisation, by Bressoud */
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "fermat2-ll.c", 5, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    int A, R;
+    long long u, v, r;
+    A = __VERIFIER_nondet_int();
+    R = __VERIFIER_nondet_int();
+    //assume_abort_if_not(A >= 1);
+    assume_abort_if_not(((long long) R - 1) * ((long long) R - 1) < A);
+    //assume_abort_if_not(A <= R * R);
+    assume_abort_if_not(A % 2 == 1);
+
+    u = ((long long) 2 * R) + 1;
+    v = 1;
+    r = ((long long) R * R) - A;
+
+    while (1) {
+        __VERIFIER_assert(4*(A+r) == u*u - v*v - 2*u + 2*v);
+        if (!(r != 0)) break;
+
+        if (r > 0) {
+            r = r - v;
+            v = v + 2;
+        } else {
+            r = r + u;
+            u = u + 2;
+        }
+    }
+
+    //return  (u - v) / 2;
+    __VERIFIER_assert(((long long) 4*A) == u*u - v*v  - 2*u + 2*v);
+    return 0;
+}
diff --git a/c/nla-digbench/fermat2-ll.yml b/c/nla-digbench/fermat2-ll.yml
new file mode 100644
index 00000000000..4a5b30c29c1
--- /dev/null
+++ b/c/nla-digbench/fermat2-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'fermat2-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/fermat2.yml b/c/nla-digbench/fermat2.yml
index bbddbec72f0..17aeec39da4 100644
--- a/c/nla-digbench/fermat2.yml
+++ b/c/nla-digbench/fermat2.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'fermat2.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/geo1-ll.c b/c/nla-digbench/geo1-ll.c
new file mode 100644
index 00000000000..62b8ee2c4df
--- /dev/null
+++ b/c/nla-digbench/geo1-ll.c
@@ -0,0 +1,50 @@
+/* 
+Geometric Series
+computes x=(z-1)* sum(z^k)[k=0..k-1] , y = z^k
+returns 1+x-y == 0
+*/
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "geo1-ll.c", 9, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+int main() {
+    int z, k;
+    long long x, y, c;
+    z = __VERIFIER_nondet_int();
+    k = __VERIFIER_nondet_int();
+    assume_abort_if_not(z >= 1);
+    assume_abort_if_not(k >= 1);
+
+    x = 1;
+    y = z;
+    c = 1;
+
+    while (1) {
+        __VERIFIER_assert(x*z - x - y + 1 == 0);
+
+        if (!(c < k)) 
+            break;
+
+        c = c + 1;
+        x = x * z + 1;
+        y = y * z;
+
+    }  //geo1
+
+    x = x * (z - 1);
+
+    __VERIFIER_assert(1 + x - y == 0);
+    return 0;
+}
diff --git a/c/nla-digbench/geo1-ll.yml b/c/nla-digbench/geo1-ll.yml
new file mode 100644
index 00000000000..5c5520205e7
--- /dev/null
+++ b/c/nla-digbench/geo1-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'geo1-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/geo1-u.c b/c/nla-digbench/geo1-u.c
new file mode 100644
index 00000000000..e2d149d8ba3
--- /dev/null
+++ b/c/nla-digbench/geo1-u.c
@@ -0,0 +1,48 @@
+/* 
+Geometric Series
+computes x=(z-1)* sum(z^k)[k=0..k-1] , y = z^k
+returns 1+x-y == 0
+*/
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "geo1-u.c", 9, "reach_error"); }
+extern unsigned int __VERIFIER_nondet_unsigned_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+int main() {
+    unsigned int z, k;
+    long long x, y, c;
+    z = __VERIFIER_nondet_unsigned_int();
+    k = __VERIFIER_nondet_unsigned_int();
+
+    x = 1;
+    y = z;
+    c = 1;
+
+    while (1) {
+        __VERIFIER_assert(x*z - x - y + 1 == 0);
+
+        if (!(c < k)) 
+            break;
+
+        c = c + 1;
+        x = x * z + 1;
+        y = y * z;
+
+    }  //geo1
+
+    x = x * (z - 1);
+
+    __VERIFIER_assert(1 + x - y == 0);
+    return 0;
+}
diff --git a/c/nla-digbench/geo1-u.yml b/c/nla-digbench/geo1-u.yml
new file mode 100644
index 00000000000..fc62c91788f
--- /dev/null
+++ b/c/nla-digbench/geo1-u.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'geo1-u.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/geo1.yml b/c/nla-digbench/geo1.yml
index e119b72cf38..ab3cbff53de 100644
--- a/c/nla-digbench/geo1.yml
+++ b/c/nla-digbench/geo1.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'geo1.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/geo2-ll.c b/c/nla-digbench/geo2-ll.c
new file mode 100644
index 00000000000..7a963e0219a
--- /dev/null
+++ b/c/nla-digbench/geo2-ll.c
@@ -0,0 +1,45 @@
+/* 
+Geometric Series
+computes x = sum(z^k)[k=0..k-1], y = z^(k-1)
+*/
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "geo2-ll.c", 8, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+
+int main() {
+    int z, k;
+    long long x, y, c;
+    z = __VERIFIER_nondet_int();
+    k = __VERIFIER_nondet_int();
+
+    x = 1;
+    y = 1;
+    c = 1;
+
+    while (1) {
+        __VERIFIER_assert(1 + x*z - x - z*y == 0);
+
+        if (!(c < k))
+            break;
+
+        c = c + 1;
+        x = x * z + 1;
+        y = y * z;
+    }
+    __VERIFIER_assert(1 + x*z - x - z*y == 0);
+    return 0;
+}
diff --git a/c/nla-digbench/geo2-ll.yml b/c/nla-digbench/geo2-ll.yml
new file mode 100644
index 00000000000..1277dcf74b5
--- /dev/null
+++ b/c/nla-digbench/geo2-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'geo2-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/geo2.yml b/c/nla-digbench/geo2.yml
index f7f4ee45019..0c410dd951f 100644
--- a/c/nla-digbench/geo2.yml
+++ b/c/nla-digbench/geo2.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'geo2.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/geo3-ll.c b/c/nla-digbench/geo3-ll.c
new file mode 100644
index 00000000000..ca3e329c107
--- /dev/null
+++ b/c/nla-digbench/geo3-ll.c
@@ -0,0 +1,45 @@
+/* 
+Geometric Series
+computes x = sum(z^k)[k=0..k-1], y = z^(k-1)
+*/
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "geo3-ll.c", 8, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+int main() {
+    int z, a, k;
+    long long x, y, c, az;
+    z = __VERIFIER_nondet_int();
+    a = __VERIFIER_nondet_int();
+    k = __VERIFIER_nondet_int();
+
+    x = a;
+    y = 1;
+    c = 1;
+    az = (long long) a * z;
+
+    while (1) {
+        __VERIFIER_assert(z*x - x + a - az*y == 0);
+
+        if (!(c < k))
+            break;
+
+        c = c + 1;
+        x = x * z + a;
+        y = y * z;
+    }
+    __VERIFIER_assert(z*x - x + a - az*y == 0);
+    return x;
+}
diff --git a/c/nla-digbench/geo3-ll.yml b/c/nla-digbench/geo3-ll.yml
new file mode 100644
index 00000000000..b7a86adee0d
--- /dev/null
+++ b/c/nla-digbench/geo3-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'geo3-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/geo3.yml b/c/nla-digbench/geo3.yml
index f8ffbb56ba1..4eeec717a03 100644
--- a/c/nla-digbench/geo3.yml
+++ b/c/nla-digbench/geo3.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'geo3.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/hard-ll.c b/c/nla-digbench/hard-ll.c
new file mode 100644
index 00000000000..0dd595f03da
--- /dev/null
+++ b/c/nla-digbench/hard-ll.c
@@ -0,0 +1,61 @@
+/*
+  hardware integer division program, by Manna
+  returns q==A//B
+  */
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "hard-ll.c", 8, "reach_error"); }
+extern unsigned int __VERIFIER_nondet_unsigned_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    unsigned int A, B;
+    long long r, d, p, q;
+    A = __VERIFIER_nondet_unsigned_int();
+    B = __VERIFIER_nondet_unsigned_int();
+    assume_abort_if_not(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;
+}
diff --git a/c/nla-digbench/hard-ll.yml b/c/nla-digbench/hard-ll.yml
new file mode 100644
index 00000000000..1bded078120
--- /dev/null
+++ b/c/nla-digbench/hard-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'hard-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/hard-u.c b/c/nla-digbench/hard-u.c
new file mode 100644
index 00000000000..31e531ed123
--- /dev/null
+++ b/c/nla-digbench/hard-u.c
@@ -0,0 +1,61 @@
+/*
+  hardware integer division program, by Manna
+  returns q==A//B
+  */
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "hard-u.c", 8, "reach_error"); }
+extern unsigned int __VERIFIER_nondet_unsigned_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    unsigned int A, B;
+    unsigned int r, d, p, q;
+    A = __VERIFIER_nondet_unsigned_int();
+    B = __VERIFIER_nondet_unsigned_int();
+    assume_abort_if_not(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;
+}
diff --git a/c/nla-digbench/hard-u.yml b/c/nla-digbench/hard-u.yml
new file mode 100644
index 00000000000..704f90967ec
--- /dev/null
+++ b/c/nla-digbench/hard-u.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'hard-u.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: false
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/hard.yml b/c/nla-digbench/hard.yml
index 7af422fa256..568f9cf1a60 100644
--- a/c/nla-digbench/hard.yml
+++ b/c/nla-digbench/hard.yml
@@ -1,7 +1,7 @@
 format_version: '2.0'
 input_files: 'hard.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
+  - property_file: ../properties/no-overflow.prp
     expected_verdict: false
 
 options:
diff --git a/c/nla-digbench/hard2.yml b/c/nla-digbench/hard2.yml
index 1ed3d1961cd..4c0304aeb4e 100644
--- a/c/nla-digbench/hard2.yml
+++ b/c/nla-digbench/hard2.yml
@@ -3,6 +3,8 @@ input_files: 'hard2.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
 
 options:
   language: C
diff --git a/c/nla-digbench/lcm2.c b/c/nla-digbench/lcm2.c
index 4c5648107a3..dc3551bfc18 100644
--- a/c/nla-digbench/lcm2.c
+++ b/c/nla-digbench/lcm2.c
@@ -17,8 +17,8 @@ void __VERIFIER_assert(int cond) {
 }
 
 int main() {
-    int a, b;
-    int x, y, u, v;
+    unsigned a, b;
+    unsigned x, y, u, v;
     a = __VERIFIER_nondet_unsigned_int();
     b = __VERIFIER_nondet_unsigned_int();
     assume_abort_if_not(a >= 1); //inf loop if remove
diff --git a/c/nla-digbench/prod4br-ll.c b/c/nla-digbench/prod4br-ll.c
new file mode 100644
index 00000000000..5e43c546c4b
--- /dev/null
+++ b/c/nla-digbench/prod4br-ll.c
@@ -0,0 +1,58 @@
+/* algorithm for computing the product of two natural numbers */
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "prod4br-ll.c", 5, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    int x, y;
+    long long a, b, p, q;
+
+    x = __VERIFIER_nondet_int();
+    y = __VERIFIER_nondet_int();
+    assume_abort_if_not(y >= 1);
+
+    a = x;
+    b = y;
+    p = 1;
+    q = 0;
+
+    while (1) {
+        __VERIFIER_assert(q + a * b * p == (long long) x * y);
+
+        if (!(a != 0 && b != 0))
+            break;
+
+        if (a % 2 == 0 && b % 2 == 0) {
+            a = a / 2;
+            b = b / 2;
+            p = 4 * p;
+        } else if (a % 2 == 1 && b % 2 == 0) {
+            a = a - 1;
+            q = q + b * p;
+        } else if (a % 2 == 0 && b % 2 == 1) {
+            b = b - 1;
+            q = q + a * p;
+        } else {
+            a = a - 1;
+            b = b - 1;
+            q = q + (a + b + 1) * p; /*fix a bug here---  was (a+b-1)*/
+        }
+    }
+
+    __VERIFIER_assert(q == (long long) x * y);
+    __VERIFIER_assert(a * b == 0);
+    return 0;
+}
diff --git a/c/nla-digbench/prod4br-ll.yml b/c/nla-digbench/prod4br-ll.yml
new file mode 100644
index 00000000000..c3781acdc76
--- /dev/null
+++ b/c/nla-digbench/prod4br-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'prod4br-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/prod4br.yml b/c/nla-digbench/prod4br.yml
index 840fb4b6725..a3db754a030 100644
--- a/c/nla-digbench/prod4br.yml
+++ b/c/nla-digbench/prod4br.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'prod4br.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/prodbin-ll.c b/c/nla-digbench/prodbin-ll.c
new file mode 100644
index 00000000000..0c5bec51376
--- /dev/null
+++ b/c/nla-digbench/prodbin-ll.c
@@ -0,0 +1,47 @@
+/* shift_add algorithm for computing the 
+   product of two natural numbers
+*/
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "prodbin-ll.c", 6, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    int a, b;
+    long long x, y, z;
+
+    a = __VERIFIER_nondet_int();
+    b = __VERIFIER_nondet_int();
+    assume_abort_if_not(b >= 1);
+
+    x = a;
+    y = b;
+    z = 0;
+
+    while (1) {
+        __VERIFIER_assert(z + x * y == (long long) a * b);
+        if (!(y != 0))
+            break;
+
+        if (y % 2 == 1) {
+            z = z + x;
+            y = y - 1;
+        }
+        x = 2 * x;
+        y = y / 2;
+    }
+    __VERIFIER_assert(z == (long long) a * b);
+    
+    return 0;
+}
diff --git a/c/nla-digbench/prodbin-ll.yml b/c/nla-digbench/prodbin-ll.yml
new file mode 100644
index 00000000000..0686f09e39b
--- /dev/null
+++ b/c/nla-digbench/prodbin-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'prodbin-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/prodbin.yml b/c/nla-digbench/prodbin.yml
index 124c5be0713..76e2f526374 100644
--- a/c/nla-digbench/prodbin.yml
+++ b/c/nla-digbench/prodbin.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'prodbin.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/ps2-ll.c b/c/nla-digbench/ps2-ll.c
new file mode 100644
index 00000000000..3cbcc0d0f8b
--- /dev/null
+++ b/c/nla-digbench/ps2-ll.c
@@ -0,0 +1,39 @@
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "ps2-ll.c", 3, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    int k;
+    long long y, x, c;
+    k = __VERIFIER_nondet_int();
+
+    y = 0;
+    x = 0;
+    c = 0;
+
+    while (1) {
+        __VERIFIER_assert((y * y) - 2 * x + y == 0);
+
+        if (!(c < k))
+            break;
+
+        c = c + 1;
+        y = y + 1;
+        x = y + x;
+    }
+    __VERIFIER_assert((y*y) - 2*x + y == 0);
+     
+    return 0;
+}
diff --git a/c/nla-digbench/ps2-ll.yml b/c/nla-digbench/ps2-ll.yml
new file mode 100644
index 00000000000..31ca22eefe8
--- /dev/null
+++ b/c/nla-digbench/ps2-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'ps2-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/ps2.yml b/c/nla-digbench/ps2.yml
index 70275d41670..03057a69d55 100644
--- a/c/nla-digbench/ps2.yml
+++ b/c/nla-digbench/ps2.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'ps2.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/ps3-ll.c b/c/nla-digbench/ps3-ll.c
new file mode 100644
index 00000000000..52bd1d559c0
--- /dev/null
+++ b/c/nla-digbench/ps3-ll.c
@@ -0,0 +1,38 @@
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "ps3-ll.c", 3, "reach_error"); }
+extern short __VERIFIER_nondet_short(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    short k; 
+    long long y, x, c;
+    k = __VERIFIER_nondet_short();
+
+    y = 0;
+    x = 0;
+    c = 0;
+
+    while (1) {
+        __VERIFIER_assert(6*x - 2*y*y*y - 3*y*y - y == 0);
+
+        if (!(c < k))
+            break;
+
+        c = c + 1;
+        y = y + 1;
+        x = y * y + x;
+    }
+    __VERIFIER_assert(6*x - 2*y*y*y - 3*y*y - y == 0);
+    return 0;
+}
diff --git a/c/nla-digbench/ps3-ll.yml b/c/nla-digbench/ps3-ll.yml
new file mode 100644
index 00000000000..ac387de01f9
--- /dev/null
+++ b/c/nla-digbench/ps3-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'ps3-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/ps3.yml b/c/nla-digbench/ps3.yml
index 30c3d28096e..0a7d6b5a4f0 100644
--- a/c/nla-digbench/ps3.yml
+++ b/c/nla-digbench/ps3.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'ps3.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/ps4-ll.c b/c/nla-digbench/ps4-ll.c
new file mode 100644
index 00000000000..a71b4cec4cf
--- /dev/null
+++ b/c/nla-digbench/ps4-ll.c
@@ -0,0 +1,39 @@
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "ps4-ll.c", 3, "reach_error"); }
+extern short __VERIFIER_nondet_short(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    short k;
+    long long y, x, c;
+    k = __VERIFIER_nondet_short();
+
+    y = 0;
+    x = 0;
+    c = 0;
+
+    while (1) {
+        __VERIFIER_assert(4*x - y*y*y*y - 2*y*y*y - y*y == 0);
+
+        if (!(c < k))
+            break;
+
+        c = c + 1;
+        y = y + 1;
+        x = y * y * y + x;
+    }
+    __VERIFIER_assert(k*y - (y*y) == 0);
+    __VERIFIER_assert(4*x - y*y*y*y - 2*y*y*y - y*y == 0);
+    return 0;
+}
diff --git a/c/nla-digbench/ps4-ll.yml b/c/nla-digbench/ps4-ll.yml
new file mode 100644
index 00000000000..bd9556eebc7
--- /dev/null
+++ b/c/nla-digbench/ps4-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'ps4-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/ps4.yml b/c/nla-digbench/ps4.yml
index b518783fc7a..d251e7a1547 100644
--- a/c/nla-digbench/ps4.yml
+++ b/c/nla-digbench/ps4.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'ps4.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/ps5-ll.c b/c/nla-digbench/ps5-ll.c
new file mode 100644
index 00000000000..9d604368183
--- /dev/null
+++ b/c/nla-digbench/ps5-ll.c
@@ -0,0 +1,41 @@
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "ps5-ll.c", 3, "reach_error"); }
+extern short __VERIFIER_nondet_short(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    short k;
+    long long y, x, c;
+    k = __VERIFIER_nondet_short();
+    assume_abort_if_not(k <= 256);
+
+    y = 0;
+    x = 0;
+    c = 0;
+
+    while (1) {
+        __VERIFIER_assert(6*y*y*y*y*y + 15*y*y*y*y + 10*y*y*y - 30*x - y == 0);
+
+        if (!(c < k))
+            break;
+
+        c = c + 1;
+        y = y + 1;
+        x = y * y * y * y + x;
+    }
+
+    __VERIFIER_assert(6*y*y*y*y*y + 15*y*y*y*y + 10*y*y*y - 30*x - y == 0);
+    __VERIFIER_assert(k*y == y*y);
+    return 0;
+}
diff --git a/c/nla-digbench/ps5-ll.yml b/c/nla-digbench/ps5-ll.yml
new file mode 100644
index 00000000000..3ad67457758
--- /dev/null
+++ b/c/nla-digbench/ps5-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'ps5-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/ps5.yml b/c/nla-digbench/ps5.yml
index 3f3fba0c436..45efccf7eb2 100644
--- a/c/nla-digbench/ps5.yml
+++ b/c/nla-digbench/ps5.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'ps5.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/ps6-ll.c b/c/nla-digbench/ps6-ll.c
new file mode 100644
index 00000000000..836939ce507
--- /dev/null
+++ b/c/nla-digbench/ps6-ll.c
@@ -0,0 +1,41 @@
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "ps6-ll.c", 3, "reach_error"); }
+extern short __VERIFIER_nondet_short(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+int main() {
+    short k;
+    long long y, x, c;
+    k = __VERIFIER_nondet_short();
+    assume_abort_if_not(k <= 256);
+
+    y = 0;
+    x = 0;
+    c = 0;
+
+    while (1) {
+        __VERIFIER_assert(-2*y*y*y*y*y*y - 6 * y*y*y*y*y - 5 * y*y*y*y + y*y + 12*x == 0);
+
+        if (!(c < k))
+            break;
+
+        c = c + 1;
+        y = y + 1;
+        x = y * y * y * y * y + x;
+    }
+    
+    __VERIFIER_assert(-2*y*y*y*y*y*y - 6 * y*y*y*y*y - 5 * y*y*y*y + y*y + 12*x == 0);
+    __VERIFIER_assert(k*y == y*y);		      
+    return 0;
+}
diff --git a/c/nla-digbench/ps6-ll.yml b/c/nla-digbench/ps6-ll.yml
new file mode 100644
index 00000000000..804b4a71d97
--- /dev/null
+++ b/c/nla-digbench/ps6-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'ps6-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/ps6.yml b/c/nla-digbench/ps6.yml
index 919e9a9503d..9873d932c94 100644
--- a/c/nla-digbench/ps6.yml
+++ b/c/nla-digbench/ps6.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'ps6.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C
diff --git a/c/nla-digbench/sqrt1-ll.c b/c/nla-digbench/sqrt1-ll.c
new file mode 100644
index 00000000000..79afa23974c
--- /dev/null
+++ b/c/nla-digbench/sqrt1-ll.c
@@ -0,0 +1,48 @@
+/* Compute the floor of the square root of a natural number */
+
+extern void abort(void);
+extern void __assert_fail(const char *, const char *, unsigned int, const char *) __attribute__ ((__nothrow__ , __leaf__)) __attribute__ ((__noreturn__));
+void reach_error() { __assert_fail("0", "sqrt1-ll.c", 5, "reach_error"); }
+extern int __VERIFIER_nondet_int(void);
+extern void abort(void);
+void assume_abort_if_not(int cond) {
+  if(!cond) {abort();}
+}
+void __VERIFIER_assert(int cond) {
+    if (!(cond)) {
+    ERROR:
+        {reach_error();}
+    }
+    return;
+}
+
+
+int main() {
+    int n;
+    long long a, s, t;
+    n = __VERIFIER_nondet_int();
+
+    a = 0;
+    s = 1;
+    t = 1;
+
+    while (1) {
+        __VERIFIER_assert(t == 2*a + 1);
+        __VERIFIER_assert(s == (a + 1) * (a + 1));
+	__VERIFIER_assert(t*t - 4*s + 2*t + 1 == 0);
+        // the above 2 should be equiv to 
+
+        if (!(s <= n))
+            break;
+
+        a = a + 1;
+        t = t + 2;
+        s = s + t;
+    }
+    
+    __VERIFIER_assert(t == 2 * a + 1);
+    __VERIFIER_assert(s == (a + 1) * (a + 1));
+    __VERIFIER_assert(t*t - 4*s + 2*t + 1 == 0);
+
+    return 0;
+}
diff --git a/c/nla-digbench/sqrt1-ll.yml b/c/nla-digbench/sqrt1-ll.yml
new file mode 100644
index 00000000000..34dc1aa13e5
--- /dev/null
+++ b/c/nla-digbench/sqrt1-ll.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'sqrt1-ll.c'
+properties:
+  - property_file: ../properties/unreach-call.prp
+    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: true
+
+options:
+  language: C
+  data_model: ILP32
diff --git a/c/nla-digbench/sqrt1.yml b/c/nla-digbench/sqrt1.yml
index 9cf54344055..926192d8553 100644
--- a/c/nla-digbench/sqrt1.yml
+++ b/c/nla-digbench/sqrt1.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
 input_files: 'sqrt1.c'
 properties:
-  - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+  - property_file: ../properties/no-overflow.prp
+    expected_verdict: false
 
 options:
   language: C