Strategy (process) for upgrading Z3 version

[rakamaric]

So I am getting back to Boogie after a longer hiatus, and I built the latest version of Boogie and installed the latest release of Z3. As if commonly happens, a few regressions are failing due to "nondeterminism" across Z3 releases, which manifests itself as slightly different error traces or models.
Since I haven't been around for a while, I am wondering if there is now a strategy/process in place for dealing with this kind of stuff, or even for just upgrading Z3 (when and how to do it, etc.)?
Thanks!

[shazqadeer]

Welcome back, @rakamaric. Boogie missed you!

For dealing with different error traces and models, we don't have a strategy except that we try to minimize such test cases. There are very few test cases that have a model in their golden output. There are lots of tests that have error traces in them but only a few of them tend to be flaky. Both kinds of differences seem to be minimized if we fix the Z3 version and the hardware/OS, which bodes well for github CI. When I test locally on my Mac, a few tests (always the same set) fails. I ignore those failures locally expecting that my PR will still land fine on github. If you have suggestions for improvement, I am all ears.

Boogie likes to stay abreast of the latest version of SMT solvers (Z3 and CVC5 are the most important by far). If the version used in github CI has fallen behind, we should try to move to the latest and update the CI config. What do you think?

[rakamaric]

Thanks @shazqadeer!
Ah, I see, so it might be the consequence of me running on a Mac and not Z3 version. Good to know.
A couple of things.
I also think we should be updating solvers pretty regularly, and so I agree with you on that one. Z3 moved quite a bit in terms of releases when compared to what the CI is currently running. So let me try to update that.
I am also wondering if it is usually the same tests that fail, maybe we could do some lit tricks (maybe it supports regular expressions) to make sure they pass across platforms. I'll look into this briefly as well.

[gauravpartha]

As a side remark: There are front-end verifiers using Boogie that use old versions of Z3, because for newer versions of Z3 various front-end tests do not work or do not terminate. The underlying issue may be in the front-end verifiers or in the newer Z3 versions. No one seems to have a good way to debug such issues and as a result, the Z3 versions for front-end verifiers do not progress.

For example, Dafny still uses Z3 4.8.5 and Viper still uses Z3 4.8.7. So, it would be good if Boogie still worked for older Z3 versions. But I agree that testing Boogie in the CI with up-to-date versions of Z3 makes sense.

[rakamaric]

I agree. Having said that, it is really tricky to maintain backwards compatibility in terms of performance/scalability. So while Boogie might still "work" for older Z3 versions in the sense that there are no crashes and all regressions are passing, it still might break benchmarks on your end (performance, incompleteness, etc.). I don't know how to guard against that, and I am totally open to ideas and suggestions.