[Termtools] Duplicates in full C category

[Thiemann, Rene]

Thanks Thomas for the observation. The duplicates have been removed, cf.

http://cl2-informatik.uibk.ac.at/mercurial.cgi/TPDB/rev/6198f4ee8da9

Cheers,
René

> Am 07.07.2015 um 12:31 schrieb Thomas Ströder <stroeder at informatik.rwth-aachen.de>:
> 
> Dear all,
> 
> By converting some numeric C programs into the new C integer program
> format, I detected the following duplicates in the current TPDB:
> 
> C/SV-Comp/AliasDarteFeautrierGonnord-SAS2010-aaron2_true-termination.c
> ->
> C/SV-Comp/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron2_true-termination.c
> 
> and
> 
> C/SV-Comp/AliasDarteFeautrierGonnord-SAS2010-aaron3_true-termination.c
> ->
> C/SV-Comp/ChawdharyCookGulwaniSagivYang-ESOP2008-aaron3_true-termination.c
> 
> and
> 
> C/SV-Comp/PodelskiRybalchenko-LICS2004-Fig2_true-termination.c
> ->
> C/SV-Comp/PodelskiRybalchenko-TACAS2011-Fig3_true-termination.c
> 
> I propose to merge the comments in these examples (as each pair of them
> refers to two different papers where the same examples have been used)
> and to keep only one program for each pair with the names
> "aaron2_true_termination.c", "aaron3_true_termination.c", and
> "PodelskiRybalchenko-LICS2004-Fig2-TACAS2011-Fig3_true-termination.c"
> respectively.
> 
> 
> C/SV-Comp/AliasDarteFeautrierGonnord-SAS2010-easy1_true-termination.c
> ->
> C/SV-Comp/ChawdharyCookGulwaniSagivYang-ESOP2008-easy1_true-termination.c
> 
> and
> 
> C/SV-Comp/AliasDarteFeautrierGonnord-SAS2010-easy2_true-termination.c
> ->
> C/SV-Comp/ChawdharyCookGulwaniSagivYang-ESOP2008-easy2_true-termination.c
> 
> These are no literal duplicates, but the only difference is that the
> variable z is declared on the same line as x and y in the
> AliasDarteFeautrierGonnord version and on a separate line in the
> ChawdharyCookGulwaniSagivYang version. So the difference is only
> syntactic and very tiny. Thus I propose the same procedure for these
> examples as for the ones above where the names of the kept programs
> should be "easy1_true-termination.c" and "easy2_true-termination.c",
> respectively.
> 
> Best regards,
> 
>  Thomas
> 
> 
> -- 
> 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
> 
> _______________________________________________
> Termtools mailing list
> Termtools at lists.lri.fr
> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools