Skip to content

Commit 022f674

Browse files
author
Enrico Steffinlongo
committed
Add working cbmc-primitives regressions with SMT2
1 parent 3559b7b commit 022f674

File tree

6 files changed

+6
-6
lines changed

6 files changed

+6
-6
lines changed

regression/cbmc-primitives/exists_assume_6231/test2.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
test2.c
33
--pointer-check
44
^EXIT=10$

regression/cbmc-primitives/implication_statement_checks_1/test.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
--div-by-zero-check
33
test.c
44
^EXIT=0$

regression/cbmc-primitives/r_w_ok_valid/test-no-cp.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
main.c
33
--pointer-check --no-simplify --no-propagation
44
^EXIT=0$

regression/cbmc-primitives/same-object-01/test-no-cp.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
main.c
33
--no-simplify --no-propagation
44
^EXIT=0$

regression/cbmc-primitives/same-object-02/test-no-cp.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
main.c
33
--no-simplify --no-propagation
44
^EXIT=0$

regression/cbmc-primitives/same-object-04/test-no-cp.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
main.c
33
--no-simplify --no-propagation
44
^EXIT=0$

0 commit comments

Comments
 (0)