what4 1.7.2 → 1.7.3

raw patch · 4 files changed

+26/−3 lines, 4 files

Files

• CHANGES.md +5/−0
• src/What4/Protocol/SMTWriter.hs +2/−1
• test/ExprBuilderSMTLib2.hs +18/−1
• what4.cabal +1/−1

@@ -1,3 +1,8 @@+# 1.7.3 -- 2026-01-26++* Fix a bug in which `what4`'s Bitwuzla adapter would generate invalid code+  involving SMT arrays.+ # 1.7.2 (November 2025)  * Fix a regression in `what4-1.7.1` in which `sbvToInteger` could compute

@@ -1166,7 +1166,8 @@   ComplexToArrayTypeMap  -> return ()   PrimArrayTypeMap args ret ->     do traverseFC_ (declareTypes conn) args-       declareStructDatatype conn args+       when (supportedFeatures conn `hasProblemFeature` useStructs) $+         declareStructDatatype conn args        declareTypes conn ret   FnArrayTypeMap args ret ->     do traverseFC_ (declareTypes conn) args

@@ -52,6 +52,7 @@ import           What4.Protocol.SMTLib2 import           What4.SatResult import           What4.Solver.Adapter+import qualified What4.Solver.Bitwuzla as Bitwuzla import qualified What4.Solver.CVC4 as CVC4 import qualified What4.Solver.CVC5 as CVC5 import qualified What4.Solver.Z3 as Z3@@ -141,6 +142,18 @@     (\(h,s) -> void $ try @SomeException (shutdownSolverProcess s `finally` maybeClose h))     (\(_,s) -> action sym s) +withBitwuzla+  :: (forall t . SimpleExprBuilder t (Flags FloatReal) -> SolverProcess t (Writer Bitwuzla.Bitwuzla) -> IO a)+  -> IO a+withBitwuzla action = withSym FloatRealRepr $ \sym -> do+  extendConfig Bitwuzla.bitwuzlaOptions (getConfiguration sym)+  bracket+    (do h <- if debugOutputFiles then Just <$> openFile "bitwuzla.out" WriteMode else return Nothing+        s <- startSolverProcess (defaultFeatures Bitwuzla.Bitwuzla) h sym+        return (h,s))+    (\(h,s) -> void $ try @SomeException (shutdownSolverProcess s `finally` maybeClose h))+    (\(_,s) -> action sym s)+ withModel   :: Session t Z3.Z3   -> BoolExpr t@@ -1260,7 +1273,7 @@ main :: IO () main = do   testLevel <- TestLevel . fromMaybe "0" <$> lookupEnv "CI_TEST_LEVEL"-  let solverNames = SolverName <$> [ "cvc4", "cvc5", "yices", "z3" ]+  let solverNames = SolverName <$> [ "bitwuzla", "cvc4", "cvc5", "yices", "z3" ]   solvers <- reportSolverVersions testLevel id              =<< (zip solverNames <$> mapM getSolverVersion solverNames)   let z3Tests =@@ -1380,6 +1393,9 @@         , testCase "Yices #315 test case" $ withYices issue315Test         , testCase "Yices #329 test case" $ withYices issue329Test         ]+  let bitwuzlaTests =+        [ testCase "Bitwuzla multidim array" $ withBitwuzla multidimArrayTest+        ]   let skipIfNotPresent nm = if SolverName nm `elem` (fst <$> solvers) then id                             else fmap (ignoreTestBecause (nm <> " not present"))   defaultMain $ testGroup "Tests" $@@ -1399,6 +1415,7 @@     , testUnsafeSetAbstractValue1     , testUnsafeSetAbstractValue2     ]+    <> (skipIfNotPresent "bitwuzla" bitwuzlaTests)     <> (skipIfNotPresent "cvc4" cvc4Tests)     <> (skipIfNotPresent "cvc5" cvc5Tests)     <> (skipIfNotPresent "yices" yicesTests)

@@ -1,6 +1,6 @@ Cabal-version: 2.4 Name:          what4-Version:       1.7.2+Version:       1.7.3 Author:        Galois Inc. Maintainer:    rscott@galois.com, kquick@galois.com Copyright:     (c) Galois, Inc 2014-2023