Skip to content

Commit 496fe33

Browse files
committed
Fix combination of new-smt-backend and gcc-only test tags
Tests which were tagged with both `new-smt-backend` and `gcc-only` would previously be executed on Windows with Visual Studio test jobs. The `gcc-only` tag is used when tests cover features which are not supported by Visual Studio. Therefore running them with Visual Studio is a an error on the part of the test framework, rather than representative of an issue with cbmc. Propagating `gcc_only_string` to the addition of the `new-smt-backend` test profile will switch off running these tests for the Visual Studio platform only.
1 parent 2c1a38e commit 496fe33

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

regression/cbmc/CMakeLists.txt

+1-1
Original file line numberDiff line numberDiff line change
@@ -34,7 +34,7 @@ add_test_pl_profile(
3434
add_test_pl_profile(
3535
"cbmc-new-smt-backend"
3636
"$<TARGET_FILE:cbmc> --incremental-smt2-solver 'z3 --smt2 -in'"
37-
"-I;new-smt-backend;-s;new-smt-backend"
37+
"${gcc_only_string}-I;new-smt-backend;-s;new-smt-backend"
3838
"CORE"
3939
)
4040

0 commit comments

Comments
 (0)