search

dafny-lang / libraries

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

Adapt some proofs for lower variability and better compatibility with Z3 4.12.1 #76

Closed atomb closed 1 year ago

atomb commented 1 year ago

This makes several proofs more explicit to reduce their variability and make them succeed with Z3 4.12.1.

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

atomb commented 1 year ago

I haven't checked myself that the proof go better with more versions of z3 but the changes seem reasonable so I approve them. When can we expect to have some tests to ensure the library is tested with different versions of z3? I guess you still have some work to do, right?

There might be a tiny bit of work left to get things working smoothly with multiple Z3 versions, but not much. Soon I'd like to update the CI to automatically verify with several versions (at least 4.8.5 and 4.12.1).

There's already a Dafny PR that runs the whole Dafny test suite (including the libraries) with Z3 4.12.1, and merging these library changes should allow that PR to pass.