Note that CVC3 doesn't care about syntax errors and it will still answer
valid at the end. Currently, CVC3 chokes on the following kind of
declarations (Div_mult, Abs_real_pos, and so on).

  ASSERT
  (FORALL (x : INT, y : INT, z : INT):PATTERN (div(((x * y) + z), x)):
  (((0 < x) AND ((0 <= y) AND (0 <= z))) => (div(((x * y) + z), x) = (y +
  div(z, x)))));