From 77b33346f5620ad57f7b6e8ebe6d3f747a99b263 Mon Sep 17 00:00:00 2001 From: Simon Cruanes Date: Sat, 14 Nov 2020 13:17:23 -0500 Subject: [PATCH] fix(tycheck): handle proper unary minus --- src/smtlib/Typecheck.ml | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/smtlib/Typecheck.ml b/src/smtlib/Typecheck.ml index ce89c1d4..80337856 100644 --- a/src/smtlib/Typecheck.ml +++ b/src/smtlib/Typecheck.ml @@ -280,6 +280,12 @@ let rec conv_term (ctx:Ctx.t) (t:PA.term) : T.t = | PA.Add, [a;b] -> T.lra ctx.tst (LRA_op (Plus, a, b)) | PA.Add, (a::l) -> List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Plus,a,b))) a l + | PA.Minus, [a] -> + begin match t_as_q a with + | Some a -> T.lra ctx.tst (LRA_const (Q.neg a)) + | None -> + T.lra ctx.tst (LRA_op (Minus, T.lra ctx.tst (LRA_const Q.zero), a)) + end | PA.Minus, [a;b] -> T.lra ctx.tst (LRA_op (Minus, a, b)) | PA.Minus, (a::l) -> List.fold_left (fun a b -> T.lra ctx.tst (LRA_op (Minus,a,b))) a l