search

dafny-lang / libraries

Libraries useful for Dafny programs
Other
43 stars 25 forks source link

Make proofs easier for multiple Z3 versions #56

Closed atomb closed 1 year ago

atomb commented 2 years ago

Tested with these versions:

Two proofs fail with 4.8.7, and the whole process takes about twice as long with 4.11.0, but all other versions take around the same amount of time.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

atomb commented 2 years ago

It's great that you can make the library work on more versions of Z3. The code looks reasonable to me, even if I'm not a fan of putting {:vcs_split_on_every_assert} in a library, I think it might be the best decision for now.

Yeah, I wasn't thrilled by doing that, either. I hope that, at some point, we can work out a way to structure the proofs so that it's not necessary.

atomb commented 1 year ago

I would love to see in the CI a test that uses all versions of Z3.

Yeah, I'd like to see that at some point soon, too. The only thing stopping us from verifying the whole library with multiple versions is the compute time, and we could run them in parallel.