[sledge] Refine Convert Exp invariant

Reviewed By: mbouaziz

Differential Revision: D15098823

fbshipit-source-id: 53b4168d7
master
Josh Berdine 6 years ago committed by Facebook Github Bot
parent 0d70f57c6f
commit 26a3058659

@ -444,7 +444,9 @@ let invariant ?(partial = false) e =
| Var _ | Nondet _ | Label _ | Float _ -> assert_arity 0 | Var _ | Nondet _ | Label _ | Float _ -> assert_arity 0
| Convert {dst; src} -> | Convert {dst; src} ->
( match args with ( 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_arity 1 ) ;
assert (Typ.convertible src dst) assert (Typ.convertible src dst)
| Add _ -> assert_polynomial e |> Fn.id | Add _ -> assert_polynomial e |> Fn.id

Loading…
Cancel
Save