From d91e3a1b2ce4b7cdd74bbb878b9adf8dbafe6eee Mon Sep 17 00:00:00 2001
From: Etienne Kneuss <ekneuss@gmail.com>
Date: Thu, 1 Nov 2012 15:31:48 +0100
Subject: [PATCH] Reduce number of tries
---
src/main/scala/leon/synthesis/Rules.scala | 2 +-
testcases/synthesis/SortedList.scala | 2 +-
2 files changed, 2 insertions(+), 2 deletions(-)
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index ace65b430..8b78e8429 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -114,7 +114,7 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
val tpe = TupleType(p.xs.map(_.getType))
var i = 0;
- var maxTries = 5;
+ var maxTries = 3;
var result: Option[RuleResult] = None
var predicates: Seq[Expr] = Seq()
diff --git a/testcases/synthesis/SortedList.scala b/testcases/synthesis/SortedList.scala
index b63c42352..2e5a42ff9 100644
--- a/testcases/synthesis/SortedList.scala
+++ b/testcases/synthesis/SortedList.scala
@@ -13,7 +13,7 @@ object SortedList {
case Cons(_, t) => 1 + size(t)
}) ensuring(res => res >= 0)
- def sizeSynth(l: List): Int = choose{ (i: Int) => i >= 0 && sizeSynth(Cons(0, l)) == i + 1}
+ //def sizeSynth(l: List): Int = choose{ (i: Int) => i >= 0 && sizeSynth(Cons(0, l)) == i + 1}
def content(l: List): Set[Int] = l match {
case Nil() => Set()
--
GitLab