OpenSMT and Applications: Lazy Abstraction, Interpolants, Proof Reduction

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

...