search

boogie-org / corral

solver for the reachability modulo theories problem
MIT License
58 stars 29 forks source link

Z3 fixedpoint module and its usage in Boogie/Corral #88

Closed zvonimir closed 4 years ago

zvonimir commented 5 years ago

We run into an issue related to Boogie/Corral trying to use Z3's fixedpoint module: https://github.com/smackers/smack/issues/425

First of all, it seems that newer versions of Z3 replaced fixedpoint module with fp module. So maybe Boogie/Corral should be updated accordingly.

Second, it is unclear to us when (and why) do Boogie/Corral use this module. We failed to reproduce the problem and we also could not find where in the Boogie/Corral source code that module gets enabled. It would be great if you could shed some light on this.

akashlal commented 5 years ago

The fixedpoint module was used for the Duality algorithm (an alternative to Corral's Stratified Inlining algorithm). It gets activated with the /useDuality flag, which then triggers this code in BoogieVerify:

CommandLineOptions.Clo.FixedPointMode = CommandLineOptions.FixedPointInferenceMode.Corral;CommandLineOptions.Clo.FixedPointEngine = "duality"; vcgen = new Microsoft.Boogie.FixedpointVC(program, CommandLineOptions.Clo.SimplifyLogFilePath, CommandLineOptions.Clo.SimplifyLogFileAppend, new List(), options.extraRecBound);

You are getting an error even without using this flag?

Akash

On Tue, Mar 26, 2019 at 9:32 PM Zvonimir notifications@github.com wrote:

We run into an issue related to Boogie/Corral trying to use Z3's fixedpoint module: smackers/smack#425 https://github.com/smackers/smack/issues/425

First of all, it seems that newer versions of Z3 replaced fixedpoint module with fp module. So maybe Boogie/Corral should be updated accordingly.

Second, it is unclear to us when (and why) do Boogie/Corral use this module. We failed to reproduce the problem and we also could not find where in the Boogie/Corral source code that module gets enabled. It would be great if you could shed some light on this.

— You are receiving this because you are subscribed to this thread. Reply to this email directly, view it on GitHub https://github.com/boogie-org/corral/issues/88, or mute the thread https://github.com/notifications/unsubscribe-auth/ABzIY-p-BHngn_aUwdUicZo8i7ekATv-ks5vakSwgaJpZM4cL1cw .

zvonimir commented 5 years ago

Thanks Akash. We are still trying to root cause it. I'll let you know once we get to the bottom of this.

shuvendu-lahiri commented 5 years ago

@akashlal how difficult is it to revive this mode to target the new fixed point engine in Z3 with spacer (not sure if it is the same as the z3 fp)?

akashlal commented 5 years ago

@shuvendu-lahiri Duality triggers a different algorithm (not stratified inlining any more) that is implemented in Microsoft.Boogie.FixedpointVC. I am unsure of the status of that implementation.

zvonimir commented 4 years ago

This does not seem to be an issue any more. Closing it.