[SMTLIB backend] Fix issue when a variable has the same name as a field

benchmarks/99-regression/02-same_name_var_field.smt2

@@ -0,0 +1,11 @@
+(set-info :source Astral)
+(set-info :status sat)
+
+(declare-sort Loc 0)
+(declare-heap (Loc Loc))
+
+(declare-const next Loc)
+
+(assert (pto next next))
+
+(check-sat)

src/backend/smtlib_backend_builder.ml

@@ -36,8 +36,8 @@ module Make (Backend : SMTLIB_BACKEND) = struct
     try translate_std_sort translate_sort sort
     with NonStandardTerm _ -> Backend.translate_non_std_sort translate_sort sort
 
-  let translate_var_decl (SMT.Variable (name, sort)) =
-    Format.asprintf "(declare-const %s %s)" (Identifier.show name) (translate_sort sort)
+  let translate_var_decl (SMT.Variable (name, sort) as var) =
+    Format.asprintf "(declare-const %s %s)" (translate_var_name var) (translate_sort sort)
 
   let translate_sort_decl = function
     | Sort.Bool | Sort.Int | Sort.Array _ | Sort.Bitvector _ -> ""

src/logics/Sort.ml

@@ -57,6 +57,15 @@ let rec show = function
   | Sum sorts -> "(" ^ (String.concat " | " @@ List.map show sorts) ^ ")"
   | Uninterpreted name -> name
 
+let rec show_kind = function
+  | Bool -> "bool"
+  | Int -> "int"
+  | Loc name -> "loc_" ^ name
+  | Finite (name, _) -> "finite_" ^ name
+  | Array (dom, range) -> "array_" ^ (show_kind dom) ^ "_" ^ (show_kind range)
+  | Bitvector width -> "bitvector_" ^ string_of_int width
+  | Uninterpreted name -> "uninterpreted_" ^ name
+
 let get_dom_sort = function
   | Set dom_sort -> dom_sort
   | Sequence dom_sort -> dom_sort

src/logics/Sort.mli

@@ -75,3 +75,5 @@ val is_atomic : t -> bool
 val substitute : t -> t -> t -> t
 (** [substitute sort pattern target] replaces all occurences of sort pattern by atomic sort
     target. *)
+
+val show_kind : t -> string