Unverified Commit 17b59136 authored by Guillaume Girol's avatar Guillaume Girol Committed by GitHub
Browse files

bitwuzla: actually build with cryptominisat support (#369786)

parents 84ed163a 08ae8278

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

+25 −0
Original line number Diff line number Diff line
@@ -14,6 +14,7 @@ 
  cryptominisat,

  zlib,

  pkg-config,

  cmake,

}:



stdenv.mkDerivation (finalAttrs: {
@@ -34,6 +35,7 @@ stdenv.mkDerivation (finalAttrs: { 
    pkg-config

    git

    ninja

    cmake

  ];

  buildInputs = [

    cadical
@@ -48,6 +50,7 @@ stdenv.mkDerivation (finalAttrs: { 
    # note: the default value for default_library fails to link dynamic dependencies

    # but setting it to shared works even in pkgsStatic

    "-Ddefault_library=shared"

    "-Dcryptominisat=true"



    (lib.strings.mesonEnable "testing" finalAttrs.finalPackage.doCheck)

  ];
@@ -56,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";