summaryrefslogtreecommitdiff
path: root/src/PrintPure.ml
diff options
context:
space:
mode:
Diffstat (limited to '')
-rw-r--r--src/PrintPure.ml6
1 files changed, 5 insertions, 1 deletions
diff --git a/src/PrintPure.ml b/src/PrintPure.ml
index 1c3d396d..8344ee41 100644
--- a/src/PrintPure.ml
+++ b/src/PrintPure.ml
@@ -226,7 +226,11 @@ let rec projection_to_string (fmt : ast_formatter) (inside : string)
let mplace_to_string (fmt : ast_formatter) (p : mplace) : string =
let name = match p.name with None -> "" | Some name -> name in
- let name = name ^ "^" ^ V.VarId.to_string p.var_id in
+ (* We add the "llbc" suffix to the variable index, because meta-places
+ * use indices of the variables in the original LLBC program, while
+ * regular places use indices for the pure variables: we want to make
+ * this explicit, otherwise it is confusing. *)
+ let name = name ^ "^" ^ V.VarId.to_string p.var_id ^ "llbc" in
projection_to_string fmt name p.projection
let place_to_string (fmt : ast_formatter) (p : place) : string =