#include<civlc.cvh>

double f(double x) 
  $requires x > 0;
  $ensures $true;
  ;

double g(double x)
  $requires x > 0;
  $ensures $result >= 0;
{
  return g(x)*g(x);
}

double main() {
  return g(2);
}