@requires true

@ensures ans = x * x

@program
     @var x, ans : int
    
     ans = x + 1;
     ans = ans * (x - 1);
     ans = ans + 1;

@end
--