From d704b289efc8cbcb69eb32dc7cd0a8f14fdb3f2b Mon Sep 17 00:00:00 2001
From: Lev Nachmanson <levnach@hotmail.com>
Date: Sat, 27 Jun 2026 08:45:19 -0700
Subject: [PATCH] Add local pre-commit hook running z3test regressions

Adds a versioned .githooks/pre-commit that builds z3 and runs the
z3test regression suite (scripts/test_benchmarks.py over
regressions/smt2) as a precondition for every commit. Enable with
'git config core.hooksPath .githooks'.

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 .githooks/README.md  | 27 +++++++++++++++++++++
 .githooks/pre-commit | 58 ++++++++++++++++++++++++++++++++++++++++++++
 2 files changed, 85 insertions(+)
 create mode 100644 .githooks/README.md
 create mode 100755 .githooks/pre-commit

diff --git a/.githooks/README.md b/.githooks/README.md
new file mode 100644
index 0000000000..c3a6fb0d34
--- /dev/null
+++ b/.githooks/README.md
@@ -0,0 +1,27 @@
+# Git hooks
+
+Versioned git hooks for this repository.
+
+## pre-commit
+
+Builds the `z3` binary and runs the [z3test](https://github.com/Z3Prover/z3test)
+regression suite (`scripts/test_benchmarks.py` over `regressions/smt2`) locally.
+The commit is aborted if the build or any regression fails.
+
+### Enable
+
+```bash
+git config core.hooksPath .githooks
+```
+
+### Configuration (environment variables)
+
+- `Z3_BUILD_DIR` — build directory to use/create (default: `build/release`).
+- `Z3TEST_DIR` — existing `z3test` checkout. If unset, `z3test` is cloned into
+  `../z3test-precommit` next to the repository.
+
+### Skip for a single commit
+
+```bash
+git commit --no-verify
+```
diff --git a/.githooks/pre-commit b/.githooks/pre-commit
new file mode 100755
index 0000000000..d22cbac76d
--- /dev/null
+++ b/.githooks/pre-commit
@@ -0,0 +1,58 @@
+#!/usr/bin/env bash
+#
+# Pre-commit hook: build Z3 and run the z3test regression suite locally as a
+# precondition for every commit. The commit is aborted if the build or any
+# regression test fails.
+#
+# It builds the `z3` binary, then runs:
+#     python z3test/scripts/test_benchmarks.py <z3> z3test/regressions/smt2
+#
+# Enable for this clone with:
+#     git config core.hooksPath .githooks
+#
+# Configuration (environment variables):
+#   Z3_BUILD_DIR   Build directory to use/create. Default: build/release
+#   Z3TEST_DIR     Existing z3test checkout. If unset, z3test is cloned into
+#                  a cache dir next to the repo (../z3test-precommit).
+#
+# Skip the hook for a one-off commit with:
+#     git commit --no-verify
+
+set -euo pipefail
+
+REPO_ROOT="$(git rev-parse --show-toplevel)"
+cd "$REPO_ROOT"
+
+BUILD_DIR="${Z3_BUILD_DIR:-build/release}"
+Z3TEST_DIR="${Z3TEST_DIR:-$REPO_ROOT/../z3test-precommit}"
+
+# --- Build the z3 binary -----------------------------------------------------
+echo "[pre-commit] Building z3 in '$BUILD_DIR'..."
+if [ ! -f "$BUILD_DIR/build.ninja" ] && [ ! -f "$BUILD_DIR/Makefile" ]; then
+    echo "[pre-commit] Configuring CMake build in '$BUILD_DIR'..."
+    cmake -G Ninja -S . -B "$BUILD_DIR" -DCMAKE_BUILD_TYPE=Release
+fi
+cmake --build "$BUILD_DIR" --target z3
+
+Z3_BIN="$BUILD_DIR/z3"
+if [ ! -x "$Z3_BIN" ]; then
+    echo "[pre-commit] ERROR: z3 binary not found at '$Z3_BIN'." >&2
+    exit 1
+fi
+
+# --- Ensure a z3test checkout is available -----------------------------------
+if [ ! -d "$Z3TEST_DIR/regressions/smt2" ]; then
+    if [ -d "$Z3TEST_DIR/.git" ]; then
+        echo "[pre-commit] Updating z3test checkout in '$Z3TEST_DIR'..."
+        git -C "$Z3TEST_DIR" pull --ff-only || true
+    else
+        echo "[pre-commit] Cloning z3test into '$Z3TEST_DIR'..."
+        git clone --depth 1 https://github.com/Z3Prover/z3test "$Z3TEST_DIR"
+    fi
+fi
+
+# --- Run the regression suite ------------------------------------------------
+echo "[pre-commit] Running regressions on z3test/regressions/smt2..."
+python "$Z3TEST_DIR/scripts/test_benchmarks.py" "$Z3_BIN" "$Z3TEST_DIR/regressions/smt2"
+
+echo "[pre-commit] Regressions passed."