Skip to content

Commit

Permalink
Fixme issue for model-checking#556
Browse files Browse the repository at this point in the history
  • Loading branch information
celinval committed Mar 16, 2022
1 parent b763ebc commit 9e94685
Showing 1 changed file with 11 additions and 0 deletions.
11 changes: 11 additions & 0 deletions tests/kani/Iterator/into_iter_fixme.rs
Original file line number Diff line number Diff line change
@@ -0,0 +1,11 @@
// compile-flags: --edition 2018
// cbmc-flags: --unwind 4 --object-bits 9
//
// This reproduces the issue seen in "Failures when iterating over results".
// See https://github.com/model-checking/kani/issues/556 for more information.
#[kani::proof]
pub fn main() {
let numbers = vec![1, 10, -1];
let positives: Vec<_> = numbers.into_iter().filter(|&n| n > 0).collect();
assert_eq!(positives.len(), 2);
}

0 comments on commit 9e94685

Please sign in to comment.