inconsistency in the boogie program

[rahxephon89]

Hi, I am seeing a strange inconsistency behavior in the boogie program attached to this question. I am wondering whether it is an issue from the program or the boogie tool. Can anyone give me some hints on how to debug this? Thanks!

boogie-error.txt

[shazqadeer]

You are using an old version of Boogie with syntax for datatypes that is no longer supported. The latest Boogie supports first-class syntax for datatypes.

I ported your example manually. I noticed that it has axioms. The last two axioms have quantifiers in them. If I comment any one of those two axioms, I get an error. Does that help?

[rahxephon89]

Thanks Shaz! We plan to use a new version of Boogie after solving the regression issue on timeout. About the axioms, they are both automatically generated and I could not see inconsistency issues in them. Is there a way to check correctness of them?

[shazqadeer]

I don't have a systematic way that I can teach you via text. I would try to remove bits and pieces of the program while retaining the inconsistency to get an even smaller example.

Once you have ported the example to the latest Boogie, I can take another look.

[rahxephon89]

Hi Shaz, I am observing a regression on verification time using boogie 2.16.9.0 and z3 4.12.2 while trying to get a minimal example of boogie program: the original program takes only 2s to get the result but removing one assert clause will cause the verification timeout (greater than 40s). Here is the command option used: boogie -doModSetAnalysis -printVerifiedProceduresCount:0 -printModel:1 -enhancedErrorMessages:1 -proverOpt:O:model_validate=true -proverOpt:PROVER_PATH=..bin/z3 -proverOpt:O:smt.QI.EAGER_THRESHOLD=100 -proverOpt:O:smt.QI.LAZY_THRESHOLD=100 -proverLog:@PROC@.smt boogie.bpl Do you have any suggestion to investigate more on this? Thanks

[rahxephon89]

Hi Shaz, the example with new syntax is attached.
boogie-error-new-syntax.txt

[shazqadeer]

Can you state more precisely what you mean by "inconsistency goes away"? If by going away you mean that some version of Z3 is unable to prove that assertion, it does not conclusively mean that there is no inconsistency in your axioms. It could just be the incompleteness in Z3 that is not allowing it to prove the assertion. Unless there is a bug in Z3, even if one version of Z3 is able to prove the assertion and you find this result counter-intuitive, it means that there is very likely some inconsistency in your axioms. In general, it would be helpful for you to have a clear model of Boogie/Z3 behavior in the presence of quantifiers. It is all rather nuanced for the users. I wish it weren't so but in general when you have quantifiers in the formula, you have to be very careful in your interpretation of the behavior you see. We can talk more about all this when we meet 1-1.

…

On Wed, Aug 16, 2023 at 2:12 AM Teng Zhang ***@***.***> wrote: @shazqadeer <https://github.com/shazqadeer> It seems that inconsistency issue goes away when using z3 4.12.2 instead of 4.11.2 — Reply to this email directly, view it on GitHub <#766 (comment)>, or unsubscribe <https://github.com/notifications/unsubscribe-auth/AB2RCFR5KDQ34JMO23BUES3XVSFJBANCNFSM6AAAAAA24HHCLU> . You are receiving this because you were mentioned.Message ID: ***@***.***>

[rahxephon89]

Hi Shaz, it turns out that the inconsistency goes away (the prover will not prove assert false) because /prune command removes an axiom, not because of update of z3.

[shazqadeer]

It seems incorrect to say that the inconsistency has gone away. There does appear to be an inconsistency among the axioms being generated by your prover.

[rahxephon89]

yeah, the issue comes from an axiom that says a generic serialize function is injective

[shazqadeer]

Ok. I will close this one then. Please reopen if anything is unresolved.