diff --git a/prusti-specs/src/specifications/preparser.rs b/prusti-specs/src/specifications/preparser.rs index 7938914f99d..47950059d18 100644 --- a/prusti-specs/src/specifications/preparser.rs +++ b/prusti-specs/src/specifications/preparser.rs @@ -900,10 +900,9 @@ mod tests { parse_prusti("forall(|x: i32| a ==> b, triggers = [(c,), (d, e)])".parse().unwrap()).unwrap().to_string(), "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) })", ); - let expr: syn::Expr = syn::parse2("assert!(a === b ==> b)".parse().unwrap()).unwrap(); assert_eq!( - parse_prusti(quote! { #expr }).unwrap().to_string(), - "assert ! ((! (snapshot_equality (a , b)) || (b)))", + parse_prusti("assert!(a === b ==> b)".parse().unwrap()).unwrap().to_string(), + "assert ! ((! (snapshot_equality (& a , & b)) || (b)))", ); }