···
+
synopsis: "Bitwuzla SMT solver executable"
+
Standalone installer for the SMT solver Bitwuzla.
+
Bitwuzla is a Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions and their combinations. Its name is derived from an Austrian dialect expression that can be translated as “someone who tinkers with bits”."""
+
maintainer: ["Frédéric Recoules <frederic.recoules@cea.fr>"]
+
authors: ["Frédéric Recoules"]
+
tags: ["SMT solver" "SMT-COMP 2020" "AUFBVFP"]
+
homepage: "https://bitwuzla.github.io"
+
bug-reports: "https://github.com/bitwuzla/bitwuzla/issues"
+
[ "sh" "-c" "cd vendor/cadical && ./configure -fPIC" ]
+
[ make "-j" jobs "-C" "vendor/cadical/build" ]
+
[ "sh" "-c" "cd vendor/btor2tools && ./configure.sh" ]
+
[ make "-j" jobs "-C" "vendor/btor2tools/build" ]
+
[ "sh" "-c" "patch -p1 --directory vendor/symfpu \
+
< vendor/bitwuzla/contrib/symfpu_20201114.patch" ]
+
"export LDFLAGS='-Wl,-rpath=$ORIGIN/../lib' && \
+
cd vendor/bitwuzla && ./configure.sh \
+
--no-testing --shared --only-cadical \
+
--path ../cadical/src \
+
--path ../cadical/build \
+
--path ../btor2tools/src/btor2parser \
+
--path ../btor2tools/build/lib \
+
[ make "-j" jobs "-C" "vendor/bitwuzla/build" ]
+
[ "install" "vendor/btor2tools/build/lib/libbtor2parser.so" lib ]
+
[ make "install" "-j" jobs "-C" "vendor/bitwuzla/build" ]
+
dev-repo: "git+https://github.com/bitwuzla/ocaml-bitwuzla.git"
+
available: [ os = "linux" & (os-distribution != "ol" & os-distribution != "centos" | os-version >= 8) ]
+
x-commit-hash: "6dd263d8147829badd3c3c134293dc6be8d29ea9"
+
"https://github.com/bitwuzla/ocaml-bitwuzla/releases/download/1.0.0/bitwuzla-1.0.0.tbz"
+
"sha256=004ccb630a070829fedcbaf071fc50f5c7df2e5f47d2016e228ab775df6961d8"
+
"sha512=9a3d46b0a0379228a17f9d5f88cf7c409eab7c72d9296a939bc254120bc89ede9471d0930f8d2f70463e99e627649e56e54556ed2f008a3800f9387a6959674a"