Bug#970510: why3: does not work with current version of cvc4
Hello,
On Wed, Sep 23, 2020 at 02:04:24PM +0200, Fabian Wolff wrote:
> And while we're at it, even though this is technically an unrelated
> problem, it also has something to do with SMT solver versions: In the
> autopkgtests control file [0], you have the following code:
>
> Tests: why3+z3
> Depends:why3, z3 (<< 4.8.7)
> Restrictions: skip-not-installable
>
> This is not a big issue, because it doesn't block migration of z3
> (unlike the cvc4 failure [1]), you might still want to adjust this
> version restriction, given that the current z3 version in unstable is
> 4.8.9 (unless, of course, there is a reason why why3 won't work with
> more recent versions of z3).
this version constraint is coming from share/provers-detection-data.conf,
so why3 will refuse to work with newer versions of z3, and I am on
myself not able to attest that it is safe to override this check.
-Ralf.
Reply to: