Skip to content

Commit 03f93ef

Browse files
thomasspriggsthomasspriggs
authored
Merge pull request #8002 from thomasspriggs/tas/smt-test-flip
Replace `new-smt-backend` tag with inverted `no-new-smt` tag
2 parents a8de0b7 + 4590da1 commit 03f93ef

File tree

1,125 files changed

+1128
-1128
lines changed

Some content is hidden

Large Commits have some content hidden by default. Use the searchbox below for content that may be hidden.

1,125 files changed

+1128
-1128
lines changed

‎regression/book-examples/CMakeLists.txt

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -30,11 +30,11 @@ add_test_pl_profile(
3030
"CORE"
3131
)
3232

33-
# If `-I` (include flag) is passed, test.pl will run only the tests matching the label following it.
33+
# If `-X` (exclude flag) is passed, test.pl will exclude the tests matching the label following it.
3434
add_test_pl_profile(
3535
"book-examples-new-smt-backend"
3636
"$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
37-
"${gcc_only_string}-I;new-smt-backend;-s;new-smt-backend"
37+
"${gcc_only_string}-X;no-new-smt;-s;new-smt-backend"
3838
"CORE"
3939
)
4040

‎regression/book-examples/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -31,7 +31,7 @@ test-paths-lifo:
3131

3232
test-new-smt-backend:
3333
@../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in'" \
34-
-I new-smt-backend \
34+
-X no-new-smt \
3535
-s new-smt-backend $(GCC_ONLY)
3636

3737
tests.log: ../test.pl test

‎regression/book-examples/abs/C1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
abs.c
33
--function abs
44
^EXIT=0$

‎regression/book-examples/abs/C13.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
abs.c
33
--function abs --signed-overflow-check --show-goto-functions
44
^EXIT=0$

‎regression/book-examples/abs/C2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
abs.c
33
--function abs --signed-overflow-check
44
^EXIT=10$

‎regression/book-examples/abs/C3.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
abs.c
33
--function abs --signed-overflow-check --trace
44
^EXIT=10$

‎regression/book-examples/binsearch/C4.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
binsearch.c
33
--function binsearch --unwind 6 --bounds-check --unwinding-assertions
44
^EXIT=0$

‎regression/book-examples/lock/depth.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
lock.c
33
--depth 10
44
^EXIT=0$

‎regression/book-examples/lock/unwind1.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
lock.c
33
--unwind 1
44
^EXIT=0$

‎regression/book-examples/lock/unwind2.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE new-smt-backend
1+
CORE
22
lock.c
33
--unwind 2
44
^EXIT=10$

0 commit comments

Comments
 (0)