search

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
356 stars 51 forks source link

Support for Z3 4.8.6 #502

Open jad-hamza opened 5 years ago

jad-hamza commented 5 years ago

See: https://github.com/epfl-lara/stainless/issues/497

jad-hamza commented 5 years ago

Support for Z3 4.8.4 in Inox should be ok now with https://github.com/epfl-lara/inox/pull/98, but in Stainless, the tests are failing for CovariantList.scala due to https://github.com/Z3Prover/z3/issues/2300.

jad-hamza commented 5 years ago

Z3Prover/z3#2300 was fixed, and I changed Set to InoxSet in epfl-lara/inox#98 to avoid clashes with the new Set from Z3's master, so now all tests from Inox and Stainless go through (with https://github.com/Z3Prover/z3/commit/8f368682852258295efc385cb16e427386aeacbd)

vkuncak commented 5 years ago

@jad-hamza, so, this just needs the documentation update? We go all the way to 3.8.5, right?

jad-hamza commented 5 years ago

Yes it all works with the Z3 binaries 4.8.5, I've updated the docs and scripts here: https://github.com/epfl-lara/stainless/pull/540. It remains to see what's going on for ScalaZ3, but that requires more debugging.