Skip to content

Commit fef8eda

Browse files
author
Owen
committed
Create paths-lifo-expected-failure tag for tests
Test which rely on convergence will not work with path-symex
1 parent a139e1d commit fef8eda

File tree

2 files changed

+2
-2
lines changed

2 files changed

+2
-2
lines changed

regression/cbmc/CMakeLists.txt

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -5,7 +5,7 @@ add_test_pl_tests(
55
add_test_pl_profile(
66
"cbmc-paths-lifo"
77
"$<TARGET_FILE:cbmc> --paths lifo"
8-
"-C;-X;thorough-paths;-X;smt-backend;-s;paths-lifo"
8+
"-C;-X;thorough-paths;-X;smt-backend;-X;paths-lifo-expected-failure;-s;paths-lifo"
99
"CORE"
1010
)
1111

regression/cbmc/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -7,7 +7,7 @@ test-cprover-smt2:
77
@../test.pl -e -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend
88

99
test-paths-lifo:
10-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend
10+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend -X paths-lifo-expected-failure
1111

1212
tests.log: ../test.pl test
1313

0 commit comments

Comments
 (0)