HiFrog as interpolating incremental C verifier offers support for the following features:

-- Various interpolants for QF_BOOL, QF_LRA, QF_LIA, QF_UF

-- User-Provided Summaries

-- Automatic recursion unwinding

 -- Assertion optimization using assertion dependency analysis

-- Tuning the Strength of Summaries

--Tuning the Size of Summaries

-- Counterexamples

The architecture is depicted in the following diagram: