fix

viperproject · Jul 27, 2022 · c74215b · c74215b
1 parent 1eaa7d0
commit c74215b
Showing 1 changed file with 2 additions and 3 deletions.
diff --git 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)))",
         );
     }