Give write permissions

.github/workflows/smt2.yml

@@ -6,6 +6,7 @@ on:
 
 permissions:
   contents: write
+  actions: write
 
 jobs:
   generate_smt2:
@@ -23,7 +24,6 @@ jobs:
           git config --global user.name "gh-action[bot]"
           git fetch origin smt2
           git checkout FETCH_HEAD -b smt2
-          git merge -X theirs main
           git checkout main
 
       - name: Install Z3 for newer version
@@ -46,9 +46,17 @@ jobs:
       # - name: Debugging with tmate
       #   uses: mxschmitt/action-tmate@v3.19
 
+      - name: Merge in from main
+        run: |
+          git stash
+          git checkout smt2
+          git merge -X theirs main
+          git checkout main
+          git stash show && git stash pop || true
+
       - name: Commit changes
         run: |
           git symbolic-ref HEAD refs/heads/smt2
           git add -A
-          git diff-index --quiet HEAD || git commit -m "Update from main and rebuild \".smt2\" files"
+          git diff-index --quiet HEAD || git commit -m "Rebuild \".smt2\" files with new main"
           git push -u origin smt2

dafny/run.sh

@@ -2,11 +2,12 @@ OUT="$(pwd)/$(echo "${2%.*}" | sed 's/ /_/g')"
 mkdir -p "$(dirname "$OUT")"
 
 cd "$(dirname "$0")/dafny"
-Binaries/Dafny /deprecation:0 /compile:0 /timeLimit:$3 /print:$OUT.bpl /vcsCores:1 /proverLog:$OUT-@PROC@.smt2 "$1" > /dev/null
+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
     exit 0
 else
+    echo "[ERROR] $OUTPUT"
     exit 1
 fi

make_smt2.sh

@@ -6,6 +6,8 @@ if [ -z "$VERIFIERS" ]; then
     VERIFIERS="dafny silicon carbon"
 fi
 
+exit 0
+
 git submodule update --init --recursive &> /dev/null
 
 DIRNAME=$(realpath "$0" | xargs dirname)