Malte Schwerhoff

A comment regarding your quantifier forall a2: array :: true ==> (forall i1: Int :: { array_loc(a2, i1) } true ==> ...) Given the nested quantifier `forall x :: forall...

In the Voila frontend, I've also regularly lost error messages due to missing positional information (`NoPosition`), and eventually decided to give each Viper AST node the positional information of the...

Comparing `offendingNode`s by identity is dangerous because the Viper AST is immutable, and front- and backend may perform transformations that result in (structurally) equivalent but non-identical nodes. How about taking...

You brought up an interesting point: so far, we are not aware of a bullet-proof system that allows to uniquely locate/identify a subtree when equality is structurally defined. Tallies and...

I've started implementing what we've discussed: https://github.com/viperproject/silicon/tree/silicon-issue-613. Please take a look and let me know if (1) the new definition of failure equivalence, see `class FailureEquivalenceWrapper`, suits you, and if...

@marcoeilers I'm tempted to close this as "won't fix" because it doesn't really seem to be a Silicon bug, and the solution/work-around you provided sounds not too hacky to me....

Silicon's Z3 configuration can be found here: https://github.com/viperproject/silicon/blob/master/src/main/resources/z3config.smt2. For option `qi.lazy_threshold`, Z3's default value is used. According to `z3 -pd`, the default is `20.0`. You could locally change the value...

Sorry for the late reply. Thanks for running the experiments! How do the runtimes compare?

I compared the benchmarks: [2020-05-27_issue-368.xlsx](https://github.com/viperproject/silicon/files/4687631/2020-05-27_issue-368.xlsx).   | Current | Eager | Lazy ----| ----- | ------------ | ------------- **Files** | 1096 | 1094 | 1095 **Minutes** | 16:04 | 39:34 |...

Updates: * As of 7175ff5, Silicon sources its set, multiset and sequence axioms from Viper files * As of 59f89af, Silicon provides command-line options for overriding the axiomatisations it uses....