Add tests of new command line option

So that the new option has some basic tests and a directory to place
tests for follow-up functionality.

Note that all tests are currently passed the `--slice-formula` argument
so that unimplemented functionality from `__cprover_initialise` does not
get passed to the solver if the user code does not depend on it. This
will support incremental implementation of each slice of work in doing
the implementation. Once the implementation is sufficiently complete to
support all expressions generated from `__cprover_initialise`, the
`--slice-formula` argument can be removed again.

Author: thomasspriggs

regression/CMakeLists.txt

@@ -32,6 +32,7 @@ add_subdirectory(cpp)
 add_subdirectory(cbmc-concurrency)
 add_subdirectory(cbmc-cover)
 add_subdirectory(cbmc-incr-oneloop)
+add_subdirectory(cbmc-incr-smt2)
 add_subdirectory(cbmc-incr)
 add_subdirectory(cbmc-with-incr)
 add_subdirectory(array-refinement-with-incr)

regression/Makefile

@@ -10,6 +10,7 @@ DIRS = cbmc \
        cbmc-concurrency \
        cbmc-cover \
        cbmc-incr-oneloop \
+       cbmc-incr-smt2 \
        cbmc-incr \
        cbmc-with-incr \
        array-refinement-with-incr \

regression/cbmc-incr-smt2/CMakeLists.txt

@@ -0,0 +1,4 @@
+
+add_test_pl_tests(
+    "$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --slice-formula"
+)

regression/cbmc-incr-smt2/Makefile

@@ -0,0 +1,14 @@
+default: test
+
+include ../../src/config.inc
+include ../../src/common
+
+test:
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --slice-formula"
+
+tests.log: ../test.pl test
+
+clean:
+	find . -name '*.out' -execdir $(RM) '{}' \;
+	find . -name '*.smt2' -execdir $(RM) '{}' \;
+	$(RM) tests*.log

regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc

@@ -0,0 +1,11 @@
+CORE
+test.c
+--incremental-smt2-solver z3
+Passing problem to incremental SMT2 solving via "z3"
+^EXIT=(0|127|134|137)$
+^SIGNAL=0$
+--
+--
+Test that running cbmc with the `--incremental-smt2-solver` argument causes the
+incremental smt2 solving to be used. Note that at the time of adding this test,
+an invariant violation is expected due to the unimplemented solving.

regression/cbmc-incr-smt2/nondeterministic-int-assert/test.c

@@ -0,0 +1,7 @@
+
+int main()
+{
+  int x;
+  __CPROVER_assert(x, "Nondeterministic int assert.");
+  return 0;
+}