[Date Prev][Date Next] [Thread Prev][Thread Next] [Date Index] [Thread Index]

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: