diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index 382122cba66859e68810bfce2f2b26aae83f40f0..9704fceba0a5245f428c7925389c521853e003e8 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -40,7 +40,9 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
       val s = super.declareFunction(tfd)
 
       try {
-        val bodyAssert = SMTAssert(Equals(s: Term, toSMT(tfd.body.get)(Map())))
+        val bodyAssert = tfd.body map { bd =>
+          SMTAssert(Equals(s: Term, toSMT(bd)(Map())))
+        }
 
         val specAssert = tfd.postcondition map { post =>
           val term = implies(
@@ -50,7 +52,7 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
           SMTAssert(toSMT(term)(Map()))
         }
 
-        Seq(bodyAssert) ++ specAssert
+        bodyAssert ++ specAssert
       } catch {
         case _ : SolverUnsupportedError =>
           addError()