[Termtools] C category: x = x++ statements

[Matthias Heizmann]

On Tuesday 21 July 2015 15:48:43 Juergen Giesl wrote:
> I also think that the best solution would be to change this typo in the
> examples.

It is definitely a typo. 

History of these examples:

1. Used in the following publication
2012SAS  - Hong Yi Chen, Shaked Flur, and Supratik Mukhopadhyay Termination 
Proofs for Linear Simple Loops.

2. Available at the following URL in pseudocode (already with typo)
https://tigerbytes2.lsu.edu/users/hchen11/lsl/LSL_benchmark.txt

3. A former student of mine transformed it into a C program.
(Unfortunately, I probably asked him to copy exactly these examples)

4. We submitted the example to SV-COMP

Matthias


PS: I will also submit a patch the SV-COMP that replaces the
"z = z++;" by "z = z + 1"



-------------- 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/20150721/95b2ce95/attachment-0001.sig>