Federico Poli

> Using `-Pserver_address=MOCK` worked! I'm glad that the 3-years old feature that nobody used so far is actually useful :rofl: It spawns a new server in a *thread*.

I totally agree that we should have some tests before merging.

This happened to me today. It's not a full explanation, but I noticed that here we register the span of the function instead of the span of the postcondition: https://github.com/viperproject/prusti-dev/blob/3dd957cf440edf04504f6b0ca8b57fac64e813a7/prusti-viper/src/encoder/procedure_encoder.rs#L4858-L4866...

Thank you for the report! One identifier generated by Prusti incorrectly contains a `::`. The detailed error from the log: ``` consistency error in scm_bisect::Search::::new: Consistency error: struct$m_std$$iter$$Map$m_std$$iter$$IntoIterator$$IntoIter$__TYPARAM__$_impl_IntoIterator_lt_Item__eq__G::Node_gt_$1$__$closure$m_Search$$$openang$G$closeang$$$new$$$opencur$closure$sharp$0$closecur$ is not...

The (quick) specification on Asana: https://app.asana.com/0/11661778102949/12871817123950

The '786__w' tag is required for example by https://github.com/inspirehep/invenio/pull/28, but to put https://github.com/inspirehep/invenio/pull/28 on prod I think that we need to add or edit also other tags/fields/indexes. I have to...

Thanks! So far I thought that Viper functions are heap-dependent only when they require predicates or permissions in their precondition. > That's due to how Silicon handles triggers. In your...

> Huh, I didn't know that. Is this documented somewhere or did you read the code? Neither. I just noticed from some stack traces of Z3 that the solver performs...

Here is an hand-crafted example where QI seems to be the true bottleneck. In this case, the modified encoding takes 44% less time. Version 1: 45s ``` (set-option :print-success true)...

This seems the same issue of #480 (and various others). As for why the incompletenesses are so basic, @alexanderjsummers, [this Z3 issue](https://github.com/Z3Prover/z3/issues/3240) might shed some light. It's enough for the...