From 7c92a88bdd2bf0c4bd8d842eb97805644054c396 Mon Sep 17 00:00:00 2001
From: Michele Alberti <michele.alberti@cea.fr>
Date: Tue, 30 May 2023 13:20:18 +0200
Subject: [PATCH] [interpretation][trans] Use caisar_x/caisar_y to refer to
input/output variables.
---
src/interpretation.ml | 2 +-
src/transformations/native_nn_prover.ml | 3 ++-
2 files changed, 3 insertions(+), 2 deletions(-)
diff --git a/src/interpretation.ml b/src/interpretation.ml
index e5dd6c9..4d5af8b 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 b28e8e8..5cf1cb7 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)
--
GitLab