Replies: 3 comments 2 replies
-
This seems related to #488. the multiplication
Counterexample |
Beta Was this translation helpful? Give feedback.
-
Since Dafny is a proof engine and not a model checker, the counter examples are rather a model we extract from Z3 after Z3 told us "I couldn't disprove that this counterexample is not valid", so unfortunately they cannot be relied upon and are not a proof of failure like in model checkers. They can give hints at the best. We recentely re-labelled them as "experimental" to lower expectations, until we have a better name or interface. Note that you'd first need to prove that n*(n+1) is even so that the division is an integer one. Try adding this and prove it:
|
Beta Was this translation helpful? Give feedback.
-
OK, thank you. That helped! |
Beta Was this translation helpful? Give feedback.
-
Hi everyone,
I tried a proof and Dafny is not able to prove it. I stripped it down to the following:
The first assert is (of course) accepted, but the second fails (after quite a while).
If I ask for a counter example (press F7 in visual studio code), then it comes up with n: int = 520 a: int = 135460.
Why does this verification fail, and how is this a counterexample?
Beta Was this translation helpful? Give feedback.
All reactions