From fe661270c22816f64239358dd6df7720e994c410 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Jon=C3=A1=C5=A1=20Fiala?= <jonas.fiala@inf.ethz.ch>
Date: Thu, 26 Dec 2024 15:52:53 +0100
Subject: [PATCH] Fix dafny

---
 .github/workflows/smt2.yml |  1 +
 dafny/run.sh               | 15 +++++++++------
 make_smt2.sh               |  2 +-
 3 files changed, 11 insertions(+), 7 deletions(-)

diff --git a/.github/workflows/smt2.yml b/.github/workflows/smt2.yml
index aeec01871..055694d6f 100644
--- a/.github/workflows/smt2.yml
+++ b/.github/workflows/smt2.yml
@@ -50,6 +50,7 @@ jobs:
         run: |
           git stash
           git checkout smt2
+          git pull
           git merge -X theirs main
           git checkout main
           git stash show && git stash pop || true
diff --git a/dafny/run.sh b/dafny/run.sh
index 1e17f88d5..9619b100c 100755
--- a/dafny/run.sh
+++ b/dafny/run.sh
@@ -3,11 +3,14 @@ mkdir -p "$(dirname "$OUT")"
 
 cd "$(dirname "$0")/dafny"
 OUTPUT=$(Binaries/Dafny /deprecation:0 /compile:0 /timeLimit:$3 /print:$OUT.bpl /vcsCores:1 /proverLog:$OUT-@PROC@.smt2 "$1")
-
-# Check if "$1.expect" exists and if so if it contains " Error:", then it's ok for the above to fail
-if [ $? -eq 0 ] || ([ -f "$1.expect" ] && grep -q " Error:" "$1.expect"); then
+if [ $? -eq 0 ]; then
     exit 0
-else
-    echo "[ERROR] $OUTPUT"
-    exit 1
 fi
+while read -r out_line; do
+    # Return error if the output line contains " Error:" but does not start with
+    # the filename. This means it's not a verification error pointing to the file.
+    if grep -q " Error:" <<< "$out_line" && ! [[ "$1" =~ "$(echo "$out_line" | sed "s|\.dfy.*|.dfy|g")" ]]; then
+        echo "[ERROR] $OUTPUT"
+        exit 1
+    fi
+done <<< "$OUTPUT"
diff --git a/make_smt2.sh b/make_smt2.sh
index d37a9be21..5285383ce 100755
--- a/make_smt2.sh
+++ b/make_smt2.sh
@@ -3,7 +3,7 @@
 
 VERIFIERS="$@"
 if [ -z "$VERIFIERS" ]; then
-    VERIFIERS="silicon carbon"
+    VERIFIERS="dafny silicon carbon"
 fi
 
 git submodule update --init --recursive &> /dev/null