Patrick-6

Here is a summary of the current state of floating point support by Prusti: ```rust use prusti_contracts::*; fn test_0() { prusti_assert!(f64::NAN == f64::NAN); // Passes, but shouldn't prusti_assert!(f64::NAN === f64::NAN);...

The following function seems to be related to this issue: ```rust use prusti_contracts::*; // #[requires(src.len() != 0)] // adding this makes it verify #[requires(src.len() == dst.len())] // This postcondition should...

This example shows another issue when parsing `&&`, `predicate` accepts syntax that is not allowed in normal Rust code: ```rust use prusti_contracts::*; predicate!{ fn test_pred(x: &Option) -> bool { match...

There should also be an error when attempting to use `old` inside a predicate: ```rust use prusti_contracts::*; predicate! { fn is_plus_one(value: &u64) -> bool { snap(value) == old(snap(value)) + 1...