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). Thanks! Fabian [0] https://sources.debian.org/src/why3/1.3.2-1/debian/tests/control/#L13 [1] https://lists.debian.org/debian-ci/2020/09/msg00042.html