OpenSMT and Applications

We describe (and show with demos) the use of OpenSMT applied to the Lazy-abstraction (with interpolants) framework, interpolants computation, interpolants strenght, and unsatisfiability-proof reduction.

...