Malte Schwerhoff

Exception: Cycle in causality graph

1

A recent nightly of the axiom profiler crashes with `Found cycle in causality graph!`. The exception occurs regardless of whether or not `Only show instantiations from single check` is ticked...

**Note:** Reducing attached SMT file to its minimum revealed issue #26. Running SMT file [set_equals_triggers_datatypes.smt2.txt](https://github.com/viperproject/axiom-profiler/files/4682586/set_equals_triggers_datatypes.smt2.txt) on Z3 4.8.6 on Windows 10 produced [z3.log](https://github.com/viperproject/axiom-profiler/files/4682598/z3.log). Loading this into the axiom profiler shows...

Incorrect translation (function, quantifiers, heap-dep. triggers) causes Z3 errors

1

The program further down (distilled from [ring-insert.vpr](https://github.com/viperproject/silver/blob/master/src/test/resources/graphs/static/examples/ring-insert.vpr)) results in Z3 warnings and errors, caused by the SMT translation of the quantifiers in lines 13 and 14: the translated triggers contain...

``` field f: Int predicate p(x: Ref) { acc(x.f) && x.f >= 3 } method foo(x: Ref, y: Ref) requires p(x) && p(y) requires unfolding p(y) in y.f == 7...

The failures in the following program are unexpectedly reported by Silicon, but not by Carbon. ```plain function id(i: Int): Int { i } method test01(i: Int) requires forall y: Int...

Incompleteness with wands and abstract functions

2

I think the following program should verify. Find out, why it doesn't. ``` field val: Int function req_wand(a: Ref): Int requires acc(a.val) --* acc(a.val) method test_wand_framing_2(a: Ref) { inhale acc(a.val)...

As of 591b332, `assert true` no longer triggers a state consolidation. Instead, the special method call `___silicon_hack510_consolidate_state()` can be used to trigger a state consolidation. Note: to satisfy the type...

Silicon issue corresponding to [Silver issue #455](https://github.com/viperproject/silver/issues/455).

Silicon fails to assert false after a vacuous wand has been applied. The program originates from the discussion around #485. ``` field val: Bool method first(x: Ref) requires acc(x.val) ensures...

The example below illustrates a difference in behaviour between invoking a function — which entails asserting its precondition — and explicitly asserting the function's precondition: in the former case, the...