From 08ae8278b6f9ebcff0a50aec829e2d7600578945 Mon Sep 17 00:00:00 2001
From: Guillaume Girol <symphorien+git@xlumurb.eu>
Date: Sat, 18 Jan 2025 12:00:00 +0000
Subject: [PATCH] bitwuzla: add simplistic installCheckPhase

---
 pkgs/by-name/bi/bitwuzla/package.nix | 22 ++++++++++++++++++++++
 1 file changed, 22 insertions(+)

diff --git a/pkgs/by-name/bi/bitwuzla/package.nix b/pkgs/by-name/bi/bitwuzla/package.nix
index 2faf3a948406..4fb78ff4e646 100644
--- a/pkgs/by-name/bi/bitwuzla/package.nix
+++ b/pkgs/by-name/bi/bitwuzla/package.nix
@@ -59,6 +59,28 @@ stdenv.mkDerivation (finalAttrs: {
   checkInputs = [ gtest ];
   # two tests fail on darwin
   doCheck = stdenv.hostPlatform.isLinux;
+  doInstallCheck = true;
+  installCheckPhase = ''
+    runHook preInstallCheck
+
+    export needle=11011110101011011011111011101111
+
+    cat > file.smt2 <<EOF
+    (declare-fun a () (_ BitVec 32))
+    (assert (= a #b$needle))
+    (check-sat)
+    (get-model)
+    EOF
+
+    # check each backend
+    (
+    set -euxo pipefail;
+    $out/bin/bitwuzla -S cms -j 3 -m file.smt2 | tee /dev/stderr | grep $needle;
+    $out/bin/bitwuzla -S cadical -m file.smt2 | tee /dev/stderr | grep $needle;
+    )
+
+    runHook postInstallCheck
+  '';
 
   meta = {
     description = "SMT solver for fixed-size bit-vectors, floating-point arithmetic, arrays, and uninterpreted functions";