Skip to content

Commit bb8746a

Browse files
committed
mark new dev version
1 parent cafc851 commit bb8746a

2 files changed

Lines changed: 15 additions & 1 deletion

File tree

CHANGES.md

Lines changed: 14 additions & 0 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,20 @@
11
* Hackage: <http://hackage.haskell.org/package/sbv>
22
* GitHub: <http://github.com/LeventErkok/sbv>
33

4+
### Version 14.5, Not yet released
5+
6+
* Add `sRealToSIntegerRM` and `sRationalToSIntegerRM`, which convert a real/rational to an
7+
integer using a symbolic rounding-mode argument, along with the helper `sCaseRoundingMode`
8+
for dispatching on a symbolic `SRoundingMode`. Thanks to Ryan Scott for the implementation.
9+
10+
* Fix `svQuot`/integer division in `Data.SBV.Dynamic`, which was using flooring (`div`)
11+
instead of truncating (`quot`) division on concrete integers. Thanks to Ryan Scott for the report.
12+
13+
* Improve the Haddocks for `sQuot`, `sDiv`, `sRem`, `sMod`, and related functions, clarifying
14+
the truncating- vs. flooring-division distinction and documenting that the `Data.SBV.Dynamic`
15+
operations `svQuot`, `svRem`, and `svQuotRem` behave differently from their `s`-prefixed
16+
counterparts on unbounded integers. Thanks to Ryan Scott for the implementation.
17+
418
### Version 14.4, 2026-07-03
519

620
* Add `curry` and `uncurry` (for symbolic 2-tuples) and `curry3` and `uncurry3` (for

sbv.cabal

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -1,7 +1,7 @@
11
Cabal-Version: 2.2
22

33
Name : sbv
4-
Version : 14.4
4+
Version : 14.5
55
Category : Formal Methods, Theorem Provers, Bit vectors, Symbolic Computation, Math, SMT
66
Synopsis : SMT Based Verification: Symbolic Haskell theorem prover using SMT solving.
77
Description : Express properties about Haskell programs and automatically prove them using SMT

0 commit comments

Comments
 (0)