Jonáš Fiala
Jonáš Fiala
The following snippet: ```rust use prusti_contracts::*; fn main() {} fn foo(x: &mut (usize, usize)) { let f = &mut x.0; *f = 1 + 1; // *f = (1, 1).0;...
Other examples from working on #901
When encoding the following fn: ```rust fn option_eq(l: &Option, r: &Option) -> bool { match (l, r) { (Some(l), Some(r)) => l == r, (None, None) => true, _ =>...
The following example: ```rust use prusti_contracts::*; fn main(){} fn id(x: &mut i32) -> &mut i32 { x } fn get_mut(root: &mut Option) -> &mut i32 { if let Some(left) =...
The following runs into a `Consistency error: Local variable _1 not found.` when verifying the `main` function: ```rust use prusti_contracts::*; #[pure] pub fn zero() -> usize { 0 } #[pure]...
Wan't sure how else to trigger a CI run
Not sure if this should actually be merged, but should hopefully make the interactive server work with traces from the latest suslik version.
The current algorithm will create confusing names in the case of a clash. For example given the two names `box_123` and `box_222` it will simplify these to `b` and `bo`...