Verus error handling

viperproject · Dec 29, 2024 · 893cdbd · 893cdbd
1 parent 2e04489
commit 893cdbd
Show file tree

Hide file tree

Showing 2 changed files with 7 additions and 3 deletions.
diff --git a/.github/workflows/smt2.yml b/.github/workflows/smt2.yml
@@ -41,8 +41,8 @@ jobs:
         with:
           ocaml-compiler: 5
 
-      # - name: Debugging with tmate
-      #   uses: mxschmitt/action-tmate@v3.19
+      - name: Debugging with tmate
+        uses: mxschmitt/action-tmate@v3.19
 
       - name: Make smt2 files
         run: ./make_smt2.sh

diff --git a/verus/run.sh b/verus/run.sh
@@ -7,7 +7,11 @@ 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 --package rust_verify_test --test ${FILE%.*} -- ${TEST[1]} --exact)
+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