Commit 9f3d1f66 authored by David Hauzar's avatar David Hauzar

OA21-004 OB13-062 Fix of parsing counterexample model returned by cvc4.

In a counterexample model returned by cvc4, values can be also of the form
"(mk_t__ref([0-9]*) (value))", while only the form "(mk_t__ref (value))"
was supported.

* src/driver/parse_smtv2_model_lexer.mll
MK_T__REF can be of the form "mk_t__ref([0-9]*)".
parent 772f4fc5
......@@ -13,7 +13,7 @@ rule token = parse
{ token lexbuf }
| space+ as space_str
{ SPACE (space_str) }
| "mk_t__ref" { MK_T_REF }
| "mk_t__ref"(num*) { MK_T_REF }
| "store" { STORE }
| "const" { CONST }
| "as" { AS }
......
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