From 20334e0f8d1115bf7f70226f5020df180d5d7f89 Mon Sep 17 00:00:00 2001
From: Brian Campbell
Date: Tue, 29 Jan 2019 16:54:36 +0000
Subject: Support case splitting on variables as well as sizeof in cast
 introduction

---
 src/monomorphise.ml | 7 +++++++
 1 file changed, 7 insertions(+)

(limited to 'src')

diff --git a/src/monomorphise.ml b/src/monomorphise.ml
index 76a48cd7..666abe86 100644
--- a/src/monomorphise.ml
+++ b/src/monomorphise.ml
@@ -4107,6 +4107,13 @@ let add_bitvector_casts (Defs defs) =
               (match destruct_atom_nexp (env_of y) (typ_of y) with
               | Some (Nexp_aux (Nexp_constant i,_)) -> [(kid,i)]
               | _ -> [])
+           | E_app (op,[x;y])
+               when string_of_id op = "eq_int" ->
+              (match destruct_atom_nexp (env_of x) (typ_of x), destruct_atom_nexp (env_of y) (typ_of y) with
+              | Some (Nexp_aux (Nexp_var kid,_)), Some (Nexp_aux (Nexp_constant i,_))
+              | Some (Nexp_aux (Nexp_constant i,_)), Some (Nexp_aux (Nexp_var kid,_))
+                -> [(kid,i)]
+              | _ -> [])
            | E_app (op, [x;y]) when string_of_id op = "and_bool" ->
               extract x @ extract y
            | _ -> []
-- 
cgit v1.2.3