Federico Poli
Federico Poli
When running the axiom profiler with Mono, loading any log file of nontrivial size (more than a few megabytes) seems to cause a crash. Using Mono is currently the only...
@marcoeilers Does Silicon encode `assert ; ...` to some SMT2 where `` is repeated twice, with a pop in between? ``` (push) (assert !) (check-sat) (pop) (assert ) ... ```...
@utaal mentioned me that the Z3 API has a way to *clone* a solver. The method seems to be [Solver::translate](https://z3prover.github.io/api/html/classcom_1_1microsoft_1_1z3_1_1_solver.html#a2f4086956a17bb24964a5b0d53ff65f6). For the Silicon parallelization it might be more efficient to...
For some reason, the following program verifies even if the `apply_on` tigger is not used in `test`. Removing the precondition of `apply_on` makes the program fail as expected. Both versions...
From a sampled profiling of Silicon, the following line is reported to be in the stacktrace of 5.5% of the samples: https://github.com/viperproject/silicon/blob/c8d4c9677d956604ec0d580e6d44f92c3c00b7ef/src/main/scala/decider/Decider.scala#L228 It's a linear search over a list of...
The following verifies in Carbon but generates an error in Silicon: ``` field f: Ref function rd(): Perm ensures result > 0/1 ensures result < 1/1 predicate G(self: Ref) predicate...
I would expect both methods below to be rejected, but apparently a `true --* ...` magic wand is enough to escape the injectivity checks. ``` predicate P(x: Ref) method m1()...
Calling `Silicon::verify` multiple times (sequentially) on the same verifier instance leaks memory, which is freed only when the verifier is destructed. In other words, there is some state that is...
Is there a way to report which triggers has been inferred by Silicon? Dafny shows them with a tooltip in the IDE, or in the standard output if a special...
On macOS arm64: * [ ] The prerequisite checks don't terminate. * [ ] Prusti Assistant downloads and tries to use the Prusti artifacts that were compiled for x86. *...