[Termtools] TPDB: C/AProVE_numeric/ex2.c

[Akihisa Yamada]

Dear Thomas and Le Ton Chanh,

the proposed patch is applied, please check the attached.

Best regards,
Akihisa

On 2015/07/15 11:28, Thomas Ströder wrote:
> Dear Le Ton Chanh,
>
> Yes, that makes sense. Akihisa, could you apply that patch, please?
>
> Best regards,
>
>    Thomas
>
>
> Am 15.07.2015 um 11:24 schrieb Ton-Chanh Le:
>> Dear all,
>>
>> In the test C/AProVE_numeric/ex2.c, should we
>> change the code
>>
>> int rec1(int i) {
>>          if(i <= 0)
>>                  return 0;
>>          rec2(rec1(i+1));
>> }
>>
>> into
>>
>> int rec1(int i) {
>>          if(i <= 0)
>>                  return 0;
>>          return rec2(rec1(i+1));
>> }
>>
>> like rec2?
>>
>> Best Regards,
>>
>> Le Ton Chanh
>> Email: chanhle at comp.nus.edu.sg <http://comp.nus.edu.sg>
>>
>>
>> _______________________________________________
>> Termtools mailing list
>> Termtools at lists.lri.fr
>> http://lists.lri.fr/cgi-bin/mailman/listinfo/termtools
>>
>
>
>
> _______________________________________________
> 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 --------------
extern int __VERIFIER_nondet_int();
int rec1(int i);
int rec2(int j);

int rec1(int i) {
	if(i <= 0)
		return 0;
	return rec2(rec1(i+1));
}

int rec2(int j) {
	if(j <= 0)
		return 0;
	return rec1(rec2(j-1));
}

int main() {
	int x = __VERIFIER_nondet_int();
	rec2(x);
}