Open muchang opened 1 year ago
Thanks for the report. I've been able to reproduce your results where the program verifies under Dafny 3.13.1.50302 but not under Dafny 4.0.0.50303. We'll investigate further.
Ah, note that in Dafny 4.0.0, the default version of Z3 changed from 4.8.5 to 4.12.1. It's unfortunate, though expected, that this may cause proof regressions - though it can also cause previously failing proofs to succeed.
Noting that your code snippet involves arithmetic, this issue may be related: https://github.com/dafny-lang/dafny/issues/3501
Thanks for the investigation! It helps a lot. I am actually still wondering why the change of Z3's version will cause Dafny's failing proof.
I can imagine that it may happen if two versions produce different results (which means there was/is a soundness bug in Z3) or the current version of Z3 produces an unknown or timeout. But it would be surprising that Z3 has a soundness bug or timeout on this simple program. Do you have any idea about it? Is the failing proof due to the incorrect or unknown result of Z3 or there are some other reasons?
Due to the heavy use of quantifiers by Dafny, Z3 is almost always working in the space of undecidable theories, and therefore it is usually able to prove only "valid" or "unknown". The error that shows up with Dafny 4 is because Z3 is returning "unknown" when it previously returned "valid". It looks like the solution suggested in #3501, setting /proverOpt:O:smt.arith.solver=6
, allows Z3 to easily prove the assertion. We've considered making that the default, but doing so unfortunately also causes many other proofs not to go through.
I see, it makes sense. I will consider using /proverOpt:O:smt.arith.solver=6
to have a better performance of Dafny, when it cannot give a proof in default. Thanks!
Dafny version
4.0.0.50303
Code to produce this issue
Command to run and resulting output
What happened?
Dafny4 reports the assertion might not hold while Dafny can successfully verify this.
If I substitute
tmp_1 := true
withassert false;
or any variable with its assignment (like substitutingtmp_2
with2830 * x
), Dafny4 can also verify this.Are there any reasons about why such a substitution affects the verification result and why this regression happens in Dafny4?
What type of operating system are you experiencing the problem on?
Linux