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