Skip to content

Commit 261131c

Browse files
committed
Revert "Add --no-standard-checks to regression/cbmc-sequentialization test runner scripts"
This reverts commit f79b5bc.
1 parent 93439b5 commit 261131c

File tree

2 files changed

+3
-3
lines changed

2 files changed

+3
-3
lines changed
Original file line numberDiff line numberDiff line change
@@ -1,10 +1,10 @@
11
if(NOT WIN32)
22
add_test_pl_tests(
3-
"$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation"
3+
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
44
)
55
else()
66
add_test_pl_tests(
7-
"$<TARGET_FILE:cbmc> --no-standard-checks --validate-goto-model --validate-ssa-equation"
7+
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation"
88
-X requires_posix_only_headers
99
)
1010
endif()

regression/cbmc-sequentialization/Makefile

+1-1
Original file line numberDiff line numberDiff line change
@@ -10,7 +10,7 @@ POSIX_ONLY =
1010
endif
1111

1212
test:
13-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --no-standard-checks --validate-goto-model --validate-ssa-equation" $(POSIX_ONLY)
13+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation" $(POSIX_ONLY)
1414

1515
tests.log: ../test.pl test
1616

0 commit comments

Comments
 (0)