Malte Schwerhoff

```plain import function foo1(n: Int): Int decreases n { 0 < n ? foo1(n) : 123 } // n does not decrease (but is bounded) function foo2(n: Int): Int decreases...

Viper ensures that Z3 may unroll a recursive function as deep as the predicates it depends on where manually (un)folded. Canonical example is a linked list and its recursively defined...

fenced_code markup not working inside a customblock

2

I've just started experimenting with custom blocks in the context of the website generator [Pelican](https://blog.getpelican.com/), and was wondering what the preferred/recommended way of nesting fenced code blocks under custom blocks...

Trigger warning might cause slow and failing verification

1

For file [wSolRec_rec.vpr.txt](https://github.com/user-attachments/files/15989395/wSolRec_rec.vpr.txt), Silicon generates a "trigger might not be usable" warning for the following loop invariant: forall xs: Seq[Int] :: {price(n, xs, prices)} valid_cut(xs, n) && 0 < xs[0]...

While playing with a forall-introduction lemma, I noticed that Silicon and Carbon handle `perm()` nested inside inhale-exhale expressions differently: ```text field f: Int function foo(x: Ref, p: Perm): Bool requires...

Carbon fails to verify the postcondition of function `coin_rec()`, while it verifies in Silicon. ``` function min(a: Int, b: Int) : Int decreases a, b { a < b ?...