Open gregnazario opened 1 year ago
Thanks for reporting. There seems to be some new non-determinism upstream causing this, because we have already multiple measures in place to ensure output is deterministic.
You can work around this for now by adding pragma verify = false;
to the spec loop_with_two_back_edges_incorrect
block. Please also point via a TODO at the pragma to this issue.
Yeah, the test case can have two ways to fail for the inductive case. One is by assigning x
, and another is assigning y
. Perhaps, we need to update the test case so that its counterexample can be deterministic.
public fun loop_with_two_back_edges_incorrect(x: u64, y: u64) {
spec {
assume x != y;
};
loop {
spec {
invariant x != y;
};
if (x > y) {
y = y + 1;
continue
};
if (y > x) {
x = x + 1;
continue
};
break
};
}
@gregnazario can work around the issue by the way @wrwg describes.
🐛 Bug
When running baseline tests locally, the loop tests provide a different output than the build servers. This causes there to be a lot of wasted time trying to figure out why these tests fail due to code changes, when in fact it has nothing to do with them.
To reproduce
Code snippet to reproduce
Stack trace/error message
https://github.com/move-language/move/runs/8222133907?check_suite_focus=true#step:6:3678
Expected Behavior
The prover needs to be predictable or:
System information
Please complete the following information:
Additional context
Add any other context about the problem here.