From 1cacc9234bfa264a7a457d959b8893a408fa10bb Mon Sep 17 00:00:00 2001
From: Manos Koukoutos <emmanouil.koukoutos@epfl.ch>
Date: Wed, 14 Oct 2015 13:36:03 +0200
Subject: [PATCH] Typos
---
src/main/scala/leon/purescala/ExprOps.scala | 16 ++++++++--------
src/main/scala/leon/synthesis/ConvertHoles.scala | 4 ++--
.../verification/VerificationSuite.scala | 4 ++--
3 files changed, 12 insertions(+), 12 deletions(-)
diff --git a/src/main/scala/leon/purescala/ExprOps.scala b/src/main/scala/leon/purescala/ExprOps.scala
index 200a9e167..c106d1393 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 a53ff8672..8c08f05e8 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 48fdd4169..c3bdc3067 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]]
--
GitLab