diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
index 0600de6cb149016dd08f2d8092c799ee3db82fc9..9fcbc9de99cbf910b2f7a5ad6a2f324e80046d97 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBUnrollingCVC4Target.scala
@@ -3,9 +3,10 @@
 package leon
 package solvers.smtlib
 
+import leon.purescala.Expressions.Expr
 import purescala.Definitions.TypedFunDef
 import purescala.DefOps.typedTransitiveCallees
-import purescala.ExprOps.matchToIfThenElse
+import leon.purescala.ExprOps.{variablesOf, matchToIfThenElse}
 import smtlib.parser.Commands._
 import smtlib.parser.Terms._
 
@@ -54,4 +55,20 @@ trait SMTLIBUnrollingCVC4Target extends SMTLIBCVC4Target {
     }
   }
 
+  override def assertCnstr(expr: Expr): Unit = {
+    val existentials = variablesOf(expr).toSeq
+
+    val term = if (existentials.isEmpty) toSMT(expr)(Map()) else {
+      val es = existentials map { id =>
+        SortedVar(id2sym(id), declareSort(id.getType))
+      }
+      Exists(
+        es.head,
+        es.tail,
+        toSMT(expr)(existentials.map { id => id -> (id2sym(id): Term)}.toMap)
+      )
+    }
+    sendCommand(Assert(term))
+  }
+
 }