Skip to content

Commit a42b439

Browse files
committed
Add new-smt-backend tag to book regression test which pass
If we are going to support this tag in the `cmakelists.txt` for the book examples, then we may as well run some of the tests with it.
1 parent 43a86ca commit a42b439

File tree

13 files changed

+13
-13
lines changed

13 files changed

+13
-13
lines changed

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
1+
CORE new-smt-backend
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
1+
CORE new-smt-backend
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
1+
CORE new-smt-backend
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
1+
CORE new-smt-backend
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
1+
CORE new-smt-backend
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
1+
CORE new-smt-backend
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
1+
CORE new-smt-backend
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
1+
CORE new-smt-backend
22
lock.c
33
--unwind 2
44
^EXIT=10$

regression/book-examples/login/C5.desc

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

regression/book-examples/login/C6.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE new-smt-backend
22
login.c
33
--show-properties --bounds-check --pointer-check
44
^EXIT=0$

regression/book-examples/login/C7.desc

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

regression/book-examples/login/C8.desc

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

regression/book-examples/login/C9.desc

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

0 commit comments

Comments
 (0)