Cuv\'ee: Blending SMT-LIB with Programs and Weakest Preconditions

Cuv'ee is a program verification tool that reads SMT-LIB-like input files where terms may additionally contain weakest precondition operators over abstract programs. Cuv'ee translates such inputs into first-order SMT-LIB by symbolically executing these programs. The input format used by Cuv'ee is intended to achieve a similar unification of tools for that for example synthesize loop summaries. A notable technical aspect of Cuv'ee itself is the consequent use of loop pre-/postconditions instead of invariants, and we demonstrate how this lowers the annotation burden on some simple while programs.