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

[Akihisa Yamada]

Dear Mathias and all,

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

thank you for clarification. Following this, I am going to apply the
attached patch.

Best regards,
Akihisa

On 2015/07/21 16:07, Matthias Heizmann wrote:
> 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"
>>
>>
>> _______________________________________________
>> Termtools mailing list
>> Termtools at lists.lri.fr
>> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools

-- 
Akihisa Yamada, Ph.D.
Computational Logic Group, Institute of Computer Science,
University of Innsbruck
http://cl-informatik.uibk.ac.at/~ayamada/
-------------- next part --------------
diff -r d113995c7fe3 C/SV-COMP_Termination_Category/ChenFlurMukhopadhyay-SAS2012-Ex3.08_true-termination.c
--- a/C/SV-COMP_Termination_Category/ChenFlurMukhopadhyay-SAS2012-Ex3.08_true-termination.c	Wed Jul 15 11:53:51 2015 +0200
+++ b/C/SV-COMP_Termination_Category/ChenFlurMukhopadhyay-SAS2012-Ex3.08_true-termination.c	Tue Jul 21 16:50:16 2015 +0200
@@ -24,7 +24,7 @@
     while (x - y > 0) {
         x = -x + y;
         y = z;
-        z = z++;
+        z = z + 1;
     }
     return 0;
 }
diff -r d113995c7fe3 C/SV-COMP_Termination_Category/ChenFlurMukhopadhyay-SAS2012-Ex4.01_true-termination.c
--- a/C/SV-COMP_Termination_Category/ChenFlurMukhopadhyay-SAS2012-Ex4.01_true-termination.c	Wed Jul 15 11:53:51 2015 +0200
+++ b/C/SV-COMP_Termination_Category/ChenFlurMukhopadhyay-SAS2012-Ex4.01_true-termination.c	Tue Jul 21 16:50:16 2015 +0200
@@ -25,7 +25,7 @@
     while (x + y >= 0 && x <= n) {
         x = 2*x + y;
         y = z;
-        z = z++;
+        z = z + 1;
     }
     return 0;
 }