Skip to content

Commit 00e03cb

Browse files
committed
Enable SMT solver tests fixed by rudimentary struct support
These tests now pass due to the functionality added in PR7740.
1 parent 683b8ba commit 00e03cb

File tree

9 files changed

+9
-9
lines changed

9 files changed

+9
-9
lines changed

regression/cbmc/Endianness7/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
main.c
33
--big-endian --no-simplify
44
^EXIT=0$

regression/cbmc/Malloc13/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
main.c
33
--string-abstraction
44
^EXIT=0$

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

regression/cbmc/String_Abstraction24/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
main.c
33
--string-abstraction
44
^VERIFICATION FAILED$

regression/cbmc/equality_through_array_of_struct1/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
main.c
33

44
^EXIT=0$

regression/cbmc/equality_through_array_of_struct2/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
main.c
33

44
^EXIT=0$

regression/cbmc/equality_through_array_of_struct3/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
main.c
33

44
^EXIT=0$

regression/cbmc/equality_through_array_of_struct4/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
main.c
33

44
^EXIT=0$

regression/cbmc/offsetof1/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
main.c
33

44
^EXIT=0$

0 commit comments

Comments
 (0)