From 26a3058659e2a1a77adce1dd15c957555a1287a4 Mon Sep 17 00:00:00 2001
From: Josh Berdine <jjb@fb.com>
Date: Fri, 26 Apr 2019 12:03:09 -0700
Subject: [PATCH] [sledge] Refine Convert Exp invariant

Reviewed By: mbouaziz

Differential Revision: D15098823

fbshipit-source-id: 53b4168d7
---
 sledge/src/llair/exp.ml | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/sledge/src/llair/exp.ml b/sledge/src/llair/exp.ml
index 303ab665d..44fd72935 100644
--- a/sledge/src/llair/exp.ml
+++ b/sledge/src/llair/exp.ml
@@ -444,7 +444,9 @@ let invariant ?(partial = false) e =
   | Var _ | Nondet _ | Label _ | Float _ -> assert_arity 0
   | Convert {dst; src} ->
       ( match args with
-      | [Integer {typ}] -> assert (Typ.equal src typ)
+      | [Integer {typ= Integer _ as typ}] -> assert (Typ.equal src typ)
+      | [arg] ->
+          assert (Option.for_all ~f:(Typ.convertible src) (typ_of arg))
       | _ -> assert_arity 1 ) ;
       assert (Typ.convertible src dst)
   | Add _ -> assert_polynomial e |> Fn.id