Zack Grannan

Finished benchmarking commit (c449775827cf7227253197dd9c2563e04953a62e): [comparison url](http://3.94.193.1:2346/compare.html?start=81c84a036c9ae233806706da639be45165593539&end=c449775827cf7227253197dd9c2563e04953a62e&stat=wall-time). Benchmark returns the average of 3 consecutive runs of the benchmark suite, performed after an initial 'warm-up' run. An external Prusti server is maintained...

Instead, if the `check()` method is marked as `#[trusted]`, the following output is observed: ``` error: [Prusti internal error] generating fold-unfold Viper statements failed (FailedToObtain(Acc(Field(Field(Field(Field(Local(_1: Ref(ref$closure$0_11$3$16578871950627681774), Position { line: 11,...

So it seems like the macro expansion forces the precondition function to be placed inside the impl block as it's defined there. Then, this error is reported during macro expansion,...

Hmm, maybe this is unrelated, but a similar error also occurs without GADT: ```haskell data Op = Foo Op Op {-@ data Op = Foo Op Op @-} ``` yields:...

@ranjitjhala The above code is in fact a minimal example. Here's a link (not sure what version of LH is used here, but it happens locally on `develop` for me...

@kosmikus I can confirm that https://github.com/ucsd-progsys/liquidhaskell/pull/1704 fixes the second case :)

I encountered this error myself. Here is a problematic json value: ``` "hello \\n world" ``` This represents hello + a literal backslash + n world, NOT a newline. When...

I'm not quite sure when the invariants will be ready; although I have a WIP PR here: https://github.com/viperproject/prusti-dev/pull/686. There is still one failing test, and also I know that it...

> Does it work if you spell out the `old`, i.e. `#[ensures(old(&out).inner === old(&out).inner)]` (or any variant thereof)? That works! > The `===` is syntax sugar for `snapshot_equality(&out.inner, &out.inner)` here,...

The only use of `ReverseRoutingContext` (which is the type of `_rrc`) I could find is here: https://github.com/playframework/playframework/blob/7d40b7eb3a6564c185077752c191ddf605ae2988/framework/src/play/src/main/scala/play/api/controllers/Assets.scala#L606 and it looks to me like it's only current purpose is to handle...