diff --git a/src/interpretation.ml b/src/interpretation.ml
index e5dd6c9add0e7b76e3a2d31abf3420d0778c74fe..4d5af8bad9c4fa51374ba4900e9a3b8ae71b1a5c 100644
--- a/src/interpretation.ml
+++ b/src/interpretation.ml
@@ -332,7 +332,7 @@ let bounded_quant engine vs ~cond : CRE.bounded_quant_result option =
       in
       let new_quant =
         List.init n ~f:(fun _ ->
-          let preid = Ident.id_fresh "caisar_v" in
+          let preid = Ident.id_fresh "caisar_x" in
           Term.create_vsymbol preid ty)
       in
       let args = List.map new_quant ~f:(fun vs -> (Term.t_var vs, ty)) in
diff --git a/src/transformations/native_nn_prover.ml b/src/transformations/native_nn_prover.ml
index b28e8e8a40c398712859db1ea3b9d15534306d2b..5cf1cb77e2c39f70ff48c0316d52de7b6bed3954 100644
--- a/src/transformations/native_nn_prover.ml
+++ b/src/transformations/native_nn_prover.ml
@@ -62,7 +62,8 @@ let create_output_vars =
         | None ->
           let output_vars =
             List.init nn_nb_outputs ~f:(fun index ->
-              (index, Term.create_fsymbol (Ident.id_fresh "y") [] nn_ty_elt))
+              ( index,
+                Term.create_fsymbol (Ident.id_fresh "caisar_y") [] nn_ty_elt ))
           in
           Term.Mterm.add term output_vars mt
         | Some _ -> mt)