Skip to content

Commit 17b5913

Browse files
authored
bitwuzla: actually build with cryptominisat support (NixOS#369786)
2 parents 84ed163 + 08ae827 commit 17b5913

File tree

1 file changed

+25
-0
lines changed

1 file changed

+25
-0
lines changed

pkgs/by-name/bi/bitwuzla/package.nix

Lines changed: 25 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -14,6 +14,7 @@
1414
cryptominisat,
1515
zlib,
1616
pkg-config,
17+
cmake,
1718
}:
1819

1920
stdenv.mkDerivation (finalAttrs: {
@@ -34,6 +35,7 @@ stdenv.mkDerivation (finalAttrs: {
3435
pkg-config
3536
git
3637
ninja
38+
cmake
3739
];
3840
buildInputs = [
3941
cadical
@@ -48,6 +50,7 @@ stdenv.mkDerivation (finalAttrs: {
4850
# note: the default value for default_library fails to link dynamic dependencies
4951
# but setting it to shared works even in pkgsStatic
5052
"-Ddefault_library=shared"
53+
"-Dcryptominisat=true"
5154

5255
(lib.strings.mesonEnable "testing" finalAttrs.finalPackage.doCheck)
5356
];
@@ -56,6 +59,28 @@ stdenv.mkDerivation (finalAttrs: {
5659
checkInputs = [ gtest ];
5760
# two tests fail on darwin
5861
doCheck = stdenv.hostPlatform.isLinux;
62+
doInstallCheck = true;
63+
installCheckPhase = ''
64+
runHook preInstallCheck
65+
66+
export needle=11011110101011011011111011101111
67+
68+
cat > file.smt2 <<EOF
69+
(declare-fun a () (_ BitVec 32))
70+
(assert (= a #b$needle))
71+
(check-sat)
72+
(get-model)
73+
EOF
74+
75+
# check each backend
76+
(
77+
set -euxo pipefail;
78+
$out/bin/bitwuzla -S cms -j 3 -m file.smt2 | tee /dev/stderr | grep $needle;
79+
$out/bin/bitwuzla -S cadical -m file.smt2 | tee /dev/stderr | grep $needle;
80+
)
81+
82+
runHook postInstallCheck
83+
'';
5984

6085
meta = {
6186
description = "SMT solver for fixed-size bit-vectors, floating-point arithmetic, arrays, and uninterpreted functions";

0 commit comments

Comments
 (0)