Skip to content

Commit 5f01e32

Browse files
committed
Disable running incremental smt2 tests on Windows
These tests currently fail when run on Windows due to issues with `piped_processt`. This commit can be reverted once the debugging is complete.
1 parent 74a83f7 commit 5f01e32

File tree

4 files changed

+16
-4
lines changed

4 files changed

+16
-4
lines changed
Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,10 @@
11

2+
if("${CMAKE_SYSTEM_NAME}" STREQUAL "Windows")
3+
set(exclude_win_broken_tests -X winbug)
4+
else()
5+
set(exclude_win_broken_tests "")
6+
endif()
7+
28
add_test_pl_tests(
3-
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --slice-formula"
9+
"$<TARGET_FILE:cbmc> --validate-goto-model --validate-ssa-equation --slice-formula" ${exclude_win_broken_tests}
410
)

regression/cbmc-incr-smt2/Makefile

Lines changed: 7 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -3,8 +3,14 @@ default: test
33
include ../../src/config.inc
44
include ../../src/common
55

6+
ifeq ($(BUILD_ENV_),MSVC)
7+
exclude_broken_windows_tests=-X winbug
8+
else
9+
exclude_broken_windows_tests=
10+
endif
11+
612
test:
7-
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --slice-formula"
13+
@../test.pl -e -p -c "../../../src/cbmc/cbmc --validate-goto-model --validate-ssa-equation --slice-formula" $(exclude_broken_windows_tests)
814

915
tests.log: ../test.pl test
1016

regression/cbmc-incr-smt2/nondeterministic-int-assert/control_flow.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE winbug
22
control_flow.c
33
--incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
44
Passing problem to incremental SMT2 solving via "z3 --smt2 -in"

regression/cbmc-incr-smt2/nondeterministic-int-assert/incremental_solver_called.desc

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,4 +1,4 @@
1-
CORE
1+
CORE winbug
22
test.c
33
--incremental-smt2-solver "z3 --smt2 -in" --verbosity 10
44
Passing problem to incremental SMT2 solving via "z3 --smt2 -in"

0 commit comments

Comments
 (0)