Z3 4.8.14

[mario-bucev]

To get getAbsFuncDecl working, we savagely apply a patch on the Z3 sources to export mkAbs.
The other changes are mostly whitespace trimming (done by the editor...) and putting () to methods expecting them to address the warnings when cross-compiling to Scala 2.13

[samarion]

To get getAbsFuncDecl working, we savagely apply a patch on the Z3 sources to export mkAbs.

So much violence! :)

If the tests pass, this LGTM. It would probably be worth updating the unmanaged jars in Inox and Stainless as well.

[mario-bucev]

I had a quick glance at updating the unmanaged jars in Inox and some tests fail, but it should not be too hard to update them.

[samarion]

Hmm, failing tests don't sound too good. Is 4.8.12 a stable Z3 version? Which version are we shipping in the z3 binary?

[mario-bucev]

It seems so; what's weird is that all tests (in the master branch) that communicate with Z3 through SMT-LIB use the 4.8.12 version and all pass.

[samarion]

Which Inox tests are failing with this version? Maybe there's been a subtle API change in the native version which we have to take into account?

Maybe you can try a different Z3 version otherwise?

[mario-bucev]

The Z3 Set Extraction test (in SemanticsSuite, for nativez3 and unrollz3 only) as well as the Model Extraction test (in SolversSuite, only for nativez3).
I'll investigate the issue and try your suggestion as well.

[samarion]

Ah, then it's fairly likely that we're running into bugs in Inox if it's only about model extraction.

[mario-bucev]

Z3 is returning a lambda which Z3Native does not currently support. Maybe we can do something similar to what is done in Z3Target:
https://github.com/epfl-lara/inox/blob/efd76f30e486a89fc4fc33c073a69f3bf2bfd052/src/main/scala/inox/solvers/smtlib/Z3Target.scala#L187-L209
(or try with a different Z3 version)

[samarion]

Adapting Z3Native to handle lambdas like Z3Target sounds like a plan.

[mario-bucev]

Upgrading to 4.8.14 resolves the problem with the set extraction, as Z3 no longer returns lambdas (seems to be related to the fix of Z3Prover/z3#5604). There are some integration tests that fail though (I did not run 4.8.12 on the integration tests, but they are likely to fail as well).

[gsps]

For what it's worth, given the mkAbs helper you added below it should be possible to make this marginally less hacky by avoiding the parsing. I had to do something similar to get a handle to the built-in if-then-else function here: https://github.com/epfl-lara/inox/blob/2f402f9bf9541cc061558e525fdd53efa5f86a87/src/main/scala/inox/solvers/z3/Z3Native.scala#L478

[mario-bucev]

With some small changes, all Inox tests pass. Stainless does not need any adaptations (except for its dependencies of course), and one Bolts benchmark, gcd, needs one tiny change.

[samarion]

That sounds reasonable. Can you please open a PR with the Inox changes too?

[mario-bucev]

Sure! Here it is: epfl-lara/inox#175