source: CIVL/examples/arithmetic/sqrt.cvl@ 7c66e72

#include <math.h>
#include <assert.h>

$input double x;
$assume x >= 0.0;

int main() {
  double y = sqrt(x) + 1;

  assert(y >= 1);
  return 0;
}