diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
index 678d5915fb38c0693be593b9baf90e3ee4453850..d8f94c40cf61e831f907d62608b478dd27b8329c 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4ProofSolver.scala
@@ -3,7 +3,11 @@
 package leon
 package solvers.smtlib
 
+import leon.purescala.Common.Identifier
 import leon.purescala.Definitions.Program
+import leon.purescala.Expressions.Expr
+import smtlib.parser.Commands.{Assert => SMTAssert}
+import smtlib.parser.Terms.Exists
 
 class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTLIBCVC4QuantifiedSolver(context, program) {
 
@@ -23,4 +27,29 @@ class SMTLIBCVC4ProofSolver(context: LeonContext, program: Program) extends SMTL
     ) ++ userDefinedOps(ctx)
   }
 
+  // For this solver, we prefer the variables of assert() commands to be exist. quantified instead of free
+  override def assertCnstr(expr: Expr) =
+    try {
+      sendCommand(SMTAssert(quantifiedTerm(Exists, expr)))
+    } catch {
+      case _ : IllegalArgumentException =>
+        addError()
+    }
+
+  // This solver does not support model extraction
+  override def getModel: Map[Identifier, Expr] = {
+    reporter.warning(s"Solver $name does not support model extraction.")
+    Map()
+  }
+
+  // FIXME: mk: This is kind of hiding the problem under the carpet.
+  // We could just return an empty counterexample, but this breaks PortfolioSolver
+  override def check: Option[Boolean] = {
+    super.check match {
+      case Some(true) =>
+        reporter.warning(s"Solver $name found a counterexample, but masking it as unknown because counterexamples are not supported.")
+        None
+      case other => other
+    }
+  }
 }
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
index 53239581b267bd8fce175541202e744809c2e4c0..e4f55acef605a73e49cde947ad1be2eb4d5febf3 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBCVC4QuantifiedSolver.scala
@@ -10,7 +10,7 @@ import Constructors.{application, implies}
 import DefOps.typedTransitiveCallees
 import verification.VC
 import smtlib.parser.Commands.{Assert => SMTAssert, FunDef => _, _}
-import smtlib.parser.Terms._
+import smtlib.parser.Terms.{Exists => SMTExists, ForAll => SMTForall, _ }
 import smtlib.theories.Core.Equals
 
 // This solver utilizes the define-funs-rec command of SMTLIB-2.5 to define mutually recursive functions.
@@ -103,13 +103,13 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
         tfd <- notSeen if !refersToCurrent(tfd.fd)
         post <- tfd.postcondition
       } {
-        //println(s"${tfd.id.uniqueName} does not refer to ${currentFunDef.get.id.uniqueName}")
+        //currentFunDef foreach { f => println(s"${tfd.id.uniqueName} does not refer to ${f.id.uniqueName}") }
         val term = implies(
           tfd.precondition getOrElse BooleanLiteral(true),
           application(post, Seq(FunctionInvocation(tfd, tfd.params map { _.toVariable})))
         )
         try {
-          sendCommand(SMTAssert(quantifiedTerm(ForAll, term)))
+          sendCommand(SMTAssert(quantifiedTerm(SMTForall, term)))
         } catch {
           case _ : IllegalArgumentException =>
             addError()
@@ -123,20 +123,12 @@ abstract class SMTLIBCVC4QuantifiedSolver(context: LeonContext, program: Program
 
   }
 
-  // For this solver, we prefer the variables of assert() commands to be exist. quantified instead of free
-  override def assertCnstr(expr: Expr) =
-    try {
-      sendCommand(SMTAssert(quantifiedTerm(Exists, expr)))
-    } catch {
-      case _ : IllegalArgumentException =>
-        addError()
-    }
-
   // We need to know the function context.
   // The reason is we do not want to assume postconditions of functions referring to 
   // the current function, as this may make the proof unsound
   override def assertVC(vc: VC) = {
     currentFunDef = Some(vc.fd)
+    //println("Setting fundef to " + currentFunDef.get.id.uniqueName)
     super.assertVC(vc)
   }
 
diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index d1cb3db34b26979d09377aedaf3ed785991536d0..a4c06d3b8597426eee0aa719631009b7e513ed7f 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
@@ -847,14 +847,18 @@ abstract class SMTLIBSolver(val context: LeonContext,
         )
 
 
-      val GetValueResponseSuccess(valuationPairs) = sendCommand(cmd)
+      sendCommand(cmd) match {
+        case GetValueResponseSuccess(valuationPairs) =>
 
-      valuationPairs.collect {
-        case (SimpleSymbol(sym), value) if variables.containsB(sym) =>
-          val id = variables.toA(sym)
+          valuationPairs.collect {
+            case (SimpleSymbol(sym), value) if variables.containsB(sym) =>
+              val id = variables.toA(sym)
 
-          (id, fromSMT(value, id.getType)(Map(), Map()))
-      }.toMap
+              (id, fromSMT(value, id.getType)(Map(), Map()))
+          }.toMap
+        case _ =>
+          Map() //FIXME improve this
+      }
     }
   }