lsrcz · lsrcz · Jul 3, 2025 · Jul 3, 2025
diff --git a/.github/workflows/test.yml b/.github/workflows/test.yml
@@ -23,11 +23,11 @@ jobs:
           - {build: nix, arg: "", ismain: false, experimental: false, ghc: "948", cachekey: "nix-948"}
           - {build: nix, arg: "", ismain: false, experimental: false, ghc: "966", cachekey: "nix-966"}
           - {build: nix, arg: "", ismain: false, experimental: false, ghc: "984", cachekey: "nix-984"}
-          - {build: nix, arg: "", ismain: true, experimental: false, ghc: "9101", cachekey: "nix-9101"}
-          - {build: cabal, arg: "", ismain: false, experimental: false, ghc: "9121", cachekey: "cabal-9121"}
+          - {build: nix, arg: "", ismain: true, experimental: false, ghc: "9102", cachekey: "nix-9102"}
+          - {build: nix, arg: "", ismain: false, experimental: false, ghc: "9122", cachekey: "nix-9122"}
         include:
           - os: macOS-latest
-            plan: {build: nix, arg: "", ismain: true, experimental: false, ghc: "9101", cachekey: "nix-9101"}
+            plan: {build: nix, arg: "", ismain: true, experimental: false, ghc: "9102", cachekey: "nix-9102"}
     runs-on: ${{ matrix.os }}
     continue-on-error: ${{ matrix.plan.experimental }}
     steps:

diff --git a/CHANGELOG.md b/CHANGELOG.md
diff --git a/README.md b/README.md
@@ -48,7 +48,7 @@ can add it to your project's `.cabal` file:
 ```cabal
 library
   ...
-  build-depends: grisette >= 0.12 < 0.13
+  build-depends: grisette >= 0.13 < 0.14
 ```
 
 #### Using stack
@@ -59,14 +59,14 @@ Note: Grisette on Stackage is currently outdated. Please make sure to use
 
 ```yaml
 extra-deps:
-  - grisette-0.12.0.0
+  - grisette-0.13.0.0
 ```
 
 and in your `package.yaml` file:
 
 ```yaml
 dependencies:
-  - grisette >= 0.12 < 0.13
+  - grisette >= 0.13 < 0.14
 ```
 
 #### Quick start template with `stack new`

diff --git a/examples/grisette-examples.cabal b/examples/grisette-examples.cabal
@@ -1,11 +1,11 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.37.0.
+-- This file has been generated from package.yaml by hpack version 0.38.0.
 --
 -- see: https://github.com/sol/hpack
 
 name:               grisette-examples
-version:            0.12.0.0
+version:            0.13.0.0
 synopsis:           Examples for Grisette
 description:        More examples are available in the
                     [tutorials](https://github.com/lsrcz/grisette/tree/main/tutorials) of
@@ -32,5 +32,7 @@ executable basic
       basic
   build-depends:
       base >=4.14 && <5
-    , grisette ==0.12.*
+    , grisette ==0.13.*
+    , mtl
+    , text
   default-language: Haskell2010
diff --git a/examples/package.yaml b/examples/package.yaml
@@ -1,5 +1,5 @@
 name: grisette-examples
-version: 0.12.0.0
+version: 0.13.0.0
 synopsis: Examples for Grisette
 description: |
   More examples are available in the
@@ -14,7 +14,9 @@ extra-source-files:
   - README.md
 dependencies:
   - base >= 4.14 && < 5
-  - grisette >= 0.12 && < 0.13
+  - grisette >= 0.13 && < 0.14
+  - mtl
+  - text
 executables:
   basic:
     source-dirs: basic

diff --git a/flake.lock b/flake.lock
diff --git a/flake.nix b/flake.nix
@@ -66,22 +66,22 @@
         pname = "grisette";
         extraOutputs = pkgs: haskellPackages: devShellWithVersion: {
           devShells = {
-            "9101" = devShellWithVersion {
-              ghcVersion = "9101";
+            "9102" = devShellWithVersion {
+              ghcVersion = "9102";
               config = {
                 isDevelopmentEnvironment = true;
                 bitwuzla = true;
               };
             };
             default = devShellWithVersion {
-              ghcVersion = "9101";
+              ghcVersion = "9102";
               config = {
                 isDevelopmentEnvironment = true;
                 bitwuzla = true;
               };
             };
-            "9121" = devShellWithVersion {
-              ghcVersion = "9121";
+            "9122" = devShellWithVersion {
+              ghcVersion = "9122";
               config = {
                 isDevelopmentEnvironment = false;
                 bitwuzla = true;

diff --git a/grisette.cabal b/grisette.cabal
@@ -1,11 +1,11 @@
 cabal-version: 1.12
 
--- This file has been generated from package.yaml by hpack version 0.37.0.
+-- This file has been generated from package.yaml by hpack version 0.38.0.
 --
 -- see: https://github.com/sol/hpack
 
 name:               grisette
-version:            0.12.0.0
+version:            0.13.0.0
 synopsis:           Symbolic evaluation as a library
 description:        Grisette is a reusable symbolic evaluation library for Haskell. By
                     translating programs into constraints, Grisette can help the development of
@@ -39,8 +39,8 @@ tested-with:
   , GHC == 9.4.8
   , GHC == 9.6.6
   , GHC == 9.8.4
-  , GHC == 9.10.1
-  , GHC == 9.12.1
+  , GHC == 9.10.2
+  , GHC == 9.12.2
 extra-source-files:
     CHANGELOG.md
     README.md
@@ -310,7 +310,7 @@ library
       src
   ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -Wno-x-partial -Wno-unrecognised-warning-flags
   build-depends:
-      QuickCheck >=2.14 && <2.16
+      QuickCheck >=2.14 && <2.17
     , array >=0.5.4 && <0.6
     , async >=2.2.2 && <2.3
     , atomic-primops >=0.8.3 && <0.9
@@ -357,7 +357,7 @@ test-suite doctest
       doctest
   ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -Wno-x-partial -Wno-unrecognised-warning-flags -threaded -rtsopts -with-rtsopts=-N
   build-depends:
-      QuickCheck >=2.14 && <2.16
+      QuickCheck >=2.14 && <2.17
     , array >=0.5.4 && <0.6
     , async >=2.2.2 && <2.3
     , atomic-primops >=0.8.3 && <0.9
@@ -479,7 +479,7 @@ test-suite spec
   ghc-options: -Wextra -Wcompat -Widentities -Wincomplete-record-updates -Wmissing-export-lists -Wmissing-home-modules -Wmissing-import-lists -Wpartial-fields -Wunused-type-patterns -Wno-x-partial -Wno-unrecognised-warning-flags -threaded -rtsopts -with-rtsopts=-N -Wredundant-constraints
   build-depends:
       HUnit ==1.6.*
-    , QuickCheck >=2.14 && <2.16
+    , QuickCheck >=2.14 && <2.17
     , array >=0.5.4 && <0.6
     , async >=2.2.2 && <2.3
     , atomic-primops >=0.8.3 && <0.9

diff --git a/hie.yaml b/hie.yaml
@@ -10,7 +10,3 @@ cradle:
       component: "grisette-examples:exe:basic"
     - path: "examples/basic/Paths_grisette_examples.hs"
       component: "grisette-examples:exe:basic"
-    - path: "examples/exception/Main.hs"
-      component: "grisette-examples:exe:exception"
-    - path: "examples/exception/Paths_grisette_examples.hs"
-      component: "grisette-examples:exe:exception"
diff --git a/package.yaml b/package.yaml
@@ -1,5 +1,5 @@
 name: grisette
-version: 0.12.0.0
+version: 0.13.0.0
 synopsis: Symbolic evaluation as a library
 description: "Grisette is a reusable symbolic evaluation library for Haskell. By\ntranslating programs into constraints, Grisette can help the development of\nprogram reasoning tools, including verification, synthesis, and more.\n.\nThe \"Grisette\" module exports all the core APIs for building a symbolic\nevaluation tool. A high-level overview of the module structures are available\nthere.\n.\nA detailed introduction to Grisette is available at \"Grisette.Core\". More\nlifted libraries are provided in @Grisette.Lib.*@ modules.\n.\nThe \"Grisette.Unified\" module offers an experimental unified interface for\nsymbolic and concrete evaluation. This module should be imported qualified.\n.\nFor more details, please checkout the README and \n[tutorials](https://github.com/lsrcz/grisette/tree/main/tutorials).\n"
 category: Formal Methods, Theorem Provers, Symbolic Computation, SMT
@@ -19,8 +19,8 @@ tested-with:
   - GHC == 9.4.8
   - GHC == 9.6.6
   - GHC == 9.8.4
-  - GHC == 9.10.1
-  - GHC == 9.12.1
+  - GHC == 9.10.2
+  - GHC == 9.12.2
 dependencies:
   - base >= 4.14 && < 5
   - hashable >= 1.3 && < 1.6
@@ -39,7 +39,7 @@ dependencies:
   - sbv >= 8.17 && < 12
   - parallel >= 3.2.2 && < 3.3
   - text >= 1.2.4.1 && < 2.2
-  - QuickCheck >= 2.14 && < 2.16
+  - QuickCheck >= 2.14 && < 2.17
   - prettyprinter >= 1.5.0 && < 1.8
   - async >= 2.2.2 && < 2.3
   - stm >= 2.5 && < 2.6

diff --git a/src/Grisette/Internal/SymPrim/SomeBV.hs b/src/Grisette/Internal/SymPrim/SomeBV.hs
@@ -234,7 +234,7 @@ import Unsafe.Coerce (unsafeCoerce)
 -- | An exception that would be thrown when operations are performed on
 -- incompatible bit widths.
 data SomeBVException = BitwidthMismatch | UndeterminedBitwidth T.Text
-  deriving (Show, Eq, Ord, Generic)
+  deriving (Eq, Ord, Generic)
   deriving anyclass (Hashable, NFData)
   deriving
     ( Mergeable,
@@ -249,11 +249,14 @@ data SomeBVException = BitwidthMismatch | UndeterminedBitwidth T.Text
     )
     via (Default (SomeBVException))
 
-instance Exception SomeBVException where
-  displayException BitwidthMismatch = "Bit width does not match"
-  displayException (UndeterminedBitwidth msg) =
+instance Show SomeBVException where
+  show BitwidthMismatch = "Bit width does not match"
+  show (UndeterminedBitwidth msg) =
     "Cannot determine bit-width for literals: " <> T.unpack msg
 
+instance Exception SomeBVException where
+  displayException = show
+
 class MaySomeBV bv where
   assignLitBitWidth :: (KnownNat n, 1 <= n) => SomeBVLit -> bv n
 
@@ -359,7 +362,8 @@ instance
 -- >>> bv 4 0x3 + bv 4 0x3 :: SomeBV IntN
 -- 0x6
 -- >>> bv 4 0x3 + bv 8 0x3 :: SomeBV IntN
--- *** Exception: BitwidthMismatch
+-- *** Exception: Bit width does not match
+-- ...
 --
 -- One exception is that the equality testing (both concrete and symbolic via
 -- 'SymEq') does not require the bitwidths to be the same. Different bitwidths
@@ -382,7 +386,8 @@ instance
 -- >>> 3 * bv 4 0x1  :: SomeBV IntN
 -- 0x3
 -- >>> 3 * 3 :: SomeBV IntN
--- *** Exception: UndeterminedBitwidth "(*)"
+-- *** Exception: Cannot determine bit-width for literals: (*)
+-- ...
 --
 -- Some operations allows the literals to be used without the bit-width, such as
 -- '(+)', '(-)', 'negate', 'toUnsigned', 'toSigned', '.&.', '.|.', 'xor',

diff --git a/stack-9.10.yaml b/stack-9.10.yaml
@@ -16,7 +16,7 @@
 #
 # resolver: ./custom-snapshot.yaml
 # resolver: https://example.com/snapshots/2018-01-01.yaml
-resolver: nightly-2025-05-05
+resolver: nightly-2025-07-03
 # User packages to be built.
 # Various formats can be used as shown in the example below.
 #

diff --git a/stack-9.10.yaml.lock b/stack-9.10.yaml.lock
@@ -1,12 +1,12 @@
 # This file was autogenerated by Stack.
 # You should not edit this file by hand.
 # For more information, please see the documentation at:
-#   https://docs.haskellstack.org/en/stable/lock_files
+#   https://docs.haskellstack.org/en/stable/topics/lock_files
 
 packages: []
 snapshots:
 - completed:
-    sha256: 5c7ae8619fe0a6b36ab11931ec13248f9731722d32da7f1baae982277e086d05
-    size: 681591
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/4/12.yaml
-  original: nightly-2025-04-12
+    sha256: 1e879c64480ca43c6b796e6d48f64fa07072cbed80c1b802b48db3265510df50
+    size: 722394
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/7/3.yaml
+  original: nightly-2025-07-03
diff --git a/stack.yaml.lock b/stack.yaml.lock
@@ -6,7 +6,7 @@
 packages: []
 snapshots:
 - completed:
-    sha256: bcbc80a081dbf9d701bb8c46f0212b251acbe6cf64332e6e3c8b108c13794841
-    size: 685947
-    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/5/5.yaml
-  original: nightly-2025-05-05
+    sha256: 1e879c64480ca43c6b796e6d48f64fa07072cbed80c1b802b48db3265510df50
+    size: 722394
+    url: https://raw.githubusercontent.com/commercialhaskell/stackage-snapshots/master/nightly/2025/7/3.yaml
+  original: nightly-2025-07-03