[Termtools] certification errors and inconsistent results

[Thomas Ströder]

Dear Johannes and all,

First of all thanks for pointing out these conflicts!

Am 29.07.2015 um 03:46 schrieb Johannes Waldmann:
> Dear all,
> 
> I implemented some automated consistency checks, and found:
> 
> http://nfa.imn.htwk-leipzig.de/termcomp-devel/problems/9546/9548/9568/9569

This seems to be a bug in HipTNT+. The example is terminating.

> http://nfa.imn.htwk-leipzig.de/termcomp-devel/problems/9632/9652

The first one seems to be a bug in AProVE. The example is terminating.
We are working on it and will submit a fixed version today.

The second one seems to be a bug in UltimateBuchiAutomizer. The example
is non-terminating.

> http://nfa.imn.htwk-leipzig.de/termcomp-devel/problems/9663/9665/9682/9683

The first one seems to be a bug in HipTNT+. The example is terminating.

The second one seems to be a bug in AProVE. The example is
non-terminating according to the C99 standard. However, according to
C89, it would be implementation-defined behavior since non-termination
only occurs if we consider integer division of negative numbers (C is a
beast). What is the opinion of the other participants on integer
division of negative numbers? Shall we consider it to do truncation
towards zero as in the more current standard? Then I would add this to
the rules to make it clear.

Best regards,

  Thomas


> - Johannes.
> 
> 
> 
> Remarks: The first access to any such page will be sllooowwwww.
> 
> This will wrongly show inconsistencies between SRS and cycle-SRS
> (because they use identical benchmarks but with different semantics)
> 
> Benchmark equality is by starecex-id (for now)
> (meaning you cannot compare jobs from different years)
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
> 

-- 
Thomas Ströder        mailto:stroeder at informatik.rwth-aachen.de
LuFG Informatik 2     http://verify.rwth-aachen.de/stroeder
RWTH Aachen           phone: +49 241 80-21241

-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: OpenPGP digital signature
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150729/2a68f67e/attachment.sig>