From 9af264f2f71b7acfdb36ced20a7f78589822e13e Mon Sep 17 00:00:00 2001
From: Nicolas Voirol <voirol.nicolas@gmail.com>
Date: Wed, 9 Dec 2015 17:36:23 +0100
Subject: [PATCH] Improved terminator reliability by increasing timeout
---
.../scala/leon/termination/Processor.scala | 2 +-
.../verification/purescala/valid/Client.scala | 18 ++++++++++++++++++
2 files changed, 19 insertions(+), 1 deletion(-)
create mode 100644 src/test/resources/regression/verification/purescala/valid/Client.scala
diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala
index 99124c5e6..bbd87b999 100644
--- a/src/main/scala/leon/termination/Processor.scala
+++ b/src/main/scala/leon/termination/Processor.scala
@@ -34,7 +34,7 @@ trait Solvable extends Processor {
val sizeUnit : UnitDef = UnitDef(FreshIdentifier("$size"),Seq(sizeModule))
val newProgram : Program = program.copy( units = sizeUnit :: program.units)
- SolverFactory.getFromSettings(context, newProgram).withTimeout(500.millisecond)
+ SolverFactory.getFromSettings(context, newProgram).withTimeout(1000.millisecond)
}
type Solution = (Option[Boolean], Map[Identifier, Expr])
diff --git a/src/test/resources/regression/verification/purescala/valid/Client.scala b/src/test/resources/regression/verification/purescala/valid/Client.scala
new file mode 100644
index 000000000..c0dd37cda
--- /dev/null
+++ b/src/test/resources/regression/verification/purescala/valid/Client.scala
@@ -0,0 +1,18 @@
+import leon.collection._
+import leon.lang._
+
+object Minimal {
+
+ case class Client(f: Int => List[Int])
+
+ val client = Client(x => List(1))
+
+ // def f(x: Int) = List(1)
+ // val client = Client(f)
+
+ def theorem() = {
+ client.f(0).size != BigInt(0)
+ } holds
+
+}
+
--
GitLab