Federico Poli

It's because `-x` is not a *checked* unary operation, but an *assert* MIR terminator. Only binary operations can be *checked*.

The Viper dump of the failing `List::push` verifies in Silicon. So, this is either an incompleteness of Viper or an issue in the way Prusti sends the program to be...

The error actually comes from the verification of the `main` function. However, a successful verification of `List::push` should ensure that the postcondition can be used at the call site without...

The program lacks a postcondition. Since `List::push` takes `&mut self`, it should ensure that the length of the list doesn't decrease. The `lookup` call in the postcondition of `List::push` requires...

Thanks for the report. Pure functions in Prusti cannot have loops, but in most cases you can replace the loop with recursive calls. Prusti should report an error (of the...

Viper is not fully thread safe because of rare issues such as https://github.com/viperproject/silicon/issues/578, but starting multiple `prusti-server`, each with its own JVM and Viper instance, would surely work. So, I...

Formatted (We should fix Silver to do this automatically): ``` function m_len__$TY$__Snap$struct$m_A$$int$(_1: Snap$struct$m_A): Int requires true requires true ensures result

There might be an easy solution to this: 1. `prusti-contracts` and `prusti-rustc` should both store their `prusti-dev` version (i.e. the hash of the commit of `prusti-dev` that is used for...

The cause might be that `old[l3](_8.val_ref)` is not recognized to be a suffix of `old[l3](_8.val_ref.val_ref)`.

Similar program: ```rust use prusti_contracts::*; struct Node { elem: i32, next: Option, } pub struct Stack { head: Option, } impl Stack { #[pure] #[trusted] fn len(&self) -> i32 {...