diff --git a/.gitignore b/.gitignore index 397b4a762..d8515b806 100644 --- a/.gitignore +++ b/.gitignore @@ -1 +1,2 @@ *.log +_opam diff --git a/verus/run.sh b/verus/run.sh index 89473584e..d1f3c00b3 100755 --- a/verus/run.sh +++ b/verus/run.sh @@ -3,11 +3,16 @@ OUT="$(pwd)/$(echo "${OP[0]%.*}" | sed 's/ /_/g')/${OP[1]}" mkdir -p "$(dirname "$OUT")" cd "$(dirname "$0")/verus/source" +VARGO="../tools/vargo/target/release/vargo" export VERUS_EXTRA_ARGS="--log-dir $OUT --log smt --rlimit $3" export VARGO_IN_NEXTEST=true TEST=($1) FILE=${TEST[0]#$(pwd)/rust_verify_test/tests/} -vargo test --package rust_verify_test --test ${FILE%.*} -- ${TEST[1]} --exact &> /dev/null || exit 1 +OUTPUT=$($VARGO test --release --package rust_verify_test --test ${FILE%.*} -- ${TEST[1]} --exact 2>&1) +if [ $? -ne 0 ]; then + echo "[ERROR] $OUTPUT" + exit 1 +fi if [ -f "$OUT/root.smt2" ]; then mv "$OUT/root.smt2" "$OUT.smt2" rmdir "$OUT" || true