From ff48795ee407ec43c62f374092a798879ea08e49 Mon Sep 17 00:00:00 2001 From: Michael Tautschnig Date: Tue, 20 Feb 2024 09:51:33 +0000 Subject: [PATCH] Make regression tests work when cvc5 is not available We should not have cvc5 as firm build (and test) dependency as CBMC works just fine when cvc5 is not available. --- regression/cbmc-incr-smt2/Makefile | 4 +++- regression/cbmc-output-file/Makefile | 8 ++++++-- 2 files changed, 9 insertions(+), 3 deletions(-) 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 \