Use fresh names for all the abstract values (OCamlPro#811)

* Use fresh names for all abstract values

* Call fresh_string in pp_abstract_value_of_type

src/lib/frontend/models.ml

@@ -236,9 +236,9 @@ module SmtlibCounterExample = struct
     else
       E.print fmt t
 
-  let pp_abstract_value_of_type ppf (name, ty) =
+  let pp_abstract_value_of_type ppf ty =
     if not @@ Options.get_interpretation_use_underscore () then
-      Fmt.pf ppf "(as @@%s %a)" name Ty.pp_smtlib ty
+      Fmt.pf ppf "(as @@%s %a)" (Hstring.fresh_string ()) Ty.pp_smtlib ty
     else
       Fmt.pf ppf "_ "
 
@@ -264,8 +264,7 @@ module SmtlibCounterExample = struct
           let destr = Hstring.view destr in
           match find_destrs destr destrs with
           | None ->
-            let name = Hstring.fresh_string () in
-            pp_abstract_value_of_type fmt (name, ty_destr)
+            pp_abstract_value_of_type fmt ty_destr
           | Some rep -> fprintf fmt "%s " rep
         ) lbs
     in
@@ -388,8 +387,7 @@ module SmtlibCounterExample = struct
 
            let rec reps_aux reps =
              match reps with
-             | [] -> dprintf "%a" pp_abstract_value_of_type
-                       (Symbols.to_string f, ty)
+             | [] -> dprintf "%a" pp_abstract_value_of_type ty
              | [srep,xs_values_list] ->
                if Options.get_interpretation_use_underscore () then
                  dprintf "(@[<hv>ite %t@ %a@ %t)@]"
@@ -476,9 +474,8 @@ let rec pp_value ppk ppf = function
   | Constant (sy, t) -> ppk ppf (sy, t)
   | Value (_, s) -> Format.pp_print_string ppf s
 
-let pp_constant ppf (sy, t) =
-  Fmt.pf ppf "%a" SmtlibCounterExample.pp_abstract_value_of_type
-    (Symbols.to_string sy, t)
+let pp_constant ppf (_sy, t) =
+  Fmt.pf ppf "%a" SmtlibCounterExample.pp_abstract_value_of_type t
 
 let output_concrete_model fmt props ~functions ~constants ~arrays =
   if ModelMap.(is_suspicious functions || is_suspicious constants

tests/cram.t/run.t

@@ -11,7 +11,7 @@ appropriate here.
 
   unknown
   (
-    (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
+    (define-fun a1 () (Array Int Int) (store (as @!k1 (Array Int Int)) 0 0))
     (define-fun x () Int 0)
     (define-fun y () Int 0)
   )

tests/issues/555.models.expected

@@ -1,7 +1,7 @@
 
 unknown
 (
-  (define-fun a1 () (Array Int Int) (store (as @a1 (Array Int Int)) 0 0))
+  (define-fun a1 () (Array Int Int) (store (as @!k1 (Array Int Int)) 0 0))
   (define-fun x () Int 0)
   (define-fun y () Int 0)
 )