source: CIVL/examples/arithmetic/quadratic1.cvl@ 1aaefd4

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

$input int x;
$assume(1 < x && x <= 3);
$input int y;
$assume(1 < y && y <= 3);
$input int n = x * y;

int main(){
  assert(1 < n && n <= 9);
}