diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
index 536ad9e009ba6aee3eb622bf1133b1379d5421f6..d55f225bc96fc83319f1cf0ae41f503a7c5a873d 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBTarget.scala
@@ -460,10 +460,12 @@ trait SMTLIBTarget {
           case (_: Or) => Core.Or(sub.map(toSMT): _*)
           case (_: IfExpr) => Core.ITE(toSMT(sub(0)), toSMT(sub(1)), toSMT(sub(2))) 
           case (f: FunctionInvocation) => 
-            FunctionApplication(
-              declareFunction(f.tfd),
-              sub.map(toSMT)
-            )
+            if (sub.isEmpty) declareFunction(f.tfd) else {
+              FunctionApplication(
+                declareFunction(f.tfd),
+                sub.map(toSMT)
+              )
+            }
           case _ => reporter.fatalError("Unhandled nary "+e)
         }