From e69595de4ebdaf6af0e222dbf226082c2a9aa475 Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Fri, 19 Jun 2015 18:58:48 +0200
Subject: [PATCH] Report timeouts as timeouts, not unknown
---
src/main/scala/leon/solvers/TimeoutSolver.scala | 2 +-
.../scala/leon/verification/AnalysisPhase.scala | 13 ++++++++++++-
2 files changed, 13 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/solvers/TimeoutSolver.scala b/src/main/scala/leon/solvers/TimeoutSolver.scala
index 75121b9f6..1ff88c1d6 100644
--- a/src/main/scala/leon/solvers/TimeoutSolver.scala
+++ b/src/main/scala/leon/solvers/TimeoutSolver.scala
@@ -9,7 +9,7 @@ trait TimeoutSolver extends Solver with Interruptible {
val ti = new TimeoutFor(this)
- protected var optTimeout: Option[Long] = None
+ var optTimeout: Option[Long] = None
def setTimeout(timeout: Long): this.type = {
optTimeout = Some(timeout)
diff --git a/src/main/scala/leon/verification/AnalysisPhase.scala b/src/main/scala/leon/verification/AnalysisPhase.scala
index 285af3753..2975fef19 100644
--- a/src/main/scala/leon/verification/AnalysisPhase.scala
+++ b/src/main/scala/leon/verification/AnalysisPhase.scala
@@ -150,7 +150,18 @@ object AnalysisPhase extends LeonPhase[Program,VerificationReport] {
VCResult(VCStatus.Cancelled, Some(s), Some(dt))
case None =>
- VCResult(VCStatus.Unknown, Some(s), Some(dt))
+ val status = s match {
+ case ts: TimeoutSolver =>
+ ts.optTimeout match {
+ case Some(t) if t < dt =>
+ VCStatus.Timeout
+ case _ =>
+ VCStatus.Unknown
+ }
+ case _ =>
+ VCStatus.Unknown
+ }
+ VCResult(status, Some(s), Some(dt))
case Some(false) =>
VCResult(VCStatus.Valid, Some(s), Some(dt))
--
GitLab