diff --git a/src/main/scala/leon/solvers/TimeoutSolver.scala b/src/main/scala/leon/solvers/TimeoutSolver.scala index 75121b9f6b3f6e4633fd93cfd91adec393a3c275..1ff88c1d68f0786fd55b9a7e16360713341e60e8 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 285af3753e1e9ec599adcfdd41a7f6988d0bcdcc..2975fef1931aae92d3b03826a483015dee4c5475 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))