diff --git a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala index 705ec1905e5a8ab5c7447dc665126ba077bc7f3c..0cce88476080f2295069224eaa0eb6214dacb4c1 100644 --- a/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala +++ b/src/main/scala/inox/solvers/unrolling/QuantificationTemplates.scala @@ -593,7 +593,9 @@ trait QuantificationTemplates { self: Templates => handledMatchers.containsAll(ms.map(_.substitute(substituter, msubst))) } - if (isOpt) 0 else 3 + if (isOpt) 0 + else if (grounds(q)(bs, m.args(i))) 10 + else 3 } (bs, map, c + cost)