From 28ad97d2b71956e76a8a67b96ffed364a62c8aec Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 27 Aug 2022 23:42:19 -0400 Subject: [PATCH] fix: typecheck issue --- src/smtlib/Typecheck.ml | 4 ++-- 1 file changed, 2 insertions(+), 2 deletions(-) diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index 46ef5259..61b157f0 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -128,13 +128,13 @@ let t_as_q t = | _ -> None *) -let is_real = Ty.is_real +let is_real t = Ty.is_real (T.ty t) (* convert [t] to a real term *) let cast_to_real (ctx : Ctx.t) (t : T.t) : T.t = let conv t = match T.view t with - | _ when Ty.is_real (T.ty t) -> t + | _ when is_real t -> t (* FIXME | T.LIA (Const n) -> T.lra ctx.tst (Const (Q.of_bigint n)) | T.LIA l ->