3f3c9caf4d
The poststate should be one where all predicates are assumed false, rather than the unchanged prestate. Closes #2374
17 lines
341 B
Rust
17 lines
341 B
Rust
// https://github.com/mozilla/rust/issues/2374
|
|
// error-pattern:unsatisfied precondition constraint (for example, even(y
|
|
|
|
|
|
fn print_even(y: int) : even(y) { log(debug, y); }
|
|
|
|
pure fn even(y: int) -> bool { true }
|
|
|
|
fn main() {
|
|
let mut y = 42;
|
|
check (even(y));
|
|
loop {
|
|
print_even(y);
|
|
loop { y += 1; break; }
|
|
}
|
|
}
|