bitwuzla: add simplistic installCheckPhase
This commit is contained in:
@@ -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";
|
||||
|
||||
Reference in New Issue
Block a user