···

       
3
       
3
       
 
       
flags: deprecated

     

       
4
       
4
       
 
       
description: """

     

       
5
       
5
       
 
       


     

       
6
       
6
       
-
       
Standalone installer for the SMT solver Bitwuzla.

     

       
6
       
6
       
+
       
/!\ Deprecated. Standalone installer for the SMT solver Bitwuzla.

     

       
7
       
7
       
+
       
OCaml users should use instead one of the packages bitwuzla, bitwuzla-c or the latest version bitwuzla-cxx to access the Bitwuzla API.

     

       
7
       
8
       
 
       


     

       
8
       
9
       
 
       
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”."""

     

       
9
       
10
       
 
       
maintainer: ["Frédéric Recoules <frederic.recoules@cea.fr>"]

     

···

       
2
       
2
       
 
       
synopsis: "Bitwuzla SMT solver executable"

     

       
3
       
3
       
 
       
description: """

     

       
4
       
4
       
 
       


     

       
5
       
5
       
-
       
Standalone installer for the SMT solver Bitwuzla.

     

       
5
       
5
       
+
       
/!\ Aging. Standalone installer for the SMT solver Bitwuzla.

     

       
6
       
6
       
+
       
OCaml users should use instead one of the packages bitwuzla, bitwuzla-c or the latest version bitwuzla-cxx to access the Bitwuzla API.

     

       
6
       
7
       
 
       


     

       
7
       
8
       
 
       
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”."""

     

       
8
       
9
       
 
       
maintainer: ["Frédéric Recoules <frederic.recoules@cea.fr>"]