viper-admin

> **@alexanderjsummers** commented on 2017-05-08 10:45 I had thought initially that this might be a triggering problem. This could be the case, but removing the triggers on (all of the)...

> **@mschwerhoff** commented on 2017-06-05 13:19 The problem appears to be quantifier-related, potentially caused by a Z3 incompleteness: when Z3 (nightly 4.5.1-a8ff97c0f446) is run on the full SMT code (attached...

> **@mschwerhoff** on 2017-06-05 13:19: > * changed `attachment` from `(none)` to `logfile-01-TIDY.smt2`

> **@mschwerhoff** on 2017-06-05 13:20: > * changed `component` from `(none)` to `Z3`

> **@mschwerhoff** commented on 2018-06-09 12:16 Still doesn't verify, using the latest Silicon version, and Z3 4.6.0 and 4.8.1-nightly

> **@Felalolf** commented on 2019-07-23 17:02 I tried to simplify the test a bit. ```plaintext predicate P(x: Int) { producer(x) && consumer(x) // THIS LINE FAILS } domain Dummy {...

> **@vakaras** commented on 2018-07-25 09:15 Carbon [issue](https://github.com/viperproject/carbon/issues/249).

> **@mschwerhoff** commented on 2018-08-07 14:04 @vakaras @alexanderjsummers Did you look at Z3's axiom instantiation statistics to confirm your matching loop theory ? It could also be that Z3's macro...

> **@vakaras** commented on 2018-08-15 10:22 After adding the following method: ``` #!silver method test2a(this: Ref, n: Int) requires P(this) { unfold P(this) fold P(this) assert fib2(this, n) > 0...

> **@mschwerhoff** commented on 2018-08-15 10:59 Thanks for looking into this; a long chain is indeed a strong indicator for a matching loop. Did you by any chance check the...