Skip to content

Commit 6e53b86

Browse files
committed
fix
1 parent 1eaa7d0 commit 6e53b86

File tree

1 file changed

+2
-3
lines changed

1 file changed

+2
-3
lines changed

prusti-specs/src/specifications/preparser.rs

+2-3
Original file line numberDiff line numberDiff line change
@@ -900,10 +900,9 @@ mod tests {
900900
parse_prusti("forall(|x: i32| a ==> b, triggers = [(c,), (d, e)])".parse().unwrap()).unwrap().to_string(),
901901
"forall (((# [prusti :: spec_only] | x : i32 | (c) ,) , (# [prusti :: spec_only] | x : i32 | (d) , # [prusti :: spec_only] | x : i32 | (e) ,) ,) , # [prusti :: spec_only] | x : i32 | -> bool { (((! (a) || (b))) : bool) })",
902902
);
903-
let expr: syn::Expr = syn::parse2("assert!(a === b ==> b)".parse().unwrap()).unwrap();
904903
assert_eq!(
905-
parse_prusti(quote! { #expr }).unwrap().to_string(),
906-
"assert ! ((! (snapshot_equality (a , b)) || (b)))",
904+
parse_prusti("assert!(a === b ==> b)".parse().unwrap()).unwrap().to_string(),
905+
"assert ! ((! (snapshot_equality ( & a , & b)) || (b)))",
907906
);
908907
}
909908

0 commit comments

Comments
 (0)