Fixed limitations in quantifier instantiation module

src/main/scala/inox/ast/CallGraph.scala

@@ -96,7 +96,7 @@ trait CallGraph {
         val (c1, c2) = (functionComponent(a), functionComponent(b))
         if (c1.isEmpty && c2.isEmpty) a.id.uniqueName.compare(b.id.uniqueName)
         else if (c1.isEmpty) -1
-        else if (c2.isEmpty) -1
+        else if (c2.isEmpty) +1
         else componentOrdering.compare(c1, c2)
       }
     }

src/main/scala/inox/ast/SymbolOps.scala

@@ -5,6 +5,8 @@ package ast
 
 import utils._
 
+import scala.collection.mutable.{Map => MutableMap}
+
 /** Provides functions to manipulate [[Expressions.Expr]] in cases where
   * a symbol table is available (and required: see [[ExprOps]] for
   * simpler tree manipulations).
@@ -88,8 +90,8 @@ trait SymbolOps { self: TypeOps =>
     fixpoint(postMap(rec))(expr)
   }
 
-  private val typedIds: scala.collection.mutable.Map[Type, List[Identifier]] =
-    scala.collection.mutable.Map.empty.withDefaultValue(List.empty)
+  private val typedIds: MutableMap[Type, List[Identifier]] =
+    MutableMap.empty.withDefaultValue(List.empty)
 
   /** Normalizes identifiers in an expression to enable some notion of structural
     * equality between expressions on which usual equality doesn't make sense
@@ -106,64 +108,71 @@ trait SymbolOps { self: TypeOps =>
     */
   def normalizeStructure(args: Seq[ValDef], expr: Expr, onlySimple: Boolean = true):
                         (Seq[ValDef], Expr, Map[Variable, Expr]) = synchronized {
-    val vars = args.map(_.toVariable).toSet
-
-    class Normalizer extends SelfTreeTransformer {
-      var subst: Map[Variable, Expr] = Map.empty
-      var varSubst: Map[Identifier, Identifier] = Map.empty
-      var remainingIds: Map[Type, List[Identifier]] = typedIds.toMap
-
-      def getId(e: Expr): Identifier = {
-        val tpe = bestRealType(e.getType)
-        val newId = remainingIds.get(tpe) match {
-          case Some(x :: xs) =>
-            remainingIds += tpe -> xs
-            x
-          case _ =>
-            val x = FreshIdentifier("x", true)
-            typedIds(tpe) = typedIds(tpe) :+ x
-            x
-        }
-        subst += Variable(newId, tpe) -> e
-        newId
-      }
 
-      override def transform(id: Identifier, tpe: Type): (Identifier, Type) = subst.get(Variable(id, tpe)) match {
-        case Some(Variable(newId, tpe)) => (newId, tpe)
-        case Some(_) => scala.sys.error("Should never happen!")
-        case None => varSubst.get(id) match {
-          case Some(newId) => (newId, tpe)
-          case None =>
-            val newId = getId(Variable(id, tpe))
-            varSubst += id -> newId
-            (newId, tpe)
-        }
+    val subst: MutableMap[Variable, Expr] = MutableMap.empty
+    val varSubst: MutableMap[Identifier, Identifier] = MutableMap.empty
+
+    // Note: don't use clone here, we want to drop the `withDefaultValue` feature of [[typeIds]]
+    val remainingIds: MutableMap[Type, List[Identifier]] = MutableMap.empty ++ typedIds.toMap
+
+    def getId(e: Expr): Identifier = {
+      val tpe = bestRealType(e.getType)
+      val newId = remainingIds.get(tpe) match {
+        case Some(x :: xs) =>
+          remainingIds += tpe -> xs
+          x
+        case _ =>
+          val x = FreshIdentifier("x", true)
+          typedIds(tpe) = typedIds(tpe) :+ x
+          x
       }
+      subst += Variable(newId, tpe) -> e
+      newId
+    }
 
-      override def transform(e: Expr): Expr = e match {
-        case expr if (!onlySimple || isSimple(expr)) && (variablesOf(expr) & vars).isEmpty =>
-          Variable(getId(expr), expr.getType)
-        case f: Forall =>
-          val (args, body, newSubst) = normalizeStructure(f.args, f.body, onlySimple)
-          subst ++= newSubst
-          Forall(args, body)
-        case l: Lambda =>
-          val (args, body, newSubst) = normalizeStructure(l.args, l.body, onlySimple)
-          subst ++= newSubst
-          Lambda(args, body)
-        case _ => super.transform(e)
+    def transformId(id: Identifier, tpe: Type): (Identifier, Type) = subst.get(Variable(id, tpe)) match {
+      case Some(Variable(newId, tpe)) => (newId, tpe)
+      case Some(_) => scala.sys.error("Should never happen!")
+      case None => varSubst.get(id) match {
+        case Some(newId) => (newId, tpe)
+        case None =>
+          val newId = getId(Variable(id, tpe))
+          varSubst += id -> newId
+          (newId, tpe)
       }
     }
 
-    val n = new Normalizer
-    // this registers the argument images into n.subst
-    val bindings = args map n.transform
-    val normalized = n.transform(expr)
+    def rec(vars: Set[Variable], body: Expr): Expr = {
+
+      class Normalizer extends SelfTreeTransformer {
+        override def transform(id: Identifier, tpe: Type): (Identifier, Type) = transformId(id, tpe)
+
+        override def transform(e: Expr): Expr = e match {
+          case expr if (!onlySimple || isSimple(expr)) && (variablesOf(expr) & vars).isEmpty =>
+            Variable(getId(expr), expr.getType)
+          case f: Forall =>
+            val newBody = rec(vars ++ f.args.map(_.toVariable), f.body)
+            Forall(f.args.map(vd => vd.copy(id = varSubst(vd.id))), newBody)
+          case l: Lambda =>
+            val newBody = rec(vars ++ l.args.map(_.toVariable), l.body)
+            Lambda(l.args.map(vd => vd.copy(id = varSubst(vd.id))), newBody)
+          case _ => super.transform(e)
+        }
+      }
+
+      val n = new Normalizer
+
+      // this registers the argument images into subst
+      vars foreach n.transform
+      n.transform(body)
+    }
 
-    val freeVars = variablesOf(normalized) -- bindings.map(_.toVariable)
-    val bodySubst = n.subst.filter(p => freeVars(p._1))
+    val newExpr = rec(args.map(_.toVariable).toSet, expr)
+    val bindings = args.map(vd => vd.copy(id = varSubst(vd.id)))
+    val freeVars = variablesOf(newExpr) -- bindings.map(_.toVariable)
+    val bodySubst = subst.filter(p => freeVars(p._1)).toMap
 
-    (bindings, normalized, bodySubst)
+    (bindings, newExpr, bodySubst)
   }
 
   def normalizeStructure(lambda: Lambda): (Lambda, Map[Variable, Expr]) = {

src/main/scala/inox/solvers/unrolling/LambdaTemplates.scala

@@ -14,6 +14,7 @@ trait LambdaTemplates { self: Templates =>
 
   import lambdasManager._
   import datatypesManager._
+  import quantificationsManager._
 
   /** Represents a POTENTIAL application of a first-class function in the unfolding procedure
     *
@@ -83,7 +84,7 @@ trait LambdaTemplates { self: Templates =>
         clauses, blockers, applications, matchers,
         lambdas, quantifications,
         structure,
-        lambda, lambdaString
+        lambda, lambdaString, false
       )
     }
   }
@@ -177,7 +178,7 @@ trait LambdaTemplates { self: Templates =>
 
       val substituter = mkSubstituter(substMap.mapValues(_.encoded))
       val deps = dependencies.map(substituter)
-      val key = (lambda, pathVar._2, deps)
+      val key = (lambda, blockerPath(pathVar._2), deps)
 
       val sortedDeps = exprOps.variablesOf(lambda).toSeq.sortBy(_.id.uniqueName)
       val locals = sortedDeps zip deps
@@ -190,6 +191,10 @@ trait LambdaTemplates { self: Templates =>
     }
 
     override def hashCode: Int = key.hashCode
+
+    def subsumes(that: LambdaStructure): Boolean = {
+      key._1 == that.key._1 && key._3 == that.key._3 && key._2.subsetOf(that.key._2)
+    }
   }
 
   class LambdaTemplate private (
@@ -208,7 +213,8 @@ trait LambdaTemplates { self: Templates =>
     val quantifications: Seq[QuantificationTemplate],
     val structure: LambdaStructure,
     val lambda: Lambda,
-    private[unrolling] val stringRepr: () => String) extends Template {
+    private[unrolling] val stringRepr: () => String,
+    private val isConcrete: Boolean) extends Template {
 
     val args = arguments.map(_._2)
     val tpe = bestRealType(ids._1.getType).asInstanceOf[FunctionType]
@@ -224,10 +230,11 @@ trait LambdaTemplates { self: Templates =>
       lambdas.map(_.substitute(substituter, msubst)),
       quantifications.map(_.substitute(substituter, msubst)),
       structure.substitute(substituter, msubst),
-      lambda, stringRepr)
+      lambda, stringRepr, isConcrete)
 
     /** This must be called right before returning the clauses in [[structure.instantiation]]! */
     def concretize(idT: Encoded): LambdaTemplate = {
+      assert(!isConcrete, "Can't concretize concrete lambda template")
       val substituter = mkSubstituter(Map(ids._2 -> idT) ++ (closures.map(_._2) zip structure.locals.map(_._2)))
       new LambdaTemplate(
         ids._1 -> idT,
@@ -238,7 +245,7 @@ trait LambdaTemplates { self: Templates =>
         matchers.map { case (b, ms) => b -> ms.map(_.substitute(substituter, Map.empty)) },
         lambdas.map(_.substitute(substituter, Map.empty)),
         quantifications.map(_.substitute(substituter, Map.empty)),
-        structure, lambda, stringRepr)
+        structure, lambda, stringRepr, true)
     }
 
     override def instantiate(blocker: Encoded, args: Seq[Arg]): Clauses = {
@@ -262,6 +269,11 @@ trait LambdaTemplates { self: Templates =>
     mkSubstituter(Map(vT -> caller) ++ (asT zip args))(app)
   }
 
+  def mkFlatApp(caller: Encoded, tpe: FunctionType, args: Seq[Encoded]): Encoded = tpe.to match {
+    case ft: FunctionType => mkFlatApp(mkApp(caller, tpe, args.take(tpe.from.size)), ft, args.drop(tpe.from.size))
+    case _ => mkApp(caller, tpe, args)
+  }
+
   def registerFunction(b: Encoded, tpe: FunctionType, f: Encoded): Clauses = {
     val ft = bestRealType(tpe).asInstanceOf[FunctionType]
     freeFunctions += ft -> (freeFunctions(ft) + (b -> f))
@@ -296,48 +308,50 @@ trait LambdaTemplates { self: Templates =>
   }
 
   def instantiateLambda(template: LambdaTemplate): (Encoded, Clauses) = {
-    byType(template.tpe).get(template.structure) match {
-      case Some(template) =>
-        (template.ids._2, Seq.empty)
-
-      case None =>
-        val idT = encodeSymbol(template.ids._1)
-        val newTemplate = template.concretize(idT)
+    byType(template.tpe).get(template.structure).map {
+      t => (t.ids._2, Seq.empty)
+    }.orElse {
+      byType(template.tpe).collectFirst {
+        case (s, t) if s subsumes template.structure => (t.ids._2, Seq.empty)
+      }
+    }.getOrElse {
+      val idT = encodeSymbol(template.ids._1)
+      val newTemplate = template.concretize(idT)
 
-        val orderingClauses = newTemplate.structure.locals.flatMap {
-          case (v, dep) => registerClosure(newTemplate.start, idT -> newTemplate.tpe, dep -> v.tpe)
-        }
+      val orderingClauses = newTemplate.structure.locals.flatMap {
+        case (v, dep) => registerClosure(newTemplate.start, idT -> newTemplate.tpe, dep -> v.tpe)
+      }
 
-        val extClauses = for ((oldB, freeF) <- freeBlockers(newTemplate.tpe) if canEqual(freeF, idT)) yield {
-          val nextB  = encodeSymbol(Variable(FreshIdentifier("b_or", true), BooleanType))
-          val ext = mkOr(mkAnd(newTemplate.start, mkEquals(idT, freeF)), nextB)
-          mkEquals(oldB, ext)
-        }
+      val extClauses = for ((oldB, freeF) <- freeBlockers(newTemplate.tpe) if canEqual(freeF, idT)) yield {
+        val nextB  = encodeSymbol(Variable(FreshIdentifier("b_or", true), BooleanType))
+        val ext = mkOr(mkAnd(newTemplate.start, mkEquals(idT, freeF)), nextB)
+        mkEquals(oldB, ext)
+      }
 
-        val arglessEqClauses = if (newTemplate.tpe.from.nonEmpty) Seq.empty[Encoded] else {
-          for ((b,f) <- freeFunctions(newTemplate.tpe) if canEqual(idT, f)) yield {
-            val (tmplApp, fApp) = (mkApp(idT, newTemplate.tpe, Seq.empty), mkApp(f, newTemplate.tpe, Seq.empty))
-            mkImplies(mkAnd(b, newTemplate.start, mkEquals(tmplApp, fApp)), mkEquals(idT, f))
-          }
+      val arglessEqClauses = if (newTemplate.tpe.from.nonEmpty) Seq.empty[Encoded] else {
+        for ((b,f) <- freeFunctions(newTemplate.tpe) if canEqual(idT, f)) yield {
+          val (tmplApp, fApp) = (mkApp(idT, newTemplate.tpe, Seq.empty), mkApp(f, newTemplate.tpe, Seq.empty))
+          mkImplies(mkAnd(b, newTemplate.start, mkEquals(tmplApp, fApp)), mkEquals(idT, f))
         }
+      }
 
-        // make sure we have sound equality between the new lambda and previously defined ones
-        val clauses = newTemplate.structure.instantiation ++
-          equalityClauses(newTemplate) ++
-          orderingClauses ++
-          extClauses ++
-          arglessEqClauses
+      // make sure we have sound equality between the new lambda and previously defined ones
+      val clauses = newTemplate.structure.instantiation ++
+        equalityClauses(newTemplate) ++
+        orderingClauses ++
+        extClauses ++
+        arglessEqClauses
 
-        byID += idT -> newTemplate
-        byType += newTemplate.tpe -> (byType(newTemplate.tpe) + (newTemplate.structure -> newTemplate))
+      byID += idT -> newTemplate
+      byType += newTemplate.tpe -> (byType(newTemplate.tpe) + (newTemplate.structure -> newTemplate))
 
-        val gen = nextGeneration(currentGeneration)
-        for (app @ (_, App(caller, _, args, _)) <- applications(newTemplate.tpe)) {
-          val cond = mkAnd(newTemplate.start, mkEquals(idT, caller))
-          registerAppBlocker(gen, app, Left(newTemplate), cond, args)
-        }
+      val gen = nextGeneration(currentGeneration)
+      for (app @ (_, App(caller, _, args, _)) <- applications(newTemplate.tpe)) {
+        val cond = mkAnd(newTemplate.start, mkEquals(idT, caller))
+        registerAppBlocker(gen, app, Left(newTemplate), cond, args)
+      }
 
-        (idT, clauses)
+      (idT, clauses)
     }
   }
 

src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala

@@ -81,8 +81,8 @@ trait QuantificationTemplates { self: Templates =>
     *
     * Instantiations of unknown polarity quantification with body {{{p}}} follows the schema:
     * {{{
-    *    b ==> (q == (q2 && inst)
-    *    b ==> (inst == (guard ==> p))
+    *    q == (q2 && inst)
+    *    inst == (guard ==> p)
     * }}}
     * It is useful to keep the two clauses separate so that satisfying assignments can be
     * constructed where only certain `inst` variables are falsified. This is used to enable
@@ -103,7 +103,7 @@ trait QuantificationTemplates { self: Templates =>
     val matchers: Matchers,
     val lambdas: Seq[LambdaTemplate],
     val quantifications: Seq[QuantificationTemplate],
-    val key: (Seq[ValDef], Expr, Seq[Encoded]),
+    val key: (Encoded, Seq[ValDef], Expr, Seq[Encoded]),
     val body: Expr,
     stringRepr: () => String) {
 
@@ -122,7 +122,7 @@ trait QuantificationTemplates { self: Templates =>
         matchers.map { case (b, ms) => substituter(b) -> ms.map(_.substitute(substituter, msubst)) },
         lambdas.map(_.substitute(substituter, msubst)),
         quantifications.map(_.substitute(substituter, msubst)),
-        (key._1, key._2, key._3.map(substituter)),
+        (substituter(key._1), key._2, key._3, key._4.map(substituter)),
         body, stringRepr)
 
     private lazy val str : String = stringRepr()
@@ -197,7 +197,8 @@ trait QuantificationTemplates { self: Templates =>
           extraGuarded merge guardedExprs, extraEqs ++ equations,
           lambdas, quantifications, substMap = substMap ++ extraSubst)
 
-      val key = templateKey(proposition.args, proposition.body, substMap)
+      val tk = templateKey(proposition.args, proposition.body, substMap)
+      val key = (pathVar._2, tk._1, tk._2, tk._3)
 
       (optVar, new QuantificationTemplate(
         pathVar, polarity, quantifiers, condVars, exprVars, condTree, clauses,
@@ -218,8 +219,8 @@ trait QuantificationTemplates { self: Templates =>
     val handledSubsts   = new IncrementalMap[Quantification, Set[(Set[Encoded], Map[Encoded,Arg])]]
     val ignoredGrounds  = new IncrementalMap[Int, Set[Quantification]]
 
-    val lambdaAxioms    = new IncrementalSet[(LambdaStructure, Seq[(Variable, Encoded)])]
-    val templates       = new IncrementalMap[(Seq[ValDef], Expr, Seq[Encoded]), Map[Encoded, Encoded]]
+    val lambdaAxioms    = new IncrementalSet[LambdaStructure]
+    val templates       = new IncrementalMap[(Encoded, Seq[ValDef], Expr, Seq[Encoded]), (QuantificationTemplate, Map[Encoded, Encoded])]
 
     val incrementals: Seq[IncrementalState] = Seq(quantifications, lambdaAxioms, templates,
       ignoredMatchers, handledMatchers, ignoredSubsts, handledSubsts, ignoredGrounds)
@@ -338,14 +339,14 @@ trait QuantificationTemplates { self: Templates =>
   @inline
   private def matcherKey(m: Matcher): MatcherKey = matcherKey(m.key)
 
-  private def correspond(k1: MatcherKey, k2: MatcherKey): Option[Boolean] = (k1, k2) match {
+  protected def correspond(k1: MatcherKey, k2: MatcherKey): Option[Boolean] = (k1, k2) match {
     case (`k2`, _) => Some(true)
     case (tp1: TypedKey, tp2: TypedKey) if tp1.tpe == tp2.tpe => Some(false)
     case _ => None
   }
 
   @inline
-  private def correspond(m1: Matcher, m2: Matcher): Option[Boolean] =
+  protected def correspond(m1: Matcher, m2: Matcher): Option[Boolean] =
     correspond(matcherKey(m1), matcherKey(m2))
 
   private trait BlockedSet[Element] extends Iterable[(Set[Encoded], Element)] with IncrementalState {
@@ -691,6 +692,14 @@ trait QuantificationTemplates { self: Templates =>
         }
       }
 
+      for (tmpl <- lambdas.map(t => byID(substituter(t.ids._2)))) {
+        instantiation ++= instantiateAxiom(tmpl)
+      }
+
+      for ((_, apps) <- applications; App(caller, _, _, _) <- apps; tmpl <- byID.get(substituter(caller))) {
+        instantiation ++= instantiateAxiom(tmpl)
+      }
+
       instantiation.toSeq
     }
 
@@ -821,63 +830,54 @@ trait QuantificationTemplates { self: Templates =>
   }
 
   def instantiateAxiom(template: LambdaTemplate): Clauses = {
-    val quantifiers = template.arguments.map { p => p._1.freshen -> encodeSymbol(p._1) }
-
-    val app = mkApplication(template.ids._1, quantifiers.map(_._1))
-    val appT = mkEncoder(quantifiers.toMap + template.ids)(app)
-    val selfMatcher = Matcher(Left(template.ids._2 -> template.tpe), quantifiers.map(p => Left(p._2)), appT)
-
-    val blocker = Variable(FreshIdentifier("blocker", true), BooleanType)
-    val blockerT = encodeSymbol(blocker)
-
-    val guard = Variable(FreshIdentifier("guard", true), BooleanType)
-    val guardT = encodeSymbol(guard)
-
-    val enablingClause = mkEquals(mkAnd(guardT, template.start), blockerT)
-
-    /* Compute Axiom's unique key to avoid redudant instantiations */
+    if (lambdaAxioms(template.structure) || lambdaAxioms.exists(s => s.subsumes(template.structure))) {
+      Seq.empty
+    } else {
+      lambdaAxioms += template.structure
+      val quantifiers = template.arguments
+      val app = mkFlatApp(template.ids._2, template.tpe, quantifiers.map(_._2))
+      val matcher = Matcher(Left(template.ids._2 -> template.tpe), quantifiers.map(p => Left(p._2)), app)
+
+      val guard = encodeSymbol(Variable(FreshIdentifier("guard", true), BooleanType))
+      val substituter = mkSubstituter(Map(template.start -> guard))
+
+      val body: Expr = {
+        def rec(caller: Expr, body: Expr): Expr = body match {
+          case Lambda(args, body) => rec(Application(caller, args.map(_.toVariable)), body)
+          case _ => Equals(caller, body)
+        }
+        rec(template.ids._1, template.structure.lambda)
+      }
 
-    def flattenLambda(e: Expr): (Seq[ValDef], Expr) = e match {
-      case Lambda(args, body) =>
-        val (recArgs, recBody) = flattenLambda(body)
-        (args ++ recArgs, recBody)
-      case _ => (Seq.empty, e)
+      val tk = QuantificationTemplate.templateKey(
+        quantifiers.map(_._1.toVal),
+        body,
+        template.structure.locals.toMap + template.ids
+      )
+      val key = (template.pathVar._2, tk._1, tk._2, tk._3)
+
+      instantiateQuantification(new QuantificationTemplate(
+        template.pathVar,
+        Positive(guard),
+        quantifiers,
+        template.condVars,
+        template.exprVars,
+        template.condTree,
+        template.clauses map substituter,
+        template.blockers.map { case (b, fis) => substituter(b) -> fis.map(_.substitute(substituter, Map.empty)) },
+        template.applications.map { case (b, fas) => substituter(b) -> fas.map(_.substitute(substituter, Map.empty)) },
+        template.matchers.map { case (b, ms) =>
+          substituter(b) -> ms.map(_.substitute(substituter, Map.empty))
+        } merge Map(guard -> Set(matcher)),
+        template.lambdas.map(_.substitute(substituter, Map.empty)),
+        template.quantifications.map(_.substitute(substituter, Map.empty)),
+        key, body, template.stringRepr))._2 // mapping is guaranteed empty!!
     }
-
-    val (structArgs, structBody) = flattenLambda(template.structure.lambda)
-    assert(quantifiers.size == structArgs.size, "Expecting lambda templates to contain flattened lamdbas")
-
-    val lambdaBody = exprOps.replaceFromSymbols((structArgs zip quantifiers.map(_._1)).toMap, structBody)
-    val quantBody = Equals(app, lambdaBody)
-
-    val substMap = template.structure.locals.toMap + template.ids
-
-    val key = QuantificationTemplate.templateKey(quantifiers.map(_._1.toVal), quantBody, substMap)
-
-    val substituter = mkSubstituter((template.args zip quantifiers.map(_._2)).toMap + (template.start -> blockerT))
-    val msubst = Map.empty[Encoded, Matcher]
-
-    instantiateQuantification(new QuantificationTemplate(
-      template.pathVar,
-      Positive(guardT),
-      quantifiers,
-      template.condVars + (blocker -> blockerT),
-      template.exprVars,
-      template.condTree,
-      (template.clauses map substituter) :+ enablingClause,
-      template.blockers.map { case (b, fis) => substituter(b) -> fis.map(_.substitute(substituter, msubst)) },
-      template.applications.map { case (b, fas) => substituter(b) -> fas.map(_.substitute(substituter, msubst)) },
-      template.matchers.map { case (b, ms) =>
-        substituter(b) -> ms.map(_.substitute(substituter, msubst))
-      } merge Map(blockerT -> Set(selfMatcher)),
-      template.lambdas.map(_.substitute(substituter, msubst)),
-      template.quantifications.map(_.substitute(substituter, msubst)),
-      key, quantBody, template.stringRepr))._2 // mapping is guaranteed empty!!
   }
 
   def instantiateQuantification(template: QuantificationTemplate): (Map[Encoded, Encoded], Clauses) = {
     templates.get(template.key) match {
-      case Some(map) =>
+      case Some((_, map)) =>
         (map, Seq.empty)
 
       case None =>
@@ -908,9 +908,8 @@ trait QuantificationTemplates { self: Templates =>
             clauses ++= substClauses
 
             // this will call `instantiateMatcher` on all matchers in `template.matchers`
-            val instClauses = Template.instantiate(template.clauses,
+            clauses ++= Template.instantiate(template.clauses,
               template.blockers, template.applications, template.matchers, substMap)
-            clauses ++= instClauses
 
             Map(insts._2 -> instT)
 
@@ -931,7 +930,8 @@ trait QuantificationTemplates { self: Templates =>
               clauses ++= quantification.instantiate(bs, m)
             }
 
-            val freshSubst = mkSubstituter(template.quantifiers.map(p => p._2 -> encodeSymbol(p._1)).toMap)
+            val freshQuantifiers = template.quantifiers.map(p => encodeSymbol(p._1))
+            val freshSubst = mkSubstituter((template.quantifiers.map(_._2) zip freshQuantifiers).toMap)
             for ((b,ms) <- template.matchers; m <- ms) {
               clauses ++= instantiateMatcher(Set.empty[Encoded], m, false)
               // it is very rare that such instantiations are actually required, so we defer them
@@ -943,7 +943,7 @@ trait QuantificationTemplates { self: Templates =>
             Map(qs._2 -> qT)
         }
 
-        templates += template.key -> mapping
+        templates += template.key -> ((template, mapping))
         (mapping, clauses.toSeq)
     }
   }