From ebcad79ca187dae75d3eb53fb49a6a68ce814050 Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@gmail.com>
Date: Mon, 14 Feb 2022 10:44:28 +0000
Subject: [PATCH 1/2] Add a test for the new SMT backend that exercises the
 flag `--div-by-zero-check` under signed integer division.

---
 .../bitvector-flag-tests/div_by_zero.c            | 15 +++++++++++++++
 .../bitvector-flag-tests/div_by_zero.desc         | 14 ++++++++++++++
 .../cbmc-incr-smt2/bitvector-flag-tests/readme.md | 12 ++++++++++++
 3 files changed, 41 insertions(+)
 create mode 100644 regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.c
 create mode 100644 regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc
 create mode 100644 regression/cbmc-incr-smt2/bitvector-flag-tests/readme.md

diff --git a/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.c b/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.c
new file mode 100644
index 00000000000..c138dc642bd
--- /dev/null
+++ b/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.c
@@ -0,0 +1,15 @@
+int main()
+{
+  int x = 5;
+  int y;
+  int z = 8;
+
+  // Negative case
+  __CPROVER_assert(x / y != 0, "This assertion is falsifiable");
+
+  // Positive case
+  __CPROVER_assert(
+    x / z != 0, "This assertion is valid under all interpretations");
+
+  return 0;
+}
diff --git a/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc b/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc
new file mode 100644
index 00000000000..9f093877f9f
--- /dev/null
+++ b/regression/cbmc-incr-smt2/bitvector-flag-tests/div_by_zero.desc
@@ -0,0 +1,14 @@
+CORE
+div_by_zero.c
+--incremental-smt2-solver 'z3 --smt2 -in' --div-by-zero-check --trace
+\[main\.division-by-zero\.1\] line \d division by zero in x / y: FAILURE
+\[main\.division-by-zero\.2\] line \d+ division by zero in x / z: SUCCESS
+y=0
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+--
+This test is designed to drive the `--div-by-zero-check` in both the positive
+and the negative case, and show that it's working for our current implementation-in-progress
+of the new SMT backend.
diff --git a/regression/cbmc-incr-smt2/bitvector-flag-tests/readme.md b/regression/cbmc-incr-smt2/bitvector-flag-tests/readme.md
new file mode 100644
index 00000000000..44d602fc700
--- /dev/null
+++ b/regression/cbmc-incr-smt2/bitvector-flag-tests/readme.md
@@ -0,0 +1,12 @@
+# Flag tests
+
+Up until this point, the tests we have for the new SMT backend focus on getting
+simple arithmetic or relational operator verification runs done.
+
+This folder contains a couple of tests that are being run with CBMC flags, adding
+extra assertions such as `--div-by-zero` or `--signed-overflow-check`.
+
+Long term the plan is for this folder to be deleted, and the tests that are being
+run as part of the old SMT backend (or maybe even the whole of CBMC's regression
+test suite) to be run through a label or a flag. But for now, this should do well
+enough to allow us to track the progress of our completion of the new backend.

From 73c3952573473498b1ff900b27719f0591a7bc4e Mon Sep 17 00:00:00 2001
From: Fotis Koutoulakis <fotis.koutoulakis@gmail.com>
Date: Mon, 14 Feb 2022 11:04:44 +0000
Subject: [PATCH 2/2] Add a test for the exercise of the
 `signed-overflow-check` flag under the new SMT backend.

---
 .../bitvector-flag-tests/signed_overflow.c            | 10 ++++++++++
 .../bitvector-flag-tests/signed_overflow.desc         | 11 +++++++++++
 2 files changed, 21 insertions(+)
 create mode 100644 regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.c
 create mode 100644 regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc

diff --git a/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.c b/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.c
new file mode 100644
index 00000000000..9ded227d542
--- /dev/null
+++ b/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.c
@@ -0,0 +1,10 @@
+#include <limits.h>
+
+int main()
+{
+  int x = INT_MAX;
+  int y;
+  int z = x + y;
+
+  __CPROVER_assert(z < INT_MIN, "This assertion is falsifiable");
+}
diff --git a/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc b/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc
new file mode 100644
index 00000000000..cd36ec1f882
--- /dev/null
+++ b/regression/cbmc-incr-smt2/bitvector-flag-tests/signed_overflow.desc
@@ -0,0 +1,11 @@
+KNOWNBUG
+signed_overflow.c
+--incremental-smt2-solver 'z3 --smt2 -in' --signed-overflow-check --trace
+^VERIFICATION FAILED$
+^EXIT=10$
+^SIGNAL=0$
+--
+Invariant check failed
+Reason: Reached unimplemented Generation of SMT formula for unknown kind of expression: overflow-\+
+--
+This tests exercise the driving of the `--signed-overflow-check` flag.