diff --git a/src/main/scala/leon/termination/Processor.scala b/src/main/scala/leon/termination/Processor.scala index 99124c5e64ed8bb61e3c44a015775280d06c584e..bbd87b999e653a943598915e7d2e38a9aba20bff 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 0000000000000000000000000000000000000000..c0dd37cda62e30202e9255b534685f9e0e9b840a --- /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 + +} +