Add simple algebraic equations (identities) as tests.

These are expected to exercise that implements conversion of
arithmetic operators for signed ints, including integers of
multiple bit widths (using `long long` and `char` for now,
because `stdint.h` introduces typecasts and we don't support
them yet).

Author: NlightNFotis

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.c

@@ -0,0 +1,46 @@
+#include <stdlib.h>
+
+int main()
+{
+  int a;
+  __CPROVER_assume(a < 100);
+  __CPROVER_assume(a > -100);
+  __CPROVER_assume(a != 0);
+
+  // Simple algebraic identities - expected to drive the SMT backend
+  __CPROVER_assert(a + a == a * 2, "a plus a always equals two times a");
+  __CPROVER_assert(a - a == 0, "a minus a always equals 0");
+  __CPROVER_assert(a + -a == 0, "a plus its additive inverse equals 0");
+  __CPROVER_assert(
+    a - -a == 2 * a, "a minus its additive inverse equals two times a");
+  __CPROVER_assert((a * a) / a == a, "a squared divided by a equals a");
+  __CPROVER_assert((2 * a) / a == 2, "two times a divided by a equals two");
+  __CPROVER_assert(a % a == 0, "a mod itself equals 0");
+
+  // Same round of tests, but for a type of different size
+  long long int b;
+  __CPROVER_assume(b < 100ll);
+  __CPROVER_assume(b > -100ll);
+  __CPROVER_assume(b != 0ll);
+
+  __CPROVER_assert(b + b == b * 2ll, "b plus b always equals two times b");
+  __CPROVER_assert(b - b == 0ll, "b minus b always equals 0");
+  __CPROVER_assert(b + -b == 0ll, "b plus its additive inverse equals 0");
+  __CPROVER_assert(
+    b - -b == 2ll * b, "b minus its additive inverse equals two times b");
+  __CPROVER_assert((b * b) / b == b, "b squared divided by b equals b");
+  __CPROVER_assert((2ll * b) / b == 2ll, "two times b divided by b equals two");
+  __CPROVER_assert(b % b == 0ll, "b mod itself equals 0");
+
+  char c = 0x0;
+  __CPROVER_assume(c != 0x00);
+
+  __CPROVER_assert(c + c == c * 0x2, "c plus c always equals two times c");
+  __CPROVER_assert(c - c == 0x0, "c minus c always equals 0");
+  __CPROVER_assert(c + -c == 0x0, "c plus its additive inverse equals 0");
+  __CPROVER_assert(
+    c - -c == 0x2 * c, "c minus its additive inverse equals two times c");
+  __CPROVER_assert((c * c) / c == c, "c squared divided by c equals c");
+  __CPROVER_assert((0x2 * c) / c == 0x2, "two times c divided by c equals two");
+  __CPROVER_assert(c % c == 0x0, "c mod itself equals 0");
+}

regression/cbmc-incr-smt2/bitvector-arithmetic-operators/simple_equation.desc

@@ -0,0 +1,34 @@
+CORE
+simple_equation.c
+--incremental-smt2-solver 'z3 --smt2 -in' --trace
+\[main\.assertion\.1\] line \d+ a plus a always equals two times a: SUCCESS
+\[main\.assertion\.2\] line \d+ a minus a always equals 0: SUCCESS
+\[main\.assertion\.3\] line \d+ a plus its additive inverse equals 0: SUCCESS
+\[main\.assertion\.4\] line \d+ a minus its additive inverse equals two times a: SUCCESS
+\[main\.assertion\.5\] line \d+ a squared divided by a equals a: SUCCESS
+\[main\.assertion\.6\] line \d+ two times a divided by a equals two: SUCCESS
+\[main\.assertion\.7\] line \d+ a mod itself equals 0: SUCCESS
+\[main\.assertion\.8\] line \d+ b plus b always equals two times b: SUCCESS
+\[main\.assertion\.9\] line \d+ b minus b always equals 0: SUCCESS
+\[main\.assertion\.10\] line \d+ b plus its additive inverse equals 0: SUCCESS
+\[main\.assertion\.11\] line \d+ b minus its additive inverse equals two times b: SUCCESS
+\[main\.assertion\.12\] line \d+ b squared divided by b equals b: SUCCESS
+\[main\.assertion\.13\] line \d+ two times b divided by b equals two: SUCCESS
+\[main\.assertion\.14\] line \d+ b mod itself equals 0: SUCCESS
+\[main\.assertion\.15\] line \d+ c plus c always equals two times c: SUCCESS
+\[main\.assertion\.16\] line \d+ c minus c always equals 0: SUCCESS
+\[main\.assertion\.17\] line \d+ c plus its additive inverse equals 0: SUCCESS
+\[main\.assertion\.18\] line \d+ c minus its additive inverse equals two times c: SUCCESS
+\[main\.assertion\.19\] line \d+ c squared divided by c equals c: SUCCESS
+\[main\.assertion\.20\] line \d+ two times c divided by c equals two: SUCCESS
+\[main\.assertion\.21\] line \d+ c mod itself equals 0: SUCCESS
+^VERIFICATION SUCCESSFUL$
+^EXIT=0$
+^SIGNAL=0$
+--
+--
+This is a simple test that's trying to verify that some simple algebraic
+identities hold for all values insider an integral interval. This is expected
+to work as an end-to-end example driving the all of the conversion function
+for bitvector arithmetic in the new SMT backend, getting us to the point of
+a full verification run producing a result.