Commit a4d0d0fe authored by Guillaume Melquiond's avatar Guillaume Melquiond

Detect syntax errors in CVC3 files.

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)))));
parent 45a49413
......@@ -5,6 +5,8 @@ prelude "%%% this is a prelude for CVC3 "
printer "cvc3"
filename "%f-%t-%g.cvc"
(* 'fail' must be before 'valid'; otherwise it is ignored *)
fail "Parse Error: \\(.*\\)" "\\1"
valid "Valid."
unknown "Unknown." ""
time "why3cpulimit time : %s s"
......
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment