Z3 version control by attribute

[seebees]

Currently Dafny pins z3 to v4.8.5.
However this is not the current version of z3.

The verification performance/stability for different versions of z3 and different code bases is large enough that there does not seem to be a single simple z3 version.

I suggest adding some kind of compile attribute to let people use older versions of z3.
This would let the Dafny project stay more current on versions of z3,
but still give customers a way to unblock themselves if verification times begin to time out.

I suggest taking 2 arguments, a version and a path.
Like this:

{ :vcs_z3_runtime v4.8.5, path/to/binary }

Obviously this would complicate the Dafny CI pipeline because it would need to test agains multiple versions of z3.
But this would unblock both Dafny and many Dafny projects to track more recent versions of z3.
The longer we wait to upgrade the more pain and work it will be.
And I don't see a path to a zero touch upgrade were ever proof obligation is just faster.

[cpitclaudel]

I think you have two proposals here:

1. Allow users to pick specific versions of Z3
2. Move Dafny to a more recent Z3

We already have support for 1, albeit with a command line flag: Dafny /proverOpt:PROVER_PATH=/path/to/custom/z3 input.dfy will run a different version of Z3. There are two warts:

• This flag is available with the legacy Dafny server, but not (AFAICT) with the new (LSP) server.
• The newest Z3s use a different name for one of Dafny's options, so we need to fix that (most likely by using version specific code to pick the right option name.

I don't think we should hardcode paths to binaries inside Dafny files (or even Dafny project files). Additionally, isn't there a redundancy between a version and a path?

Once we have a Dafny project file, I would find it nice if we could specify a range of Z3 versions there. This would be consistent with project-file entries replacing command line options.

As for 2, yes, it would probably be a good idea — but not before we understand what got slower, maybe?

[atomb]

One thing I think may be worth teasing out of the original issue description is that sometimes one version of Z3 will be most effective for verifying most parts of a Dafny program but another one might be required for one specific lemma, for instance. In that case, it's worth having some sort of local selection (similarly to how we have /vcsSplitOnEveryAssert and {:vcs_split_on_every_assert}, where the latter is more targeted). I had hoped to avoid the need for something like that, but I'm increasingly thinking it might be necessary.

I'm also wary of hard-coding paths into Dafny source files, but some form of solver selection might wind up being important (even if only for a few edge cases, and recommended against when possible). One possibility, which I'm not thrilled with, would be to have two officially-supported solver versions, both of which we distribute, and a way of selecting between them. I think the goal in that case would be to eventually drop the older one, but I don't know how long it'd take to get there.

[seebees]

I don't like hard coding paths either. What I really want is:

one version of Z3 will be most effective for verifying most parts of a Dafny program but another one might be required for one specific lemma, for instance.

As such, a global command line argument does not work.
How about something like this:
Additional arguments to add in specific versions of z3?
CLI:
dafny /vcsAlternateZ3:V438=/path/to/custom/z3

lemma {:vcs_alternate_z3 V438 } NeedsCustomVersion {}

As to this:

As for 2, yes, it would probably be a good idea — but not before we understand what got slower, maybe?

I'm suggesting that you are not going to make a Z3 upgrade bad for no one.
This means that there are always going to be edge cases.
If there is no way to incrementally update Z3,
either for Dafny or for Dafny customers,
then we are stuck waiting.