Lithum- Z3 shell aborts with error message

ID0000030: This issue was created automatically from Mantis Issue 30. Further discussion may take place here.

---

Id	Project	Category	View	Due Date	Updated
ID0000030	Frama-C	Plug-in > jessie	public	2009-04-07	2014-02-12

Reporter	virgile	Assigned To	cmarche	Resolution	unable to reproduce
Priority	normal	Severity	minor	Reproducibility	always
Platform	-	OS	-	OS Version	-
Product Version	Frama-C Lithium-20081201	Target Version	-	Fixed in Version	Frama-C Beryllium-20090902

Description :

[bug #7241 from old bts, reported by Christoph Weber] Hello,

while I was trying to proof a function I got an error message.

Unfortunatly, I dont have time to figure out a smaller example

But the error occured when I altered the clause:

====== ensures ( (\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) && a[k1] < b[k1]) || (\forall integer k2; (0 <= k2 < length_a) ==> length_a < length_b && a[k2] == b[k2]) ) ==> \result == 1 ;

into: ensures ( (\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) && a[k1] < b[k1]) || (\forall integer k2; (0 <= k2 < length_a) ==> length_a < length_b && a[k2] == b[k2]) ) ^^ \result == 0 ;

========== Here the source-code:

/*@ requires 0 <= length_a; requires 0 <= length_b;

requires \valid_range (a, 0, length_a-1); requires \valid_range (b, 0, length_b-1);

assigns \nothing;

ensures \result == 1 || \result == 0;

ensures ( (\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) && a[k1] < b[k1]) || (\forall integer k2; (0 <= k2 < length_a) ==> length_a < length_b && a[k2] == b[k2]) ) ^^ \result ==0 ;

/ int lexicographical_compare_array (int a, int length_a, int* b, int length_b) { int i = 0; /*@ loop invariant 0 <= i <= length_a;
loop invariant 0 <= i <= length_b;

loop invariant \forall integer k; 0 <= k < i ==> a[k] == b[k];   
*/
for ( ; i != length_a && i != length_b; ++i)
{
    if (a[i] < b[i])
    {		
					/*@ 
						assert \exists integer k1; 0 <= k1 <= i && a[k1] < b[k1];

					*/			
        return 1;
    }
    if (b[i] < a[i])
    {
    
        return 0;  
    }     

}
//return i == length_a && i != length_b ? 1 : 0;

if (i == length_a && i != length_b)
{
		/*@
			assert 
			(

(\exists integer k1; (0 <= k1 < length_a && 0 <= k1 < length_b) && a[k1] < b[k1]) || (\forall integer k2; (0 <= k2 < length_a) ==> length_a < length_b && a[k2] == b[k2]) ); */ return 1; } else { return 0; } }

Sorry for the complex function,

Cheers Christoph