Incremental SMT back-end no longer requires --slice-formula

tautschnig · tautschnig · commit f89db31f1806 · 2022-12-14T08:53:37.000Z
With #6590, several unnecessary symbols are no longer included in goto programs. These include unbounded arrays, which the incremental SMT back-end hitherto does not support. The use of --slice-formula was a workaround to make sure the unnecessary symbols (or equalities over them) don't end up in the formula; now they aren't part of the goto program, so the workaround no longer adds value.
diff --git a/doc/cprover-manual/smt2-incr.md b/doc/cprover-manual/smt2-incr.md
@@ -61,15 +61,12 @@ To use the incremental SMT2 backend it is enough to add the `--incremental-smt2-
 the CBMC command line followed by the command to invoke the chosen solver using smtlib 2.6 input in
 interactive mode.
 
-Note that the use of the `--slice-formula` option is recommended at this time to slice out
-unnecessary code (that may not be supported at the moment) and this can also improve performance.
-
 Here are two examples to show how to analyse a file `program.c` using Z3 and CVC5 solvers.
 
 To use the Z3 SMT solver:
 
 ```shell 
-cbmc --slice-formula --incremental-smt2-solver 'z3 -smt2 -in' program.c
+cbmc --incremental-smt2-solver 'z3 -smt2 -in' program.c
 ```
 
 If `z3` is not on the `PATH`, then it is enough to replace `'z3 -smt2 -in'`
@@ -78,7 +75,7 @@ with `'<command-to-execute-z3> -smt2 -in'`,
 Similarly to execute CBMC using the CVC5 solver:
 
 ```shell
-cbmc --slice-formula --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' program.c
+cbmc --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' program.c
 ```
 
 As the command to execute the solver is left to the user, it is possible to fine-tune it by passing
@@ -87,7 +84,7 @@ adding `param_name=value` to the command line, so to use the Z3 solver with `wel
 property set to `false` the following has to be run:
 
 ```shell
-cbmc --slice-formula --incremental-smt2-solver 'z3 -smt2 -in well_sorted_check=false' program.c
+cbmc --incremental-smt2-solver 'z3 -smt2 -in well_sorted_check=false' program.c
 ```
 
 ### Examples
@@ -110,7 +107,7 @@ int main()
 To analyze it we should run:
 
 ```shell
-cbmc --incremental-smt2-solver 'z3 -smt2 -in' --slice-formula program.c
+cbmc --incremental-smt2-solver 'z3 -smt2 -in' program.c
 ```
 
 We will get the verification results as follows:
@@ -162,7 +159,7 @@ The incremental smt2 backend also supports trace generation, so to get a trace t
 assertions the `--trace` argument should be added, so the command to run is:
 
 ```shell
-cbmc --incremental-smt2-solver 'z3 -smt2 -in' --slice-formula --trace program.c
+cbmc --incremental-smt2-solver 'z3 -smt2 -in' --trace program.c
 ```
 
 This will append the trace to CBMC's output as follows:
diff --git a/doc/man/cbmc.1 b/doc/man/cbmc.1
@@ -461,8 +461,6 @@ The solver name must be in the "PATH" or be an executable with full path.
 The SMT solver should accept incremental SMTlib v2.6 formatted input from the stdin.
 .br
 The SMT solver should support the QF_AUFBV logic.
-.br
-The flag \fB\-\-slice\-formula\fR should be added to remove some not-yet supported features.
 .TP
 \fB\-\-outfile\fR filename
 output formula to given file
diff --git a/regression/cbmc-incr-smt2/CMakeLists.txt b/regression/cbmc-incr-smt2/CMakeLists.txt
@@ -7,14 +7,14 @@ endif()
 
 add_test_pl_profile(
     "cbmc-incr-smt2-z3"
-    "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula"
+    "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
     "-C;${exclude_win_broken_tests};-s;new-smt-z3"
     "CORE"
 )
 
 add_test_pl_profile(
     "cbmc-incr-smt2-cvc5"
-    "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation --slice-formula"
+    "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation"
     "-C;${exclude_win_broken_tests};-s;new-smt-cvc5"
     "CORE"
 )
diff --git a/regression/cbmc-incr-smt2/Makefile b/regression/cbmc-incr-smt2/Makefile
@@ -12,10 +12,10 @@ endif
 test: test.z3 test.cvc5
 
 test.z3:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation" $(exclude_broken_windows_tests)
 
 test.cvc5:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation" $(exclude_broken_windows_tests)
 
 tests.log: ../test.pl test
 
diff --git a/regression/cbmc-incr-smt2/arrays/array_of.desc b/regression/cbmc-incr-smt2/arrays/array_of.desc
@@ -1,6 +1,6 @@
 CORE
 array_of.c
-
+--slice-formula
 Passing problem to incremental SMT2 solving
 line \d+ False array condition: FAILURE
 line \d+ Valid array condition: SUCCESS
@@ -10,4 +10,5 @@ line \d+ Valid array condition: SUCCESS
 --
 Test using __CPROVER_array_set consisting in an `array_of` node which sets all values of a given
 array to a given value.
-This test uses a forall SMT statement.
+This test uses a forall SMT statement. Requires --slice-formula for the time
+being, but this is a workaround.
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign-between.desc
@@ -1,6 +1,6 @@
 CORE
 array-misalign-between.c
---slice-formula
+
 \[main\.assertion\.1\] line \d+ assertion x\[0\] == 256: SUCCESS
 \[main\.assertion\.2\] line \d+ assertion x\[0\] == 0: FAILURE
 \[main\.assertion\.3\] line \d+ assertion x\[1\] == 0: SUCCESS
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/array-misalign.desc
@@ -1,6 +1,6 @@
 CORE
 array-misalign.c
---slice-formula
+
 \[main.assertion\.1\] line \d+ assertion x\[0\] == 256ul: SUCCESS
 \[main.assertion\.2\] line \d+ assertion x\[0\] == 0ul: FAILURE
 \[main.assertion\.3\] line \d+ assertion x\[1\] == 0ul: SUCCESS
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/bitwise.desc
@@ -1,6 +1,6 @@
 CORE
 bitwise_ops.c
---slice-formula
+
 \[main\.assertion\.1\] line \d+ This is going to fail for bit-opposites: FAILURE
 \[main\.assertion\.2\] line \d+ This is going to hold for all values != 0: SUCCESS
 \[main\.assertion\.3\] line \d+ This is going to fail for the same value in A and B: FAILURE
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract-small.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract-small.desc
@@ -1,6 +1,6 @@
 CORE
 byte-extract-small.c
---slice-formula
+
 \[main.assertion\.1\] line \d+ assertion z == 257: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-extract.desc
@@ -1,6 +1,6 @@
 CORE
 byte-extract.c
---slice-formula
+
 \[main.assertion\.1\] line \d+ assertion y\[0\] == 0: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update-small.desc
@@ -1,6 +1,6 @@
 CORE
 byte-update-small.c
---slice-formula
+
 \[main\.assertion\.1\] line \d+ assertion x\[0\] == 2: SUCCESS
 \[main\.assertion\.2\] line \d+ assertion x\[1\] == 1: SUCCESS
 ^EXIT=0$
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/byte-update.desc
@@ -1,6 +1,6 @@
 CORE
 byte-update.c
---slice-formula
+
 \[main\.assertion\.1\] line \d+ assertion x == 256: SUCCESS
 ^EXIT=0$
 ^SIGNAL=0$
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_left.desc
@@ -1,6 +1,6 @@
 CORE
 shift_left.c
---slice-formula
+
 \[main\.assertion\.1\] line \d Shifted result should be greater than one: FAILURE
 ^EXIT=10$
 ^SIGNAL=0$
diff --git a/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc b/regression/cbmc-incr-smt2/bitvector-bitwise-operators/shift_right.desc
@@ -1,6 +1,6 @@
 CORE
 shift_right.c
---slice-formula --trace
+--trace
 \[main\.assertion\.1\] line \d+ Right shifting a uint with leftmost bit set is a logical shift: FAILURE
 \[main\.assertion\.2\] line \d+ Right shifting a positive number has a lower bound of 0: SUCCESS
 \[main\.assertion\.3\] line \d+ Right shifting a negative number has a lower bound value of -1: SUCCESS
diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc
@@ -23,7 +23,6 @@ Solver response - sat
 ^EXIT=10$
 ^SIGNAL=0$
 --
-type: pointer
 --
 Test that running cbmc with the `--incremental-smt2-solver` argument can be used
 to send a valid SMT2 formula to a sub-process solver for an example input file
diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc
@@ -1,6 +1,6 @@
 CORE
 test.c
---verbosity 10
+--slice-formula --verbosity 10
 Passing problem to incremental SMT2 solving via
 Sending command to SMT2 solver - \(set-option :produce-models true\)
 Sending command to SMT2 solver - \(set-logic ALL\)
diff --git a/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc b/regression/cbmc-incr-smt2/nondeterministic-int-assert/valid_unsat.desc
@@ -8,7 +8,6 @@ VERIFICATION SUCCESSFUL
 ^EXIT=0$
 ^SIGNAL=0$
 --
-type: pointer
 --
 Test that given a `.c` program where all assertions hold, the solver responds
 with unsat and CBMC reports that verification is successful.
diff --git a/regression/cbmc-incr-smt2/pointers/pointer_values_2.desc b/regression/cbmc-incr-smt2/pointers/pointer_values_2.desc
@@ -1,6 +1,6 @@
 CORE
 pointer_values_2.c
---trace --slice-formula
+--trace
 \[main\.assertion\.1\] line \d should fail as b can also be assigned 0xDEADBEEF: FAILURE
 a=\(signed int \*\)3735928559
 b=\(signed int \*\)3735928559
diff --git a/regression/cbmc-output-file/dump-smt-formula/cvc5-match.desc b/regression/cbmc-output-file/dump-smt-formula/cvc5-match.desc
@@ -1,6 +1,6 @@
 CORE
 test.c
---incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --slice-formula --dump-smt-formula %out-file-name%
+--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --dump-smt-formula %out-file-name%
 Passing problem to incremental SMT2 solving via "cvc5 --lang=smtlib2.6 --incremental"
 \[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
 Output file matches.
diff --git a/regression/cbmc-output-file/dump-smt-formula/cvc5-no-match.desc b/regression/cbmc-output-file/dump-smt-formula/cvc5-no-match.desc
@@ -1,6 +1,6 @@
 CORE
 test.c
---incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --slice-formula --dump-smt-formula %out-file-name%
+--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --dump-smt-formula %out-file-name%
 Passing problem to incremental SMT2 solving via "cvc5 --lang=smtlib2.6 --incremental"
 \[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
 Output file does not match.
diff --git a/regression/cbmc-output-file/dump-smt-formula/z3-match.desc b/regression/cbmc-output-file/dump-smt-formula/z3-match.desc
@@ -1,6 +1,6 @@
 CORE
 test.c
---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --dump-smt-formula %out-file-name%
+--incremental-smt2-solver 'z3 --smt2 -in' --dump-smt-formula %out-file-name%
 Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
 \[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
 Output file matches.
diff --git a/regression/cbmc-output-file/dump-smt-formula/z3-no-match.desc b/regression/cbmc-output-file/dump-smt-formula/z3-no-match.desc
@@ -1,6 +1,6 @@
 CORE
 test.c
---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --dump-smt-formula %out-file-name%
+--incremental-smt2-solver 'z3 --smt2 -in' --dump-smt-formula %out-file-name%
 Passing problem to incremental SMT2 solving via "z3 --smt2 -in"
 \[main.assertion.\d+\] line \d+ Nondeterministic int assert.: FAILURE
 Output file does not match.
diff --git a/regression/cbmc-output-file/outfile/cvc5-match.desc b/regression/cbmc-output-file/outfile/cvc5-match.desc
@@ -1,6 +1,6 @@
 CORE
 test.c
---incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --slice-formula --outfile %out-file-name%
+--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --outfile %out-file-name%
 Passing problem to incremental SMT2 solving via SMT2 incremental dry-run
 Output file matches.
 ^EXIT=0$
diff --git a/regression/cbmc-output-file/outfile/cvc5-no-match.desc b/regression/cbmc-output-file/outfile/cvc5-no-match.desc
@@ -1,6 +1,6 @@
 CORE
 test.c
---incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --slice-formula --outfile %out-file-name%
+--incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --outfile %out-file-name%
 Passing problem to incremental SMT2 solving via SMT2 incremental dry-run
 Output file does not match.
 ^EXIT=1$
diff --git a/regression/cbmc-output-file/outfile/z3-match.desc b/regression/cbmc-output-file/outfile/z3-match.desc
@@ -1,6 +1,6 @@
 CORE
 test.c
---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --outfile %out-file-name%
+--incremental-smt2-solver 'z3 --smt2 -in' --outfile %out-file-name%
 Passing problem to incremental SMT2 solving via SMT2 incremental dry-run
 Output file matches.
 ^EXIT=0$
diff --git a/regression/cbmc-output-file/outfile/z3-no-match.desc b/regression/cbmc-output-file/outfile/z3-no-match.desc
@@ -1,6 +1,6 @@
 CORE
 test.c
---incremental-smt2-solver 'z3 --smt2 -in' --slice-formula --outfile %out-file-name%
+--incremental-smt2-solver 'z3 --smt2 -in' --outfile %out-file-name%
 Passing problem to incremental SMT2 solving via SMT2 incremental dry-run
 Output file does not match.
 ^EXIT=1$
diff --git a/regression/cbmc-primitives/CMakeLists.txt b/regression/cbmc-primitives/CMakeLists.txt
@@ -8,7 +8,7 @@ if(Z3_EXISTS)
     # If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
     add_test_pl_profile(
             "cbmc-primitives-new-smt-backend"
-            "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --slice-formula"
+            "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
             "-I;new-smt-backend;-s;new-smt-backend"
             "CORE"
     )
diff --git a/regression/cbmc-primitives/Makefile b/regression/cbmc-primitives/Makefile
@@ -4,7 +4,7 @@ test:
 	@../test.pl -e -p -c ../../../src/cbmc/cbmc
 
 test.smt2_incr:
-	@../test.pl -e -p -I new-smt-backend -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula"
+	@../test.pl -e -p -I new-smt-backend -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation"
 
 tests.log: ../test.pl
 	@../test.pl -e -p -c ../../../src/cbmc/cbmc
diff --git a/regression/cbmc-primitives/exists_memory_checks/negated_exists.desc b/regression/cbmc-primitives/exists_memory_checks/negated_exists.desc
@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 negated_exists.c
 --pointer-check
 ^EXIT=0$
diff --git a/regression/cbmc/CMakeLists.txt b/regression/cbmc/CMakeLists.txt
@@ -27,7 +27,7 @@ add_test_pl_profile(
 # If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
 add_test_pl_profile(
   "cbmc-new-smt-backend"
-  "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in' --slice-formula"
+  "$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
   "-I;new-smt-backend;-s;new-smt-backend"
   "CORE"
 )
diff --git a/regression/cbmc/Makefile b/regression/cbmc/Makefile
@@ -30,7 +30,7 @@ test-paths-lifo:
 					  -s paths-lifo $(GCC_ONLY)
 
 test-new-smt-backend:
-	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --slice-formula" \
+	@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \
 					  -I new-smt-backend \
 					  -s new-smt-backend $(GCC_ONLY)
 
diff --git a/regression/cbmc/Pointer14/test.desc b/regression/cbmc/Pointer14/test.desc
@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 --pointer-check
 ^VERIFICATION FAILED$
diff --git a/regression/cbmc/Pointer27/test.desc b/regression/cbmc/Pointer27/test.desc
@@ -1,4 +1,4 @@
-CORE new-smt-backend
+CORE
 main.c
 
 ^SIGNAL=0$
diff --git a/src/solvers/smt2_incremental/README.md b/src/solvers/smt2_incremental/README.md
@@ -35,14 +35,6 @@ The new incremental SMT backend has been designed to interoperate with external
 solvers, so the solver name must be in the `PATH` or an executable with full
 path must be provided.
 
-Due to lack of support for conversion of `array_of` expressions that are added
-by CBMC in the before the new SMT backend is invoked, it is necessary to supply
-an extra argument `--slice-formula` so that instances of `arrayof_exprt` are
-removed from the formula to be converted.
-
-As we move forward with our array-support implementation, we anticipate that the
-need for this extra flag will be diminished.
-
 ## Internal code architecture
 
 ### Overview of the sequence of data processing and data flow -
