Use fresh names for all abstract values

Halbaroth · Sep 12, 2023 · 23c17a5 · 23c17a5
1 parent 36e5fe6
commit 23c17a5
Show file tree

Hide file tree

Showing 3 changed files with 5 additions and 5 deletions.
diff --git a/src/lib/frontend/models.ml b/src/lib/frontend/models.ml
@@ -389,7 +389,7 @@ module SmtlibCounterExample = struct
            let rec reps_aux reps =
              match reps with
              | [] -> dprintf "%a" pp_abstract_value_of_type
-                       (Symbols.to_string f, ty)
+                       (Hstring.fresh_string (), ty)
              | [srep,xs_values_list] ->
                if Options.get_interpretation_use_underscore () then
                  dprintf "(@[<hv>ite %t@ %a@ %t)@]"
@@ -476,9 +476,9 @@ 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) =
+let pp_constant ppf (_sy, t) =
   Fmt.pf ppf "%a" SmtlibCounterExample.pp_abstract_value_of_type
-    (Symbols.to_string sy, t)
+    (Hstring.fresh_string (), t)
 
 let output_concrete_model fmt props ~functions ~constants ~arrays =
   if ModelMap.(is_suspicious functions || is_suspicious constants

diff --git a/tests/cram.t/run.t b/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)
   )

diff --git a/tests/issues/555.models.expected b/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)
 )