SMT-based program verifier
