diff --git a/crates/va-test/examples/misc-parsing/src/main.rs b/crates/va-test/examples/misc-parsing/src/main.rs
index 07bd5ef3f21f..39e948a69b6b 100644
--- a/crates/va-test/examples/misc-parsing/src/main.rs
+++ b/crates/va-test/examples/misc-parsing/src/main.rs
@@ -1,11 +1,11 @@
+use vstd::prelude::*;
+
 verus! {
 
-spec fn lemma_div_basics(a:bool, b:bool)
-{
-    a <== b
+spec fn wrapping_add_u8() -> u8 {
+    <u8>::MAX
 }
 
-
 } // verus!
 
 fn main() { }