Commit 3f732c46 authored by Sylvain Dailler's avatar Sylvain Dailler

Q418-025 Printing arrays with bv indices

This commits allows printing of arrays which have indices typed as
bitvectors.

* src/driver/collect_data_model.ml
(convert_to_indice): Add bitvector case.

Change-Id: Iafe10e5e6cd1aab0a3e023aeb69df03fde8880e8
parent af6c3d91
...@@ -198,6 +198,7 @@ and refine_variable_value (table: correspondence_table) key v = ...@@ -198,6 +198,7 @@ and refine_variable_value (table: correspondence_table) key v =
let convert_to_indice t = let convert_to_indice t =
match t with match t with
| Integer i -> i | Integer i -> i
| Bitvector bv -> bv
| _ -> raise Not_value | _ -> raise Not_value
let rec convert_array_value (a: array) : Model_parser.model_array = let rec convert_array_value (a: array) : Model_parser.model_array =
......
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