[SMT-COMP] Issues with tracer for application track

[Tjark Weber]

Andres,

On Mon, 2018-05-28 at 18:56 -0700, Andres Nötzli wrote:
> 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.

Thank you for reporting this. The reason for this issue is that the
trace executor doesn't actually do proper SMT-LIB parsing, but expects
the :status information on a line by itself.

Fortunately, this shouldn't affect the competition: as far as I can
see, all benchmarks where this occurs happen to be ineligible for the
application track (because the :status of their first check-sat command
is unknown).

I will prepare competition benchmark spaces on StarExec within the next
few days.

Best,
Tjark


När du har kontakt med oss på Uppsala universitet med e-post så innebär det att vi behandlar dina personuppgifter. För att läsa mer om hur vi gör det kan du klicka här https://mp.uu.se/web/info/stod/dataskyddsforordningen.

E-mailing Uppsala University means that we will process your personal data. For more information on how this is performed, please click here https://mp.uu.se/web/info/stod/dataskyddsforordningen.