Matrix Addition example (encoded via domains) does not verify

[viper-admin]

Created by @alexanderjsummers on 2017-05-08 10:33 Last updated on 2018-06-09 12:16

See the attached file - the first loop invariant cannot be shown to be preserved

---

Attachments:

• matrix_addition.sil
• logfile-01-FAILS.smt2
• logfile-01-TIDY.smt2

[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) loop invariants (which causes Viper to pick rather more permissive options) doesn't seem to help, at least.

[viper-admin]

@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 as logfile-01-FAILS.smt2) generated by Silicon then the check-sat corresponding to the failing invariant check yields unknown with reason "incomplete quantifiers". However, if the SMT code is tidied up by removing all intermediate push-pop blocks (logfile-01-TIDY.smt2) then the check-sat passes (yields unsat).

[viper-admin]

@mschwerhoff on 2017-06-05 13:19:

• changed attachment from (none) to logfile-01-TIDY.smt2

[viper-admin]

@mschwerhoff on 2017-06-05 13:20:

• changed component from (none) to Z3

[viper-admin]

@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

[mschwerhoff]

Still doesn't verify, using the latest Silicon version, neither with Z3 4.8.7, nor 4.8.14.