Skip to content

Commit bdee3b7

Browse files
committed
fix test
1 parent bef9688 commit bdee3b7

1 file changed

Lines changed: 2 additions & 4 deletions

File tree

source/rust_verify_test/tests/atomics.rs

Lines changed: 2 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -358,8 +358,7 @@ test_verify_one_file! {
358358
});
359359
}
360360
pub fn call_do_nothing<A, B: InvariantPredicate<A, u8>>(i: Tracked<&AtomicInvariant<A, u8, B>>) {
361-
let Tracked(credit) = create_open_invariant_credit();
362-
proof { do_nothing(credit, i.get()); }
361+
proof { do_nothing(create_open_invariant_credit(), i.get()); }
363362
}
364363
} => Ok(())
365364
}
@@ -376,8 +375,7 @@ test_verify_one_file! {
376375
});
377376
}
378377
pub fn call_do_nothing<A, B: InvariantPredicate<A, u8>>(i: Tracked<&LocalInvariant<A, u8, B>>) {
379-
let Tracked(credit) = create_open_invariant_credit();
380-
proof { do_nothing(credit, i.get()); }
378+
proof { do_nothing(create_open_invariant_credit(), i.get()); }
381379
}
382380
} => Ok(())
383381
}

0 commit comments

Comments
 (0)