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

[Andreas Gebhardt]

Dear Ton-Chanh Le,

> We have a problem with the x = x++ statements,
> which appear in the examples
>
> TPDB/C/SV-COMP_Termination_Category/ChenFlurMukhopadhyay-SAS2012-Ex3.08_true-termination.c
>
>
> TPDB/C/SV-COMP_Termination_Category/ChenFlurMukhopadhyay-SAS2012-Ex4.01_true-termination.c
 >
> [...]
 >
> Could we use x++ instead of x = x++ in those examples?

these two statements (together with a ';') are not interchangeable by 
default, the first statement

	x++;

increments the value of `x` and returns the value of `x` before it was 
incremented. The value which the statement returns is not used.
   But the second one uses the return value of `x++`

	x = x++;

which is the value of `x` before it was incremented. So the value of `x` 
right before and right after the statement `x = x++;` does not change.

Without using the postincrement operator (`x_` a fresh variable of same 
type as `x`)

    x_ = x;
    x = x+1;
    x = x_;


Best Regards,
Andreas