Multi-property solving about sally HOT 2 OPEN

This can be done with not too much work, depending on the engine used.

There is a question of how to interact with the user in this case, with the user potentially being another program, e.g. how to report that a specific property is valid or a counter-example is found.

Do you have any problems you can share for the multi-property checking?

from sally.

Here's an example of a multi-property file where lemmas are needed to prove a property:

https://gist.github.com/agacek/ad0b3513b0e78b47995b

Here lemmaA is hard to prove on its own, but easy if you conjoin it with lemmaB (or lemmaC even). Moreover, the ok1 property is much easier if conjoined with lemmaA, lemmaB, and lemmaC.

Playing with this file also exposed another strange result in sally. Consider these two queries for the transition system given in the file.

(query T (and (or |lemmaA| |%init|)
          (or |lemmaB| |%init|)))
(query T (or |lemmaA| |%init|))

Using k-induction, the first query is proved instantly. Sally then gets stuck on the second property. But the second property is an immediate consequence of the first. Sally should be using previously proven results as invariants for proving future properties.

I have no strong feelings about the UI / API.

from sally.