sbv v8.10 Release Notes

Release Date: 2021-02-13 // over 1 year ago
    • Add "Documentation/SBV/Examples/Misc/NestedArray.hs" to demonstrate how to model multi-dimensional arrays in SBV.

    • Add "Documentation/SBV/Examples/Puzzles/Murder.hs" as another puzzle example.

    • Performance updates: Thanks to Jeff Young, SBV now uses better underlying data structures, performing better for heavy use-case scenarios.

    • SBV now tracks constants more closely in query mode, providing more support for constant arrays in a seamless way. (See #574 for details.)

    • Pop-calls are now support for Yices and Boolector. (#577)

    • Changes required to make SBV work with latest version of z3 regarding String and Characters, which now allow for unicode characters. This required renaming of certain recognizers in 'Data.SBV.Char' to restrict them to the Latin1 subset. Otherwise, the changes should be transparent to the end user. Please report any issues you might run into when you use SChar and SString types.