-
Notifications
You must be signed in to change notification settings - Fork 256
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Compilation of :| assume
omitted
#5166
Comments
After waffling a bit :) I feel this deserves the Note the followed program creates a method Main() {
var y :| assume {:axiom} y == 4 && P(y);
print y, "\n";
}
opaque predicate P(x: int) { true }
|
More specifically (since the lack of
Edit: In both cases compilation should fail as it does now if the heuristics can't figure out how to compile the search at all. |
Dafny version
4.4.0
Code to produce this issue
Command to run and resulting output
What happened?
The
:| assume
construct should be different from:|
only in that it omits the proof obligation that a value exists. So, if the compiler does compile the program, then, in the event that the value actually does exist, the code should find it.In other words,
should behave like
However, it seems the compiler emits no code for the
:| assume
statement, which is wrong.Additional test case
Currently, this gives:
but it should have printed
2 3 4
.What type of operating system are you experiencing the problem on?
Mac
The text was updated successfully, but these errors were encountered: