Feature request: Multiple engines
Closed this issue · 2 comments
It would be nice to be able to use ic3 and kind engines simultaneously.
Although interesting, there is currently no plans of parallelization. The internals of sally are not thread-safe, and this would put extra requirements on the SMT solvers that can be used. Doing it from the outside is probably good enough.
I don't think this can be done effectively from the outside. One of the major reasons for using ic3 and k-induction simultaneously is that they can share results. In particular, invariants found by ic3 can be used to strengthen the k-induction queries. Thus you can have cases where neither engine can solve a property on its own, but they can solve it together.
On a related note, does sally currently do any kind of invariant generation/discovery when using k-induction?