diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 200a9e167e8d70e076b9d13fc7c301331e127138..c106d1393bcf793a7fe5d6944ecd533d84a42e36 100644
--- a/src/main/scala/leon/purescala/ExprOps.scala
+++ b/src/main/scala/leon/purescala/ExprOps.scala
@@ -1474,14 +1474,14 @@ object ExprOps {
       val solver = SimpleSolverAPI(sf)
 
       toCheck.forall { cond =>
-        solver.solveSAT(cond) match {
-            case (Some(false), _)  =>
-              true
-            case (Some(true), model)  =>
-              false
-            case (None, _)  =>
-              // Should we be optimistic here?
-              false
+        solver.solveSAT(cond)._1 match {
+          case Some(false) =>
+            true
+          case Some(true)  =>
+            false
+          case None =>
+            // Should we be optimistic here?
+            false
         }
       }
     case _ =>
diff --git a/src/main/scala/leon/synthesis/ConvertHoles.scala b/src/main/scala/leon/synthesis/ConvertHoles.scala
index a53ff8672082d03873141e21c1f11141281095fd..8c08f05e89f6fcb133609802ffe46c686e40fa36 100644
--- a/src/main/scala/leon/synthesis/ConvertHoles.scala
+++ b/src/main/scala/leon/synthesis/ConvertHoles.scala
@@ -15,7 +15,7 @@ object ConvertHoles extends TransformationPhase {
   val description = "Convert Holes found in bodies to equivalent Choose"
 
   /**
-   * This phase converts a body with "withOracle{ .. }" into a choose construct:
+   * This phase converts a body with "???" into a choose construct:
    *
    * def foo(a: T) = {
    *   require(..a..)
@@ -44,7 +44,7 @@ object ConvertHoles extends TransformationPhase {
     (pre ++ post).foreach {
       preTraversal{
         case h : Hole =>
-          ctx.reporter.error("Holes are not supported in preconditions. @"+ h.getPos)
+          ctx.reporter.error("Holes are not supported in pre- or postconditions. @"+ h.getPos)
         case _ =>
       }
     }
diff --git a/src/test/scala/leon/regression/verification/VerificationSuite.scala b/src/test/scala/leon/regression/verification/VerificationSuite.scala
index 48fdd416931ffefefed6c3ee1447320a1e185f48..c3bdc306798cc4a298b8819cdfe7330d8b37d3ce 100644
--- a/src/test/scala/leon/regression/verification/VerificationSuite.scala
+++ b/src/test/scala/leon/regression/verification/VerificationSuite.scala
@@ -15,8 +15,8 @@ import leon.xlang.FixReportLabels
 
 import org.scalatest.{Reporter => _, _}
 
-// If you add another regression test, make sure it contains one object whose name matches the file name
-// This is because we compile all tests from each folder separately.
+// If you add another regression test, make sure it contains exactly one object, whose name matches the file name.
+// This is because we compile all tests from each folder together.
 trait VerificationSuite extends LeonRegressionSuite {
 
   val optionVariants: List[List[String]]