diff --git a/doc/cprover-manual/smt2-incr.md b/doc/cprover-manual/smt2-incr.md index 35247e2b46e..0fec02fe597 100644 --- 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 `' -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 index 8b3a2b61202..c405c795c11 100644 --- 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 index 6b00d1fc51d..0591dd946e3 100644 --- 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" - "$ --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation --slice-formula" + "$ --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" - "$ --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation --slice-formula" + "$ --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 index a5e36136c30..30b1ba812d2 100644 --- 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 index 03c974c3464..27481c98b18 100644 --- 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 index 65d08a7a3f5..f941681827b 100644 --- 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 index ebf12032610..184ca5e259c 100644 --- 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 index 44db46465de..ed3a2f2edd5 100644 --- 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 index 351ef6fd938..ef029c5e3d3 100644 --- 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 index d0ce61f1ab5..61fea82c37f 100644 --- 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 index 2b297829663..e422cb3f706 100644 --- 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 index 47a0e05d468..85428f006f3 100644 --- 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 index ffe947dd21e..439e90cbd22 100644 --- 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 index dc7a14fd911..1f22bf1d4fe 100644 --- 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 index e3558754414..8e68072c81a 100644 --- 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 index 3baacbdd299..1c9befba1ab 100644 --- 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 index 7535bf54fa0..0adccbaeeca 100644 --- 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 index da75fa6938d..1eb0c602802 100644 --- 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 index 5057888a70f..87a82a3c65b 100644 --- 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 index 4b6e6c4ff6b..0169b2b073d 100644 --- 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 index 5b984b25e56..8a77acb30c1 100644 --- 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 index efd0191bcbe..6658ea193cd 100644 --- 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 index 9b3302f432a..db90fccc3c6 100644 --- 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 index 54aa72698e6..841fa18b714 100644 --- 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 index 7a9c919ce04..5e7905ddf56 100644 --- 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 index 4ff90e2c18b..3a9dc44520d 100644 --- 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 index e0fad8a1528..d29594eebd1 100644 --- 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" - "$ --incremental-smt2-solver 'z3 --smt2 -in' --slice-formula" + "$ --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 index ce3a7a84543..64e9659281e 100644 --- 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 index 2681ab20f55..8eb7c3431eb 100644 --- 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 index 9d3ca895383..138811a009e 100644 --- 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" - "$ --incremental-smt2-solver 'z3 --smt2 -in' --slice-formula" + "$ --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 index d4b3dbe7220..13108fb57b8 100644 --- 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 index 706031b1df9..350a589e4a6 100644 --- 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 index 3bb3ae685d6..17695a197ac 100644 --- 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 index d3ffa865d71..6d512daea48 100644 --- 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 -