@function isqrt: int -> int

@axiom I1: isqrt(1) = 1
@axiom I2: all n,k:int. n > 1 && k >= 1 && 
				k*k = n ==> isqrt(n) = k
@axiom I3: all n,k:int. n > 1 && k >= 1 && 
				k*k < n && (k+1)*(k+1) > n ==> isqrt(n) = k

// @axiom I4: all n:int. isqrt(n) >= 1

@requires n >= 2
@ensures prime <=> all(k, 2 : isqrt(n), n%k != 0)

@program 

// must not declare k
@var  i, n : int
@var  prime : bool

i = 2;
prime = true;

@invariant 2 =< i=< isqrt(n)+1 &&  (prime <=> all(k, 2:i-1, n%k != 0))

while (i =< isqrt(n)) {
      if (n % i == 0) {
	     prime = false; 
             break;
          }
      i = i+1;
}
@end
--