source: CIVL/mods/dev.civl.com/examples/arithmetic/sqrtCall.cvl@ cb4d4f4

#include <civlc.cvh>
#include <math.h>

$input double a;
$assume(a > 0);

void main() {
  double b = sqrt(a);
  double c = sqrt(b);
  double d = sqrt(c);

  $assert(a == d*d*d*d*d*d*d*d);
}