PV4 ⊧ COLIBRI (COnstraint LIBrary for veRIfication)produces a satisfiability result for a formula
Colibri is a family of three tools in Frama-C: COLIBRI (the ancestor in development since 2000), Colibri2 (its reimplementation in OCaml) and Colibrics (formally proved)