diff --git a/src/main/scala/leon/synthesis/rules/Tegis.scala b/src/main/scala/leon/synthesis/rules/Tegis.scala index c436b6ed0d3aced39e181c40ee29d6549a0574cd..3ce5a908902304cd0f39ed856b5cf34717b2408a 100644 --- a/src/main/scala/leon/synthesis/rules/Tegis.scala +++ b/src/main/scala/leon/synthesis/rules/Tegis.scala @@ -33,18 +33,6 @@ case object TEGIS extends Rule("TEGIS") { def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = { - // check if the formula contains passes: - if (!sctx.program.library.passes.isDefined) { - return Nil; - } - - val passes = sctx.program.library.passes.get - - val mayHaveTests = exists({ - case FunctionInvocation(TypedFunDef(`passes`, _), _) => true - case _ => false - })(p.phi) - List(new RuleInstantiation(p, this, SolutionBuilder.none, this.name, this.priority) { def apply(sctx: SynthesisContext): RuleApplication = { diff --git a/src/main/scala/leon/utils/Library.scala b/src/main/scala/leon/utils/Library.scala index 5b5621b142de012ed1d5b58918086f88f0537461..2a254a8610fbcd38f6bebe9673d9615b252ff8f5 100644 --- a/src/main/scala/leon/utils/Library.scala +++ b/src/main/scala/leon/utils/Library.scala @@ -17,10 +17,6 @@ case class Library(pgm: Program) { case fd: FunDef => fd } - lazy val passes = lookup("leon.lang.passes").collect { - case fd: FunDef => fd - } - lazy val guide = lookup("leon.lang.synthesis.guide") collect { case (fd: FunDef) => fd }