From b10e87cbb22eaa0b248dde0381b367de79ae011b Mon Sep 17 00:00:00 2001
From: divyesh <divyesh@cse.iitb.ac.in>
Date: Mon, 5 Oct 2020 10:25:26 +0530
Subject: [PATCH 01/13] Only overflow check for hard.c and a new benchmark with
 unsigned integers

---
 c/nla-digbench/hard.yml  |  2 +-
 c/nla-digbench/hardu.c   | 61 ++++++++++++++++++++++++++++++++++++++++
 c/nla-digbench/hardu.yml | 11 ++++++++
 3 files changed, 73 insertions(+), 1 deletion(-)
 create mode 100644 c/nla-digbench/hardu.c
 create mode 100644 c/nla-digbench/hardu.yml

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/hardu.c b/c/nla-digbench/hardu.c
new file mode 100644
index 00000000000..4f1e6215d70
--- /dev/null
+++ b/c/nla-digbench/hardu.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.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/hardu.yml b/c/nla-digbench/hardu.yml
new file mode 100644
index 00000000000..95848be8917
--- /dev/null
+++ b/c/nla-digbench/hardu.yml
@@ -0,0 +1,11 @@
+format_version: '2.0'
+input_files: 'hardu.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

From 21cbb7d43ad2307f2ef67f649a6dbfd7d1eb83b0 Mon Sep 17 00:00:00 2001
From: Divyesh Unadkat <divyeshunadkat@users.noreply.github.com>
Date: Mon, 5 Oct 2020 10:33:56 +0530
Subject: [PATCH 02/13] Update hard.yml

The program has an overflow so the verdict should be true.
---
 c/nla-digbench/hard.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/c/nla-digbench/hard.yml b/c/nla-digbench/hard.yml
index 568f9cf1a60..c8d6e4431e7 100644
--- a/c/nla-digbench/hard.yml
+++ b/c/nla-digbench/hard.yml
@@ -2,7 +2,7 @@ format_version: '2.0'
 input_files: 'hard.c'
 properties:
   - property_file: ../properties/no-overflow.prp
-    expected_verdict: false
+    expected_verdict: true
 
 options:
   language: C

From fbebf3c80fac991a330595d7965f3737d59b53d9 Mon Sep 17 00:00:00 2001
From: divyesh <divyesh@cse.iitb.ac.in>
Date: Wed, 7 Oct 2020 15:49:59 +0530
Subject: [PATCH 03/13] Revert "Update hard.yml"

This reverts commit 21cbb7d43ad2307f2ef67f649a6dbfd7d1eb83b0.
---
 c/nla-digbench/hard.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/c/nla-digbench/hard.yml b/c/nla-digbench/hard.yml
index c8d6e4431e7..568f9cf1a60 100644
--- a/c/nla-digbench/hard.yml
+++ b/c/nla-digbench/hard.yml
@@ -2,7 +2,7 @@ format_version: '2.0'
 input_files: 'hard.c'
 properties:
   - property_file: ../properties/no-overflow.prp
-    expected_verdict: true
+    expected_verdict: false
 
 options:
   language: C

From d0f58e66a0be8cd9dcf59fbe7a19bbd9443cc79f Mon Sep 17 00:00:00 2001
From: divyesh <divyesh@cse.iitb.ac.in>
Date: Wed, 7 Oct 2020 16:46:45 +0530
Subject: [PATCH 04/13] corrected the file name in hardu.c

---
 c/nla-digbench/hardu.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/c/nla-digbench/hardu.c b/c/nla-digbench/hardu.c
index 4f1e6215d70..b02b866d828 100644
--- a/c/nla-digbench/hardu.c
+++ b/c/nla-digbench/hardu.c
@@ -5,7 +5,7 @@
 
 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.c", 8, "reach_error"); }
+void reach_error() { __assert_fail("0", "hardu.c", 8, "reach_error"); }
 extern unsigned int __VERIFIER_nondet_unsigned_int(void);
 extern void abort(void);
 void assume_abort_if_not(int cond) {

From b3fb86cdbd390223a4abc7034be407253a328dbb Mon Sep 17 00:00:00 2001
From: divyesh <divyesh@cse.iitb.ac.in>
Date: Sun, 11 Oct 2020 09:46:11 +0530
Subject: [PATCH 05/13] Attempt to fix the overflow

---
 c/nla-digbench/hardu.c | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/c/nla-digbench/hardu.c b/c/nla-digbench/hardu.c
index b02b866d828..91978fc6152 100644
--- a/c/nla-digbench/hardu.c
+++ b/c/nla-digbench/hardu.c
@@ -21,7 +21,7 @@ void __VERIFIER_assert(int cond) {
 
 int main() {
     unsigned int A, B;
-    unsigned int r, d, p, q;
+    unsigned long long r, d, p, q;
     A = __VERIFIER_nondet_unsigned_int();
     B = __VERIFIER_nondet_unsigned_int();
     assume_abort_if_not(B >= 1);

From 7b81d2a9f863f97d039f6d4c322b6a76ba751525 Mon Sep 17 00:00:00 2001
From: divyesh <divyesh@cse.iitb.ac.in>
Date: Sun, 11 Oct 2020 10:05:51 +0530
Subject: [PATCH 06/13] Resolving overflow issue makes the reachability
 property true

---
 c/nla-digbench/hardu.yml | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/c/nla-digbench/hardu.yml b/c/nla-digbench/hardu.yml
index 95848be8917..9f3df20a582 100644
--- a/c/nla-digbench/hardu.yml
+++ b/c/nla-digbench/hardu.yml
@@ -2,7 +2,7 @@ format_version: '2.0'
 input_files: 'hardu.c'
 properties:
   - property_file: ../properties/unreach-call.prp
-    expected_verdict: false
+    expected_verdict: true
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
 

From ba206d3466efb7472c3bbb88963824e6042e2da7 Mon Sep 17 00:00:00 2001
From: divyesh <divyesh@cse.iitb.ac.in>
Date: Wed, 14 Oct 2020 02:09:57 +0530
Subject: [PATCH 07/13] Renamed

---
 c/nla-digbench/{hardu.c => hard-u.c}     | 0
 c/nla-digbench/{hardu.yml => hard-u.yml} | 0
 2 files changed, 0 insertions(+), 0 deletions(-)
 rename c/nla-digbench/{hardu.c => hard-u.c} (100%)
 rename c/nla-digbench/{hardu.yml => hard-u.yml} (100%)

diff --git a/c/nla-digbench/hardu.c b/c/nla-digbench/hard-u.c
similarity index 100%
rename from c/nla-digbench/hardu.c
rename to c/nla-digbench/hard-u.c
diff --git a/c/nla-digbench/hardu.yml b/c/nla-digbench/hard-u.yml
similarity index 100%
rename from c/nla-digbench/hardu.yml
rename to c/nla-digbench/hard-u.yml

From bcd2451f787be721df8b7dd0e132414377d36425 Mon Sep 17 00:00:00 2001
From: divyesh <divyesh@cse.iitb.ac.in>
Date: Wed, 14 Oct 2020 02:11:23 +0530
Subject: [PATCH 08/13] Changed the property from unreach to no-overflow
 Modifications in lcm2.c and hard-u.c

---
 c/nla-digbench/bresenham.yml | 4 ++--
 c/nla-digbench/cohencu.yml   | 4 ++--
 c/nla-digbench/cohendiv.yml  | 4 ++--
 c/nla-digbench/dijkstra.yml  | 4 ++--
 c/nla-digbench/egcd.yml      | 4 ++--
 c/nla-digbench/egcd2.yml     | 4 ++--
 c/nla-digbench/egcd3.yml     | 4 ++--
 c/nla-digbench/fermat1.yml   | 4 ++--
 c/nla-digbench/fermat2.yml   | 4 ++--
 c/nla-digbench/geo1.yml      | 4 ++--
 c/nla-digbench/geo2.yml      | 4 ++--
 c/nla-digbench/geo3.yml      | 4 ++--
 c/nla-digbench/hard-u.c      | 4 ++--
 c/nla-digbench/hard-u.yml    | 4 ++--
 c/nla-digbench/hard2.yml     | 2 ++
 c/nla-digbench/lcm2.c        | 4 ++--
 c/nla-digbench/prod4br.yml   | 4 ++--
 c/nla-digbench/prodbin.yml   | 4 ++--
 c/nla-digbench/ps2.yml       | 4 ++--
 c/nla-digbench/ps3.yml       | 4 ++--
 c/nla-digbench/ps4.yml       | 4 ++--
 c/nla-digbench/ps5.yml       | 4 ++--
 c/nla-digbench/ps6.yml       | 4 ++--
 c/nla-digbench/sqrt1.yml     | 4 ++--
 24 files changed, 48 insertions(+), 46 deletions(-)

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.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.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.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.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.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.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.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.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.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.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.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-u.c b/c/nla-digbench/hard-u.c
index 91978fc6152..31e531ed123 100644
--- a/c/nla-digbench/hard-u.c
+++ b/c/nla-digbench/hard-u.c
@@ -5,7 +5,7 @@
 
 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", "hardu.c", 8, "reach_error"); }
+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) {
@@ -21,7 +21,7 @@ void __VERIFIER_assert(int cond) {
 
 int main() {
     unsigned int A, B;
-    unsigned long long r, d, p, q;
+    unsigned int r, d, p, q;
     A = __VERIFIER_nondet_unsigned_int();
     B = __VERIFIER_nondet_unsigned_int();
     assume_abort_if_not(B >= 1);
diff --git a/c/nla-digbench/hard-u.yml b/c/nla-digbench/hard-u.yml
index 9f3df20a582..704f90967ec 100644
--- a/c/nla-digbench/hard-u.yml
+++ b/c/nla-digbench/hard-u.yml
@@ -1,8 +1,8 @@
 format_version: '2.0'
-input_files: 'hardu.c'
+input_files: 'hard-u.c'
 properties:
   - property_file: ../properties/unreach-call.prp
-    expected_verdict: true
+    expected_verdict: false
   - property_file: ../properties/no-overflow.prp
     expected_verdict: true
 
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.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.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.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.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.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.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.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.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

From a36f931c1198eea38fb13c1a08e15c10c798dfa1 Mon Sep 17 00:00:00 2001
From: divyesh <divyesh@cse.iitb.ac.in>
Date: Wed, 14 Oct 2020 02:12:48 +0530
Subject: [PATCH 09/13] Benchmarks without overflows while retaining program
 complexity and unreach property

---
 c/nla-digbench/bresenham-ll.c   | 49 ++++++++++++++++++++++
 c/nla-digbench/bresenham-ll.yml | 11 +++++
 c/nla-digbench/cohencu-ll.c     | 55 ++++++++++++++++++++++++
 c/nla-digbench/cohencu-ll.yml   | 11 +++++
 c/nla-digbench/cohendiv-ll.c    | 64 ++++++++++++++++++++++++++++
 c/nla-digbench/cohendiv-ll.yml  | 11 +++++
 c/nla-digbench/dijkstra-u.c     | 60 ++++++++++++++++++++++++++
 c/nla-digbench/dijkstra-u.yml   | 11 +++++
 c/nla-digbench/egcd-ll.c        | 57 +++++++++++++++++++++++++
 c/nla-digbench/egcd-ll.yml      | 11 +++++
 c/nla-digbench/egcd2-ll.c       | 67 +++++++++++++++++++++++++++++
 c/nla-digbench/egcd2-ll.yml     | 11 +++++
 c/nla-digbench/egcd3-ll.c       | 74 +++++++++++++++++++++++++++++++++
 c/nla-digbench/egcd3-ll.yml     | 11 +++++
 c/nla-digbench/fermat1-ll.c     | 57 +++++++++++++++++++++++++
 c/nla-digbench/fermat1-ll.yml   | 11 +++++
 c/nla-digbench/fermat1-u.c      | 57 +++++++++++++++++++++++++
 c/nla-digbench/fermat2-ll.c     | 49 ++++++++++++++++++++++
 c/nla-digbench/fermat2-ll.yml   | 11 +++++
 c/nla-digbench/geo1-ll.c        | 50 ++++++++++++++++++++++
 c/nla-digbench/geo1-ll.yml      | 11 +++++
 c/nla-digbench/geo1-u.c         | 48 +++++++++++++++++++++
 c/nla-digbench/geo1-u.yml       | 11 +++++
 c/nla-digbench/geo2-ll.c        | 45 ++++++++++++++++++++
 c/nla-digbench/geo2-ll.yml      | 11 +++++
 c/nla-digbench/geo3-ll.c        | 44 ++++++++++++++++++++
 c/nla-digbench/geo3-ll.yml      | 11 +++++
 c/nla-digbench/hard-ll.c        | 61 +++++++++++++++++++++++++++
 c/nla-digbench/hard-ll.yml      | 11 +++++
 c/nla-digbench/prod4br-ll.c     | 58 ++++++++++++++++++++++++++
 c/nla-digbench/prod4br-ll.yml   | 11 +++++
 c/nla-digbench/prodbin-ll.c     | 47 +++++++++++++++++++++
 c/nla-digbench/prodbin-ll.yml   | 11 +++++
 c/nla-digbench/ps2-ll.c         | 39 +++++++++++++++++
 c/nla-digbench/ps2-ll.yml       | 11 +++++
 c/nla-digbench/ps3-ll.c         | 38 +++++++++++++++++
 c/nla-digbench/ps3-ll.yml       | 11 +++++
 c/nla-digbench/ps4-ll.c         | 39 +++++++++++++++++
 c/nla-digbench/ps4-ll.yml       | 11 +++++
 c/nla-digbench/ps5-ll.c         | 41 ++++++++++++++++++
 c/nla-digbench/ps5-ll.yml       | 11 +++++
 c/nla-digbench/ps6-ll.c         | 41 ++++++++++++++++++
 c/nla-digbench/ps6-ll.yml       | 11 +++++
 c/nla-digbench/sqrt1-ll.c       | 48 +++++++++++++++++++++
 c/nla-digbench/sqrt1-ll.yml     | 11 +++++
 45 files changed, 1430 insertions(+)
 create mode 100644 c/nla-digbench/bresenham-ll.c
 create mode 100644 c/nla-digbench/bresenham-ll.yml
 create mode 100644 c/nla-digbench/cohencu-ll.c
 create mode 100644 c/nla-digbench/cohencu-ll.yml
 create mode 100644 c/nla-digbench/cohendiv-ll.c
 create mode 100644 c/nla-digbench/cohendiv-ll.yml
 create mode 100644 c/nla-digbench/dijkstra-u.c
 create mode 100644 c/nla-digbench/dijkstra-u.yml
 create mode 100644 c/nla-digbench/egcd-ll.c
 create mode 100644 c/nla-digbench/egcd-ll.yml
 create mode 100644 c/nla-digbench/egcd2-ll.c
 create mode 100644 c/nla-digbench/egcd2-ll.yml
 create mode 100644 c/nla-digbench/egcd3-ll.c
 create mode 100644 c/nla-digbench/egcd3-ll.yml
 create mode 100644 c/nla-digbench/fermat1-ll.c
 create mode 100644 c/nla-digbench/fermat1-ll.yml
 create mode 100644 c/nla-digbench/fermat1-u.c
 create mode 100644 c/nla-digbench/fermat2-ll.c
 create mode 100644 c/nla-digbench/fermat2-ll.yml
 create mode 100644 c/nla-digbench/geo1-ll.c
 create mode 100644 c/nla-digbench/geo1-ll.yml
 create mode 100644 c/nla-digbench/geo1-u.c
 create mode 100644 c/nla-digbench/geo1-u.yml
 create mode 100644 c/nla-digbench/geo2-ll.c
 create mode 100644 c/nla-digbench/geo2-ll.yml
 create mode 100644 c/nla-digbench/geo3-ll.c
 create mode 100644 c/nla-digbench/geo3-ll.yml
 create mode 100644 c/nla-digbench/hard-ll.c
 create mode 100644 c/nla-digbench/hard-ll.yml
 create mode 100644 c/nla-digbench/prod4br-ll.c
 create mode 100644 c/nla-digbench/prod4br-ll.yml
 create mode 100644 c/nla-digbench/prodbin-ll.c
 create mode 100644 c/nla-digbench/prodbin-ll.yml
 create mode 100644 c/nla-digbench/ps2-ll.c
 create mode 100644 c/nla-digbench/ps2-ll.yml
 create mode 100644 c/nla-digbench/ps3-ll.c
 create mode 100644 c/nla-digbench/ps3-ll.yml
 create mode 100644 c/nla-digbench/ps4-ll.c
 create mode 100644 c/nla-digbench/ps4-ll.yml
 create mode 100644 c/nla-digbench/ps5-ll.c
 create mode 100644 c/nla-digbench/ps5-ll.yml
 create mode 100644 c/nla-digbench/ps6-ll.c
 create mode 100644 c/nla-digbench/ps6-ll.yml
 create mode 100644 c/nla-digbench/sqrt1-ll.c
 create mode 100644 c/nla-digbench/sqrt1-ll.yml

diff --git a/c/nla-digbench/bresenham-ll.c b/c/nla-digbench/bresenham-ll.c
new file mode 100644
index 00000000000..759549e7cd2
--- /dev/null
+++ b/c/nla-digbench/bresenham-ll.c
@@ -0,0 +1,49 @@
+/*
+  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;
+    int x, y;
+    long long v;
+    X = __VERIFIER_nondet_int();
+    Y = __VERIFIER_nondet_int();
+    assume_abort_if_not(X < 2147483647); // required to avoid overflow of x in the loop
+    v = ((long long) 2 * Y) - X;         // cast required to avoid int overflow
+    y = 0;
+    x = 0;
+
+    while (1) {
+	__VERIFIER_assert( 2*Y*x - 2*X*y - X + 2*Y - v == 0);
+        if (!(x <= X))
+            break;
+        // out[x] = y
+
+        if (v < 0) {
+            v = v + 2 * Y;
+        } else {
+            v = v + 2 * (Y - X);
+            y++;
+        }
+        x++;
+    }
+    __VERIFIER_assert(2*Y*x - 2*x*y - X + 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/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/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/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..a9c6d7dea3a
--- /dev/null
+++ b/c/nla-digbench/dijkstra-u.yml
@@ -0,0 +1,11 @@
+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: true
+
+options:
+  language: C
+  data_model: ILP32
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/egcd2-ll.c b/c/nla-digbench/egcd2-ll.c
new file mode 100644
index 00000000000..03e6ca0e50b
--- /dev/null
+++ b/c/nla-digbench/egcd2-ll.c
@@ -0,0 +1,67 @@
+/* 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;
+    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;
+    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*x*y + s*y*y - 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/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/fermat1-ll.c b/c/nla-digbench/fermat1-ll.c
new file mode 100644
index 00000000000..23de8b1ed3a
--- /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) * (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(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-u.c b/c/nla-digbench/fermat1-u.c
new file mode 100644
index 00000000000..05089efe149
--- /dev/null
+++ b/c/nla-digbench/fermat1-u.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-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 A, R;
+    unsigned int u, v, r;
+    A = __VERIFIER_nondet_unsigned_int();
+    R = __VERIFIER_nondet_unsigned_int();
+    assume_abort_if_not((R - 1) * (R - 1) < A);
+    //assume_abort_if_not(A <= R * R);
+    assume_abort_if_not(A % 2 == 1);
+
+    u = 2 * R + 1;
+    v = 1;
+    r = 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(4*A == u*u - v*v  - 2*u + 2*v);
+    return 0;
+}
diff --git a/c/nla-digbench/fermat2-ll.c b/c/nla-digbench/fermat2-ll.c
new file mode 100644
index 00000000000..0d3f35eb5c1
--- /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) * (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(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/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/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/geo3-ll.c b/c/nla-digbench/geo3-ll.c
new file mode 100644
index 00000000000..63403ee59bd
--- /dev/null
+++ b/c/nla-digbench/geo3-ll.c
@@ -0,0 +1,44 @@
+/* 
+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;
+    z = __VERIFIER_nondet_int();
+    a = __VERIFIER_nondet_int();
+    k = __VERIFIER_nondet_int();
+
+    x = a;
+    y = 1;
+    c = 1;
+
+    while (1) {
+        __VERIFIER_assert(z*x - x + a - a*z*y == 0);
+
+        if (!(c < k))
+            break;
+
+        c = c + 1;
+        x = x * z + a;
+        y = y * z;
+    }
+    __VERIFIER_assert(z*x - x + a - a*z*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/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/prod4br-ll.c b/c/nla-digbench/prod4br-ll.c
new file mode 100644
index 00000000000..13eaee22173
--- /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 == 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 == 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/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/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/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/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/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/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/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

From af1524ff90e4b1cde855ffa0b6024e97f338d9ae Mon Sep 17 00:00:00 2001
From: divyesh <divyesh@cse.iitb.ac.in>
Date: Wed, 14 Oct 2020 02:43:10 +0530
Subject: [PATCH 10/13] Corrections

---
 c/nla-digbench/dijkstra-u.yml |  2 +-
 c/nla-digbench/fermat1-u.c    | 57 -----------------------------------
 2 files changed, 1 insertion(+), 58 deletions(-)
 delete mode 100644 c/nla-digbench/fermat1-u.c

diff --git a/c/nla-digbench/dijkstra-u.yml b/c/nla-digbench/dijkstra-u.yml
index a9c6d7dea3a..778f24281ea 100644
--- a/c/nla-digbench/dijkstra-u.yml
+++ b/c/nla-digbench/dijkstra-u.yml
@@ -1,5 +1,5 @@
 format_version: '2.0'
-input_files: 'dijkstra.c'
+input_files: 'dijkstra-u.c'
 properties:
   - property_file: ../properties/unreach-call.prp
     expected_verdict: true
diff --git a/c/nla-digbench/fermat1-u.c b/c/nla-digbench/fermat1-u.c
deleted file mode 100644
index 05089efe149..00000000000
--- a/c/nla-digbench/fermat1-u.c
+++ /dev/null
@@ -1,57 +0,0 @@
-/* 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-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 A, R;
-    unsigned int u, v, r;
-    A = __VERIFIER_nondet_unsigned_int();
-    R = __VERIFIER_nondet_unsigned_int();
-    assume_abort_if_not((R - 1) * (R - 1) < A);
-    //assume_abort_if_not(A <= R * R);
-    assume_abort_if_not(A % 2 == 1);
-
-    u = 2 * R + 1;
-    v = 1;
-    r = 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(4*A == u*u - v*v  - 2*u + 2*v);
-    return 0;
-}

From ada9e4178b906a3aef0e7ff9c50da6b1ac321134 Mon Sep 17 00:00:00 2001
From: "divyesh@cse.iitb.ac.in" <divyesh@cse.iitb.ac.in>
Date: Tue, 20 Oct 2020 10:16:36 +0530
Subject: [PATCH 11/13] Missed adding the type cast to avoid the overflow

---
 c/nla-digbench/prod4br-ll.c | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/c/nla-digbench/prod4br-ll.c b/c/nla-digbench/prod4br-ll.c
index 13eaee22173..5e43c546c4b 100644
--- a/c/nla-digbench/prod4br-ll.c
+++ b/c/nla-digbench/prod4br-ll.c
@@ -30,7 +30,7 @@ int main() {
     q = 0;
 
     while (1) {
-        __VERIFIER_assert(q + a * b * p == x * y);
+        __VERIFIER_assert(q + a * b * p == (long long) x * y);
 
         if (!(a != 0 && b != 0))
             break;
@@ -52,7 +52,7 @@ int main() {
         }
     }
 
-    __VERIFIER_assert(q == x * y);
+    __VERIFIER_assert(q == (long long) x * y);
     __VERIFIER_assert(a * b == 0);
     return 0;
 }

From 0794c4560763959673e62c9d55020a39288f7c7b Mon Sep 17 00:00:00 2001
From: "divyesh@cse.iitb.ac.in" <divyesh@cse.iitb.ac.in>
Date: Tue, 20 Oct 2020 10:21:15 +0530
Subject: [PATCH 12/13] Type casts at sub-expression level

llvm has a local handling of the implicity casting when generating the
type cast instructions in the IR.
This commit can be reverted if llvm starts looking at the entire
expression as given in a C progam, rather than just the type of
the variables involved in the current expression, before
generating the needed type casts.
---
 c/nla-digbench/bresenham-ll.c | 8 +++-----
 c/nla-digbench/egcd2-ll.c     | 7 +++++--
 c/nla-digbench/fermat1-ll.c   | 8 ++++----
 c/nla-digbench/fermat2-ll.c   | 8 ++++----
 c/nla-digbench/geo3-ll.c      | 7 ++++---
 5 files changed, 20 insertions(+), 18 deletions(-)

diff --git a/c/nla-digbench/bresenham-ll.c b/c/nla-digbench/bresenham-ll.c
index 759549e7cd2..1bc1492e5cd 100644
--- a/c/nla-digbench/bresenham-ll.c
+++ b/c/nla-digbench/bresenham-ll.c
@@ -20,17 +20,15 @@ void __VERIFIER_assert(int cond) {
 
 int main() {
     int X, Y;
-    int x, y;
-    long long v;
+    long long x, y, v;
     X = __VERIFIER_nondet_int();
     Y = __VERIFIER_nondet_int();
-    assume_abort_if_not(X < 2147483647); // required to avoid overflow of x in the loop
     v = ((long long) 2 * Y) - X;         // cast required to avoid int overflow
     y = 0;
     x = 0;
 
     while (1) {
-	__VERIFIER_assert( 2*Y*x - 2*X*y - X + 2*Y - v == 0);
+	__VERIFIER_assert( 2*Y*x - 2*X*y - X + (long long) 2*Y - v == 0);
         if (!(x <= X))
             break;
         // out[x] = y
@@ -43,7 +41,7 @@ int main() {
         }
         x++;
     }
-    __VERIFIER_assert(2*Y*x - 2*x*y - X + 2*Y - v + 2*y == 0);
+    __VERIFIER_assert(2*Y*x - 2*x*y - X + (long long) 2*Y - v + 2*y == 0);
 
     return 0;
 }
diff --git a/c/nla-digbench/egcd2-ll.c b/c/nla-digbench/egcd2-ll.c
index 03e6ca0e50b..be285a4a147 100644
--- a/c/nla-digbench/egcd2-ll.c
+++ b/c/nla-digbench/egcd2-ll.c
@@ -17,7 +17,7 @@ void __VERIFIER_assert(int cond) {
 
 int main() {
     int x, y;
-    long long a, b, p, q, r, s, c, k;
+    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);
@@ -31,6 +31,9 @@ int main() {
     s = 1;
     c = 0;
     k = 0;
+    xy = (long long) x * y;
+    yy = (long long) y * y;
+
     while (1) {
         if (!(b != 0))
             break;
@@ -41,7 +44,7 @@ int main() {
             __VERIFIER_assert(a == k * b + c);
             __VERIFIER_assert(a == y*r + x*p);
             __VERIFIER_assert(b == x * q + y * s);
-	    __VERIFIER_assert(q*x*y + s*y*y - q*x - b*y - s*y + b == 0);
+	    __VERIFIER_assert(q*xy + s*yy - q*x - b*y - s*y + b == 0);
             if (!(c >= b))
                 break;
             c = c - b;
diff --git a/c/nla-digbench/fermat1-ll.c b/c/nla-digbench/fermat1-ll.c
index 23de8b1ed3a..2d82b5c0e90 100644
--- a/c/nla-digbench/fermat1-ll.c
+++ b/c/nla-digbench/fermat1-ll.c
@@ -21,13 +21,13 @@ int main() {
     long long u, v, r;
     A = __VERIFIER_nondet_int();
     R = __VERIFIER_nondet_int();
-    assume_abort_if_not(((long long) (R - 1) * (R - 1)) < A);
+    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;
+    u = ((long long) 2 * R) + 1;
     v = 1;
-    r = (long long) R * R - A;
+    r = ((long long) R * R) - A;
 
 
     while (1) {
@@ -52,6 +52,6 @@ int main() {
         }
     }
 
-    __VERIFIER_assert(4*A == u*u - v*v - 2*u + 2*v);
+    __VERIFIER_assert(((long long) 4*A) == u*u - v*v - 2*u + 2*v);
     return 0;
 }
diff --git a/c/nla-digbench/fermat2-ll.c b/c/nla-digbench/fermat2-ll.c
index 0d3f35eb5c1..07a885afab6 100644
--- a/c/nla-digbench/fermat2-ll.c
+++ b/c/nla-digbench/fermat2-ll.c
@@ -22,13 +22,13 @@ int main() {
     A = __VERIFIER_nondet_int();
     R = __VERIFIER_nondet_int();
     //assume_abort_if_not(A >= 1);
-    assume_abort_if_not((long long) (R - 1) * (R - 1) < A);
+    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;
+    u = ((long long) 2 * R) + 1;
     v = 1;
-    r = (long long) R * R - A;
+    r = ((long long) R * R) - A;
 
     while (1) {
         __VERIFIER_assert(4*(A+r) == u*u - v*v - 2*u + 2*v);
@@ -44,6 +44,6 @@ int main() {
     }
 
     //return  (u - v) / 2;
-    __VERIFIER_assert(4*A == u*u - v*v  - 2*u + 2*v);
+    __VERIFIER_assert(((long long) 4*A) == u*u - v*v  - 2*u + 2*v);
     return 0;
 }
diff --git a/c/nla-digbench/geo3-ll.c b/c/nla-digbench/geo3-ll.c
index 63403ee59bd..ca3e329c107 100644
--- a/c/nla-digbench/geo3-ll.c
+++ b/c/nla-digbench/geo3-ll.c
@@ -20,7 +20,7 @@ void __VERIFIER_assert(int cond) {
 }
 int main() {
     int z, a, k;
-    long long x, y, c;
+    long long x, y, c, az;
     z = __VERIFIER_nondet_int();
     a = __VERIFIER_nondet_int();
     k = __VERIFIER_nondet_int();
@@ -28,9 +28,10 @@ int main() {
     x = a;
     y = 1;
     c = 1;
+    az = (long long) a * z;
 
     while (1) {
-        __VERIFIER_assert(z*x - x + a - a*z*y == 0);
+        __VERIFIER_assert(z*x - x + a - az*y == 0);
 
         if (!(c < k))
             break;
@@ -39,6 +40,6 @@ int main() {
         x = x * z + a;
         y = y * z;
     }
-    __VERIFIER_assert(z*x - x + a - a*z*y == 0);
+    __VERIFIER_assert(z*x - x + a - az*y == 0);
     return x;
 }

From 9166aa3f65064e43c3c38ccdd9410f07a416ffd6 Mon Sep 17 00:00:00 2001
From: "divyesh@cse.iitb.ac.in" <divyesh@cse.iitb.ac.in>
Date: Tue, 20 Oct 2020 19:22:47 +0530
Subject: [PATCH 13/13] Added a few more type casts to avoid overflow in llvm
 IR Can be reverted with same reason as the previous commit.

---
 c/nla-digbench/bresenham-ll.c | 14 +++++++++-----
 c/nla-digbench/egcd2-ll.c     |  2 ++
 2 files changed, 11 insertions(+), 5 deletions(-)

diff --git a/c/nla-digbench/bresenham-ll.c b/c/nla-digbench/bresenham-ll.c
index 1bc1492e5cd..7108c158a73 100644
--- a/c/nla-digbench/bresenham-ll.c
+++ b/c/nla-digbench/bresenham-ll.c
@@ -20,7 +20,7 @@ void __VERIFIER_assert(int cond) {
 
 int main() {
     int X, Y;
-    long long x, y, v;
+    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
@@ -28,20 +28,24 @@ int main() {
     x = 0;
 
     while (1) {
-	__VERIFIER_assert( 2*Y*x - 2*X*y - X + (long long) 2*Y - v == 0);
+        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 + 2 * Y;
+            v = v + (long long) 2 * Y;
         } else {
-            v = v + 2 * (Y - X);
+            v = v + 2 * ((long long) Y - X);
             y++;
         }
         x++;
     }
-    __VERIFIER_assert(2*Y*x - 2*x*y - X + (long long) 2*Y - v + 2*y == 0);
+    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/egcd2-ll.c b/c/nla-digbench/egcd2-ll.c
index be285a4a147..e3272e21d3b 100644
--- a/c/nla-digbench/egcd2-ll.c
+++ b/c/nla-digbench/egcd2-ll.c
@@ -33,6 +33,8 @@ int main() {
     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))