From 7b4bf2bd14cae99a4d8086a0b66d9875be1acbab Mon Sep 17 00:00:00 2001
From: Alasdair Armstrong
Date: Tue, 21 May 2019 17:31:13 +0100
Subject: SMT: Use a separate constructor for memory read variables

We want to ensure simplication can treat these separately so we
don't accidentally simplify away dependencies between reads and write
addresses.
---
 src/jib/jib_smt.ml | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

(limited to 'src/jib')

diff --git a/src/jib/jib_smt.ml b/src/jib/jib_smt.ml
index 7420707c..0d6f42fe 100644
--- a/src/jib/jib_smt.ml
+++ b/src/jib/jib_smt.ml
@@ -1044,7 +1044,7 @@ let builtin_read_mem ctx rk addr_size addr data_size ret_ctyp =
   let name = "R" ^ string_of_int !reads in
   [Read_mem (name, ctx.node, Lazy.force ctx.pathcond, smt_ctyp ctx ret_ctyp, smt_cval ctx rk,
              smt_cval ctx addr, smt_ctyp ctx (cval_ctyp addr))],
-  Var (name ^ "_ret")
+  Read_res name
 
 let excl_results = ref (-1)
 
@@ -1626,7 +1626,7 @@ module Make_optimizer(S : Sequence) = struct
          | Some n -> Hashtbl.replace uses var (n + 1)
          | None -> Hashtbl.add uses var 1
          end
-      | Enum _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> ()
+      | Enum _ | Read_res _ | Hex _ | Bin _ | Bool_lit _ | String_lit _ | Real_lit _ -> ()
       | Fn (_, exps) | Ctor (_, exps) ->
          List.iter uses_in_exp exps
       | Ite (cond, t, e) ->
-- 
cgit v1.2.3