Groups > linux.debian.bugs.dist > #1026201

Bug#970510: why3: does not work with current version of cvc4

From	Ralf Treinen <treinen@free.fr>
Newsgroups	linux.debian.bugs.dist, linux.debian.maint.ocaml.maint
Subject	Bug#970510: why3: does not work with current version of cvc4
Date	2020-09-23 22:10 +0200
Message-ID	<ASjfr-2fT-1@gated-at.bofh.it> (permalink)
References	(1 earlier) <ASjfr-2fT-3@gated-at.bofh.it> <ASjfr-2fT-3@gated-at.bofh.it> <ASjfs-2fT-5@gated-at.bofh.it> <ASjfr-2fT-3@gated-at.bofh.it> <ASjfs-2fT-5@gated-at.bofh.it>
Organization	linux.* mail to news gateway

Cross-posted to 2 groups.

Show all headers | View raw

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.

Back to linux.debian.bugs.dist | Previous | Next | Find similar | Unroll thread

Thread

Bug#970510: why3: does not work with current version of cvc4 Ralf Treinen <treinen@free.fr> - 2020-09-23 22:10 +0200

csiph-web