[Termtools] more strange outputs

[Thiemann, Rene]

Dear all,

concerning the first two of the rejected-NO’s, it is in fact not a reject, but an unsupported:
The generated proofs are not even CPFs according to the schema, since the entry for
<constantToUnary> is missing a child-element. (seems to be an easy-to-fix output bug in the CPF 
generator of AProVE)

The third rejected NO is a valid CPF, but partial CPF: it contains an <unknownProof> named aprove.DPFramework.TRSProblem.Processors.RelTRSEmissionProcessor.RelTRSEmissionProof. 
(seems to be a miss-configured strategy for certification)

The rejected complexity proof is a known incompatibility between TcT and CeTA where some
optimization in TcT has not yet been formalized and is thus rejected and already yesterday
I had a discussion with Michael Schaper on that point.

So far the analysis from the technical side.

As CeTA developer I’m perfectly fine to accept the above problem, but I’m not in the position 
to speak for the tool authors.

Cheers,
René


> Am 29.07.2015 um 10:48 schrieb Johannes Waldmann <johannes.waldmann at htwk-leipzig.de>:
> 
> Fresh from the kitchen of termcomp @ starexec:
> Today's choice of YES/NO conflicts for C programs,
> and some rejects from the certifier:
> 
> http://nfa.imn.htwk-leipzig.de/termcomp-devel/problems/9663/9665/9682/9683
> 
> Happy bugfixing to you all! Looking at the time that I waste^H^H^H^H^H
> invest on star-exec-presenter, I think this is only fair...
> 
> 
> Seriously, it would be good if you could indicate whether you
> "accept" the bug - or reject because of suspected error in
> TPDB benchmark, semantics specification, postprocessor, ..
> 
> You can write here, and/or add a note at
> http://www.termination-portal.org/wiki/Termination_Competition_2015_Bugs
> 
> 
> - J.
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools