Path programs where neither
    SMTInterpol with tree interpolation,
    Z3 with ForwardPredicates, nor
    Z3 with BackwardPredicates,
was able to generate a perfect sequence of interpolants.

All SV-COMP 2016 benchmarks from the following sets
    ReachSafety-BitVectors
    ReachSafety-ControlFlow
    ReachSafety-Loops
    ReachSafety-ProductLines
    ReachSafety-Sequentialized
    
Timeout 30s
Procedure Inlining
SequenceOfStatements