Commit 772f4fc5 authored by David Hauzar's avatar David Hauzar

OB10-023 Parse prover output with presence of mk_t__ref.

Enabling the transformation detect_polymorphism caused some variables be
of reference type and their values outputed in the form "mk_t__ref value".
This was not recognized by the counterexample model parser.

* src/driver/parse_smtv2_model_lexer.mll
Add new token corresponding to string "mk_t__ref"

* src/driver/parse_smtv2_model_parser.mly
Value can be also of the form "(mk_t__ref value)"
parent 69de5f30
...@@ -13,6 +13,7 @@ rule token = parse ...@@ -13,6 +13,7 @@ rule token = parse
{ token lexbuf } { token lexbuf }
| space+ as space_str | space+ as space_str
{ SPACE (space_str) } { SPACE (space_str) }
| "mk_t__ref" { MK_T_REF }
| "store" { STORE } | "store" { STORE }
| "const" { CONST } | "const" { CONST }
| "as" { AS } | "as" { AS }
......
...@@ -13,6 +13,7 @@ ...@@ -13,6 +13,7 @@
%token <string * string> DEC_STR %token <string * string> DEC_STR
%token <string * string> MINUS_DEC_STR %token <string * string> MINUS_DEC_STR
%token LPAREN RPAREN %token LPAREN RPAREN
%token MK_T_REF
%token EOF %token EOF
%% %%
...@@ -53,6 +54,7 @@ text_without_int: ...@@ -53,6 +54,7 @@ text_without_int:
| AS { "as" } | AS { "as" }
value: value:
| LPAREN MK_T_REF SPACE value RPAREN { $4 }
| integer { $1 } | integer { $1 }
| decimal { $1 } | decimal { $1 }
| other_val_str { Model_parser.Unparsed $1 } | other_val_str { Model_parser.Unparsed $1 }
......
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