Support floats and uninterpreted sorts in Bitwuzla

LeventErkok · Aug 21, 2024 · f23f2c4 · f23f2c4
1 parent 922049f
commit f23f2c4
Show file tree

Hide file tree

Showing 2 changed files with 6 additions and 2 deletions.
diff --git a/CHANGES.md b/CHANGES.md
@@ -1,6 +1,10 @@
 * Hackage: <http://hackage.haskell.org/package/sbv>
 * GitHub:  <http://github.com/LeventErkok/sbv>
 
+### Version 10.12.5, Not yet released
+
+  * Turn on support for floats and uninterpreted sorts/functions in Bitwuzla.
+
 ### Version 10.12, 2024-08-11
 
   * Fix a few custom-floating-point format conversion bugs. Thanks to Sirui Lu for the patch.

diff --git a/Data/SBV/Provers/Bitwuzla.hs b/Data/SBV/Provers/Bitwuzla.hs
@@ -31,13 +31,13 @@ bitwuzla = SMTSolver {
                               , supportsDefineFun          = True
                               , supportsDistinct           = True
                               , supportsBitVectors         = True
-                              , supportsUninterpretedSorts = False
+                              , supportsUninterpretedSorts = True
                               , supportsUnboundedInts      = False
                               , supportsInt2bv             = False
                               , supportsReals              = False
                               , supportsApproxReals        = False
                               , supportsDeltaSat           = Nothing
-                              , supportsIEEE754            = False
+                              , supportsIEEE754            = True
                               , supportsSets               = False
                               , supportsOptimization       = False
                               , supportsPseudoBooleans     = False