source: CIVL/examples/arithmetic/division.cvl

/* division.cvl: simple real division, whose correctness
 * depends on real arithmetic.
 * 
 * Commandline execution:
 *              civl verify division.cvl
 */
$input double x;
$input double y;
$assume(y!=0);

void main() {
  double z = x/y;
  $assert(y*z==x);
}