diff --git a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala index 3e04edf2747abf4327dfe6801372bc606fd99417..b7cefba50d26eca526a4933f8674796c901be850 100644 --- a/src/test/scala/leon/test/synthesis/SynthesisSuite.scala +++ b/src/test/scala/leon/test/synthesis/SynthesisSuite.scala @@ -23,7 +23,7 @@ class SynthesisSuite extends LeonTestSuite { counter } - def forProgram(title: String)(content: String)(block: (SynthesisContext, FunDef, Problem) => Unit) { + def forProgram(title: String, opts: SynthesisOptions = SynthesisOptions())(content: String)(block: (SynthesisContext, FunDef, Problem) => Unit) { val ctx = testContext.copy(settings = Settings( synthesis = true, @@ -31,8 +31,6 @@ class SynthesisSuite extends LeonTestSuite { verify = false )) - val opts = SynthesisOptions() - val pipeline = leon.utils.TemporaryInputPhase andThen leon.frontends.scalac.ExtractionPhase andThen SynthesisProblemExtractionPhase val (program, results) = pipeline.run(ctx)((content, Nil)) @@ -123,6 +121,31 @@ class SynthesisSuite extends LeonTestSuite { } } + forProgram("Ground Enum", SynthesisOptions(selectedSolvers = Set("enum")))( + """ +import scala.collection.immutable.Set +import leon.annotation._ +import leon.lang._ + +object Injection { + sealed abstract class List + case class Cons(tail: List) extends List + case class Nil() extends List + + // proved with unrolling=0 + def size(l: List) : Int = (l match { + case Nil() => 0 + case Cons(t) => 1 + size(t) + }) ensuring(res => res >= 0) + + def simple() = choose{out: List => size(out) == 2 } +} + """ + ) { + case (sctx, fd, p) => + assertAllAlternativesSucceed(sctx, rules.Ground.instantiateOn(sctx, p)) + } + forProgram("Cegis 1")( """ import scala.collection.immutable.Set