[SMT-COMP] Issues with tracer for application track

[Andres Nötzli]

Hi all,

We’ve been running some tests on the incremental benchmarks using StarExec with the tracer, scrambler, and post-processor from 2016 and it looks like the tracer is unable to parse some of the expected statuses in benchmarks. For example on QF_ABVFP/20170501-Heizmann-UltimateAutomizer/filter2_alt_true-unreach-call.c.smt2:

BAD expected result: unknown)(declare-fun ~unnamed0~FALSE () (_ BitVec 32)

All errors seem to involve an unknown status that is immediately followed by an opening parenthesis. The issue seems to occur in the Heizmann-UltimateAutomizer benchmark families in the logics QF_BVFP, QF_ABVFP, ABVFP, BVFP. I can compile a complete list of affected benchmarks if that’s helpful.

-Andres