A confusing result of DySy for greatest common divisor algorithm

Feb 1, 2012 at 2:39 AM

Below is the code of computing greatest common divisor. 

        int gcd_new(int m, int n)        {          

           int r;
            while (n != 0)            {                 r = n;                n = m % n;                m = r;            }             

          return m;        }
While i test it with DySy using 

             gcd_new(25,205);            

gcd_new(20, 5);            

gcd_new(26, 95);

the output (below) is quite confusing:

[-] inferred spec of ICSE08.gcd_new(Int32, Int32)

=== Purity
pure; // on all observed paths
=== Precondition
bool s0 = m == int.MinValue && n == -1;
int s2 = m % n % n % m % n;
bool s1 = s2 == 0;
bool s3 = m % n == int.MinValue && n % m % n == -1;
bool s4 = n == int.MinValue && m % n == -1;
bool s5 = n % m % n != 0;
int s6 = n % m % n % s2;
return !s3 && s1 && !s4 && !s0 && s5 && m % n != 0 && n != 0 || !s0 && m % n == 0 && n != 0 || 
                                                                (s6 != int.MinValue || s2 % s6 != -1) && s6 % s2 % s6 == 0 && (s2 != int.MinValue || s6 != -1) && 
                                                                (n % m % n != int.MinValue || s2 != -1) && !s3 && !s4 && 
                                                                !s0 && s2 % s6 != 0 && s6 != 0 && !s1 && s5 && m % n != 0 && n != 0;

=== Result 
if ((m % n != int.MinValue || n % m % n != -1) && 
    m % n % n % m % n == 0 && (n != int.MinValue || m % n != -1) && 
    (m != int.MinValue || n != -1) && n % m % n != 0 && m % n != 0 && n != 0)
  return n % m % n;
if ((m != int.MinValue || n != -1) && m % n == 0 && n != 0)
  return n;
int s1 = m % n % n % m % n;
int s0 = n % m % n % s1;
if (
  (s0 != int.MinValue || s1 % s0 != -1) && s0 % s1 % s0 == 0 && (s1 != int.MinValue || s0 != -1) && 
  (n % m % n != int.MinValue || s1 != -1) && 
  (m % n != int.MinValue || n % m % n != -1) && (n != int.MinValue || m % n != -1) && 
  (m != int.MinValue || n != -1) && s1 % s0 != 0 && s0 != 0 && 
  s1 != 0 && n % m % n != 0 && m % n != 0 && n != 0)
{
  int s2 = m % n % n % m % n;
  return s2 % n % m % n % s2;
}