diff --git a/src/core/model_parser.ml b/src/core/model_parser.ml index f32ab25065ad37316f667b221928261b1875d76f..0df58a2ead47a90fed3e0f515fd1b15af15bd38c 100644 --- a/src/core/model_parser.ml +++ b/src/core/model_parser.ml @@ -31,7 +31,7 @@ type model_value = | Integer of string | Decimal of (string * string) | Array of model_array - | Bitvector of int + | Bitvector of string | Unparsed of string and arr_index = { arr_index_key : model_value; @@ -87,7 +87,7 @@ print_model_value_sanit sanit_print fmt value = | Array a -> print_array str_formatter a; sanit_print fmt (flush_str_formatter ()) - | Bitvector v -> sanit_print fmt (string_of_int v) + | Bitvector v -> sanit_print fmt v and print_model_value fmt value = print_model_value_sanit (fun fmt s -> fprintf fmt "%s" s) fmt value diff --git a/src/core/model_parser.mli b/src/core/model_parser.mli index 0693633c56b5ac947c8238a40648295f6b75c850..da0abc8892c8284e6f32fad2772e4b5a52a31f33 100644 --- a/src/core/model_parser.mli +++ b/src/core/model_parser.mli @@ -18,7 +18,7 @@ type model_value = | Integer of string | Decimal of (string * string) | Array of model_array - | Bitvector of int + | Bitvector of string | Unparsed of string and arr_index = { arr_index_key : model_value; diff --git a/src/driver/parse_smtv2_model_lexer.mll b/src/driver/parse_smtv2_model_lexer.mll index f06be25a5d6ba1b516eabe3ec99bf2b757958e8c..712ce98f07be0fcd14633674d418ec97f575422d 100644 --- a/src/driver/parse_smtv2_model_lexer.mll +++ b/src/driver/parse_smtv2_model_lexer.mll @@ -20,7 +20,7 @@ rule token = parse { LPAREN } | ')' { RPAREN } - | "(_ bv"(num as bv_value)" "num")" { BITVECTOR_VALUE (int_of_string bv_value) } + | "(_ bv"(num as bv_value)" "num")" { BITVECTOR_VALUE bv_value } | num as integer { INT_STR (integer) } | '-'space*(num as integer) { MINUS_INT_STR ("-"^integer) } diff --git a/src/driver/parse_smtv2_model_parser.mly b/src/driver/parse_smtv2_model_parser.mly index de8bde6a8ebb00ef423c31c431a8c098d5949897..2f6668a235ee4bfb9ec369bfff49f5a139b86a66 100644 --- a/src/driver/parse_smtv2_model_parser.mly +++ b/src/driver/parse_smtv2_model_parser.mly @@ -7,7 +7,7 @@ %token STORE %token CONST %token AS -%token <int> BITVECTOR_VALUE +%token <string> BITVECTOR_VALUE %token <string> INT_STR %token <string> MINUS_INT_STR %token <string * string> DEC_STR