Added regression tests for running in SMT2 mode

This commit introduces a new regression test suite for CBMC's SMT2 translation,
and only tests the translation of structs.

Author: SaswatPadhi

regression/cbmc-smt2-z3/CMakeLists.txt

@@ -0,0 +1,3 @@
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc> --smt2 --z3"
+)

regression/cbmc-smt2-z3/Makefile

@@ -0,0 +1,19 @@
+default: tests.log
+
+include ../../src/config.inc
+include ../../src/common
+
+test: ../test.pl
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --smt2 --z3"
+
+tests.log: test
+
+show:
+	@for dir in *; do \
+		if [ -d "$$dir" ]; then \
+			vim -o "$$dir/*.c" "$$dir/*.out"; \
+		fi; \
+	done;
+
+clean:
+	$(RM) tests.log */*.out

regression/cbmc-smt2-z3/struct/main.c

@@ -0,0 +1,12 @@
+#include <assert.h>
+
+struct test {
+	unsigned int a;
+	unsigned int b;
+};
+
+int main()
+{
+	struct test t;
+	assert (t.a > 0);
+}

regression/cbmc-smt2-z3/struct/test.desc

@@ -0,0 +1,9 @@
+CORE
+main.c
+
+^EXIT=6$
+^SIGNAL=0$
+^VERIFICATION ERROR$
+--
+--
+This test checks the encoding of C `struct`s using SMT2 data types.