Skip to content

Commit 6f9fb2b

Browse files
committed
Use -X broken-smt-backend instead of deleting files
This actually simplifies our CI scripts.
1 parent 21d0c8a commit 6f9fb2b

File tree

5 files changed

+2
-91
lines changed

5 files changed

+2
-91
lines changed

.travis.yml

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -304,7 +304,7 @@ script:
304304
- if [ -e bin/gcc ] ; then export PATH=$PWD/bin:$PATH ; fi ;
305305
- env UBSAN_OPTIONS=print_stacktrace=1 make -C regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2
306306
- UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-paths-lifo
307-
- scripts/delete_failing_smt2_solver_tests ; env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
307+
- env PATH=$PATH:`pwd`/src/solvers UBSAN_OPTIONS=print_stacktrace=1 make -C regression/cbmc test-cprover-smt2
308308
- make -C unit "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2
309309
- make -C unit test
310310
- env UBSAN_OPTIONS=print_stacktrace=1 make -C jbmc/regression test-parallel "CXX=${COMPILER} ${EXTRA_CXXFLAGS}" -j2 JOBS=2

buildspec-linux-clang.yml

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -22,7 +22,6 @@ phases:
2222
commands:
2323
- make -C unit test CXX='ccache /usr/bin/clang++-7' CXX_FLAGS='-Qunused-arguments'
2424
- make -C regression test
25-
- scripts/delete_failing_smt2_solver_tests
2625
- env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
2726
- make -C jbmc/unit test CXX='ccache /usr/bin/clang++-7' CXX_FLAGS='-Qunused-arguments'
2827
- make -C jbmc/regression test

buildspec.yml

Lines changed: 0 additions & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -26,7 +26,6 @@ phases:
2626
- make -C unit test
2727
- make -C regression test
2828
- make -C regression/cbmc test-paths-lifo
29-
- scripts/delete_failing_smt2_solver_tests
3029
- env PATH=$PATH:`pwd`/src/solvers make -C regression/cbmc test-cprover-smt2
3130
- make -C jbmc/unit test
3231
- make -C jbmc/regression test

regression/cbmc/Makefile

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -4,7 +4,7 @@ test:
44
@../test.pl -p -c "../../../src/cbmc/cbmc --validate-goto-model" -X smt-backend
55

66
test-cprover-smt2:
7-
@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2"
7+
@../test.pl -p -c "../../../src/cbmc/cbmc --cprover-smt2" -X broken-smt-backend
88

99
test-paths-lifo:
1010
@../test.pl -p -c "../../../src/cbmc/cbmc --paths lifo" -X thorough-paths -X smt-backend

scripts/delete_failing_smt2_solver_tests

Lines changed: 0 additions & 87 deletions
This file was deleted.

0 commit comments

Comments
 (0)