Now that we have moved the default GHC version to 9.8 (#2055), using SBV versions greater than 11.0 (or perhaps, greater than 11.5; 11.1 through 11.5 don't build with GHC 9.8) causes test failures as described below. This is because the Z3 version we're using is older than the minimum supported by SBV. SBV upstream is also not particularly interested in providing compatibility for old versions, and to be fair the version we're using is very old, not just a little old.
In order to lift this restriction and use current SBV, we need to update the Z3 we're using for the regression tests. That in turn requires updating the default Z3 in what4-solvers, and that in turn requires updates to SAW to allow it to run alternate Z3 versions and/or provide config to the solver under user control. Currently a couple of things in SAW's test suite do not work with recent Z3. (See GaloisInc/saw-script#2404.) Those updates are in the works, but expected to take a while, so I'm leaving this issue open to track the situation on the Cryptol side.
Note also that:
- SBV does publish a minimum Z3 version upstream, but apparently doesn't check it at runtime; it's possible that we should.
- All of this happened because the CI only tests the builds done with the default GHC version; thus, any problem that arises with libraries or version skew with some other GHC version will not be detected.
Either of those points should maybe get their own issue someday.
Original description follows:
Moving the default GHC version to 9.8 (which was going to be part of #1966) causes the tests to be run on the GHC 9.8 build, and this fails with z3-related SBV exceptions, for example:
SBV exception:
*** Data.SBV: Unexpected non-success response from Z3:
***
*** Sent : (define-fun s1 () Int (ubv_to_int s0))
*** Expected : success
*** Received : (error "line 8 column 36: unknown constant ubv_to_int ((_ BitVec 2)) ")
***
*** Exit code : ExitFailure (-15)
*** Executable: /home/runner/work/cryptol/cryptol/bin/z3
*** Options : -nw -in -smt2
***
*** Reason : Check solver response for further information. If your code is correct,
*** please report this as an issue either with SBV or the solver itself!
This seems to be related to Z3Prover/z3#7572, which in turn arises because we're using an ancient z3 in what4-solvers, and that is in turn because of GaloisInc/saw-script#2404 (see also GaloisInc/saw-script#2448, basically a couple things in the SAW test suite run forever on newer z3, and fixing SAW to be able to be more selective about solver versions is a longstanding issue GaloisInc/saw-script#390)... anyway it isn't going to be fixed right away.
It also seems to be happening because we're using a newer SBV version with ghc 9.8+ (because it doesn't support 9.6 or earlier), so probably we should temporarily back off from that.
It would probably be good to adjust the CI so it tests at least one build from each GHC version... or at least the newest as well as the default, or something like that. Right now it only tests with the default GHC version.
@danmatichuk fyi
Now that we have moved the default GHC version to 9.8 (#2055), using SBV versions greater than 11.0 (or perhaps, greater than 11.5; 11.1 through 11.5 don't build with GHC 9.8) causes test failures as described below. This is because the Z3 version we're using is older than the minimum supported by SBV. SBV upstream is also not particularly interested in providing compatibility for old versions, and to be fair the version we're using is very old, not just a little old.
In order to lift this restriction and use current SBV, we need to update the Z3 we're using for the regression tests. That in turn requires updating the default Z3 in what4-solvers, and that in turn requires updates to SAW to allow it to run alternate Z3 versions and/or provide config to the solver under user control. Currently a couple of things in SAW's test suite do not work with recent Z3. (See GaloisInc/saw-script#2404.) Those updates are in the works, but expected to take a while, so I'm leaving this issue open to track the situation on the Cryptol side.
Note also that:
Either of those points should maybe get their own issue someday.
Original description follows:
Moving the default GHC version to 9.8 (which was going to be part of #1966) causes the tests to be run on the GHC 9.8 build, and this fails with z3-related SBV exceptions, for example:
This seems to be related to Z3Prover/z3#7572, which in turn arises because we're using an ancient z3 in what4-solvers, and that is in turn because of GaloisInc/saw-script#2404 (see also GaloisInc/saw-script#2448, basically a couple things in the SAW test suite run forever on newer z3, and fixing SAW to be able to be more selective about solver versions is a longstanding issue GaloisInc/saw-script#390)... anyway it isn't going to be fixed right away.
It also seems to be happening because we're using a newer SBV version with ghc 9.8+ (because it doesn't support 9.6 or earlier), so probably we should temporarily back off from that.
It would probably be good to adjust the CI so it tests at least one build from each GHC version... or at least the newest as well as the default, or something like that. Right now it only tests with the default GHC version.
@danmatichuk fyi