Use fstar makefiles to run test instead

.github/workflows/smt2.yml

@@ -41,8 +41,8 @@ jobs:
         with:
           ocaml-compiler: 5
 
-      - name: Debugging with tmate
-        uses: mxschmitt/[email protected]
+      # - name: Debugging with tmate
+      #   uses: mxschmitt/[email protected]
 
       - name: Make smt2 files
         run: ./make_smt2.sh

fstar/run.sh

@@ -1,8 +1,21 @@
-FSTAR="$(realpath "$(dirname "$0")")/fstar/bin/fstar.exe"
+Z3_VERSION=$(z3 --version | sed -E 's/.* ([0-9]+\.[0-9]+\.[0-9]+).*/\1/g')
+
+export FSTAR_ROOT="$(realpath "$(dirname "$0")")/fstar"
+# Instead of using "OTHERFLAGS", this is an ugly hack to force our flags to take
+# priority since "HINTS_ENABLED" is last appended in "fstar/mk/test.mk".
+export HINTS_ENABLED=" --z3version \"$Z3_VERSION\" --log_queries "
+# FSTAR_EXE="$FSTAR_ROOT/bin/fstar.exe"
 
 OUT="$(pwd)/$(dirname "$2")"
 mkdir -p "$OUT"
-cd "$OUT"
 
-Z3_VERSION=$(z3 --version | sed -E 's/.* ([0-9]+\.[0-9]+\.[0-9]+).*/\1/g')
-"$FSTAR" --z3version "$Z3_VERSION" --log_queries "$1"
+cd "$(dirname "$1")"
+make clean
+make
+
+while read -r file; do
+    [ -z "$file" ] && continue
+    tgt="$(basename "$file")"
+    tgt="$OUT/${tgt#./}"
+    mv "$file" "$tgt"
+done <<< "$(find . -name "*.smt2" -type f)"

fstar/tests.sh

@@ -1 +1,2 @@
-find "$(realpath "$(dirname "$0")")/fstar/tests" -name "*.fst" -type f
+TESTS="$(realpath "$(dirname "$0")")/fstar/tests"
+find "$TESTS" -name "Makefile" -type f