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

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

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

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

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