[Termtools] certification errors and inconsistent results

[Matthias Heizmann]

Hi Johannes,

> 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?
Yes. I am in favor for this.

> Then I would add this to the rules to make it clear.
Maybe a good idea.

Best,
Matthias


On Wednesday 29 July 2015 11:41:14 Thomas Ströder wrote:
> 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
-------------- next part --------------
A non-text attachment was scrubbed...
Name: signature.asc
Type: application/pgp-signature
Size: 819 bytes
Desc: This is a digitally signed message part.
URL: <http://lists.lri.fr/pipermail/termtools/attachments/20150729/74157780/attachment.sig>