From 255ec4a98d329d021dbc86ca81a59d562efaa8d1 Mon Sep 17 00:00:00 2001
From: Alex Auvolat <alex.auvolat@ansys.com>
Date: Wed, 25 Jun 2014 09:51:51 +0200
Subject: Differentiate pre witin different scopes.

---
 abstract/transform.ml | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'abstract')

diff --git a/abstract/transform.ml b/abstract/transform.ml
index 82b6731..b9c173d 100644
--- a/abstract/transform.ml
+++ b/abstract/transform.ml
@@ -61,6 +61,7 @@ let rec f_of_neexpr td (node, prefix) where expr =
       | _ -> le invalid_arity "binary operator") a
   (* temporal *)
   | AST_pre(expr, id) ->
+    let id = node^"/"^id in
     let typ = type_expr td.rp node expr in
       where
         (List.mapi
@@ -183,6 +184,7 @@ let rec f_of_scope active td (node, prefix, eqs) assume_guarantees =
     let eq_i = f_and_list (List.map instance_eq (extract_instances td.rp.p e)) in
 
     let pre_expr (id, expr) =
+      let id = node^"/"^id in
       if active then
         f_of_neexpr td (node, prefix) (fun elist ->
             list_fold_op f_and
-- 
cgit v1.2.3