Something went wrong. Try again.
forked from verus-lang/verus
Something went wrong. Try again.
1234567891011121314151617181920212223242526272829303132use vstd::pervasive::runtime_assert;use vstd::prelude::*;use vstd::std_specs::iter::IteratorSpec;use std::str::*;
verus! {#[verifier::loop_isolation(false)]fn test() { let s = "abca"; proof { reveal_strlit("abca"); } let mut chars_it = s.chars(); for c in it: chars_it { let is_expected_char = c == 'a' || c == 'b' || c == 'c'; runtime_assert(is_expected_char); } let mut it2 = s.chars(); let mut x = it2.next(); runtime_assert(x == Some('a')); x = it2.next(); runtime_assert(x == Some('b')); x = it2.next(); runtime_assert(x == Some('c')); x = it2.next(); runtime_assert(x == Some('a')); x = it2.next(); runtime_assert(x == None);}}