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

[Matthias Heizmann]

Why am I convinced that it is a typo?

The comment of the authors
(https://tigerbytes2.lsu.edu/users/hchen11/lsl/LSL_benchmark.txt)
says terminating for Example 3.8 and Example 4.1

The comment of the authors in only correct, if we replace 
"z = z++" by "z = z + 1"

Best,
Matthias



On Tuesday 21 July 2015 16:01:56 Matthias Heizmann wrote:
> 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/e52494a6/attachment.sig>