From f23f2c420324073bbad3ffe10f4b531158232c1f Mon Sep 17 00:00:00 2001
From: Levent Erkok <erkokl@gmail.com>
Date: Wed, 21 Aug 2024 16:08:13 -0700
Subject: [PATCH] Support floats and uninterpreted sorts in Bitwuzla

---
 CHANGES.md                   | 4 ++++
 Data/SBV/Provers/Bitwuzla.hs | 4 ++--
 2 files changed, 6 insertions(+), 2 deletions(-)

diff --git a/CHANGES.md b/CHANGES.md
index e9396fa28..90cf52875 100644
--- 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
index 61bd069dc..8b5103108 100644
--- 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