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.
