diff --git a/regression/cbmc-incr-smt2/Makefile b/regression/cbmc-incr-smt2/Makefile index 9a5b8bf4195..1c910bce8c3 100644 --- a/regression/cbmc-incr-smt2/Makefile +++ b/regression/cbmc-incr-smt2/Makefile @@ -9,7 +9,9 @@ test.z3: @../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'z3 --smt2 -in' --validate-goto-model --validate-ssa-equation" test.cvc5: - @../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation" + @if which cvc5 ; then \ + ../test.pl -e -p -c "../../../src/cbmc/cbmc --incremental-smt2-solver 'cvc5 --lang=smtlib2.6 --incremental' --validate-goto-model --validate-ssa-equation" ; \ + fi tests.log: ../test.pl test diff --git a/regression/cbmc-output-file/Makefile b/regression/cbmc-output-file/Makefile index a90c84526a9..7fe769a7e07 100644 --- a/regression/cbmc-output-file/Makefile +++ b/regression/cbmc-output-file/Makefile @@ -4,10 +4,14 @@ include ../../src/config.inc include ../../src/common test: - @../test.pl -f -e -p -c '../chain.py ../../../src/cbmc/cbmc' + @if which cvc5 ; then \ + ../test.pl -f -e -p -c '../chain.py ../../../src/cbmc/cbmc' ; \ + fi tests.log: - @../test.pl -f -e -p -c '../chain.py ../../../src/cbmc/cbmc' + @if which cvc5 ; then \ + ../test.pl -f -e -p -c '../chain.py ../../../src/cbmc/cbmc' ; \ + fi clean: @for dir in *; do \