search

boogie-org / boogie

Boogie
http://research.microsoft.com/en-us/projects/boogie/
MIT License
509 stars 112 forks source link

Incompatible with Z3 which has changed the parameter name from "model_compress" to "model.compact" #169

Closed junkil-park closed 4 years ago

junkil-park commented 4 years ago

In "boogie/Source/Provers/SMTLib/Z3.cs", Boogie sets the Z3 parameter "model_compress" to be false. This cause a problem with the latest Z3 (4.8.7+) which has changed the parameter name from "model_compress" to "model.compact".

shazqadeer commented 4 years ago

@bkragl : I recall discussing a similar issue with you. Thoughts?

bkragl commented 4 years ago

Yes, Nikolaj pointed out this change when I reported a segfault in Z3: https://github.com/Z3Prover/z3/issues/2707

I think that the code that sets the Z3 parameters should be revised in general.

zvonimir commented 4 years ago

Yes! Cleaning up the code that sets up solver parameters has been on my mind for a long time now. Should we create a separate issue for that and discuss it there?

shazqadeer commented 4 years ago

@zvonimir : Please create a separate issue. I am closing this one.