Printing counterexample arrays made compatible with json format.

src/core/model_parser.ml

@@ -60,29 +60,31 @@ let array_add_element ~array ~index ~value =
     arr_indices = arr_index::array.arr_indices;
   }
 
-let rec print_indices sanit_print fmt indices =
+let rec print_indices fmt indices =
   match indices with
   | [] -> ()
   | index::tail ->
-    fprintf fmt "; %a -> " (print_model_value_sanit sanit_print) index.arr_index_key;
-    print_model_value_sanit sanit_print fmt index.arr_index_value;
-    print_indices sanit_print fmt tail
+    fprintf fmt "; %a -> " print_model_value index.arr_index_key;
+    print_model_value fmt index.arr_index_value;
+    print_indices fmt tail
 and
-print_array sanit_print fmt arr =
-  fprintf fmt "{others -> ";
-  print_model_value_sanit sanit_print fmt arr.arr_others;
-  print_indices sanit_print fmt arr.arr_indices;
-  fprintf fmt "}"
+print_array fmt arr =
+  fprintf fmt "[others -> ";
+  print_model_value fmt arr.arr_others;
+  print_indices fmt arr.arr_indices;
+  fprintf fmt "]"
 and
 print_model_value_sanit sanit_print fmt value =
   (* Prints model value. *)
   match value with
   | Integer s -> sanit_print fmt s
   | Unparsed s -> sanit_print fmt s
-  | Array a -> print_array sanit_print fmt a
+  | Array a ->
+    print_array str_formatter a;
+    sanit_print fmt (flush_str_formatter ());
   | Bitvector v -> sanit_print fmt (string_of_int v)
-
-let print_model_value fmt value =
+and
+print_model_value fmt value =
   print_model_value_sanit (fun fmt s -> fprintf fmt "%s" s) fmt value