int multiply(int m, int n) {
  
  int p = 1;
  int i;
  for (i = 0; i <= n; i++) {
    p = p * m;
  }
  // assert (p >= 1);
  return p;
}

int nondet_int();

void main(void)
{
  int a = nondet_int();  
  int b = nondet_int();
  __CPROVER_assume(a > 0 && b > 0);

  int result = multiply(a,b);  
  assert (result >= 1);
}
