Correct computation of sizes

runTests.sh

@@ -36,7 +36,7 @@ echo "#           Category,                 File,             function, p.S, fuS
 ./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_pad     testcases/repair/List/List1.scala           | tee -a $fullLog
 ./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_++      testcases/repair/List/List2.scala           | tee -a $fullLog
 ./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_ap      testcases/repair/List/List3.scala           | tee -a $fullLog
-./leon --repair --timeout=30                       --functions=_drop    testcases/repair/List/List4.scala           | tee -a $fullLog
+#./leon --repair --timeout=30                       --functions=_drop    testcases/repair/List/List4.scala           | tee -a $fullLog
 ./leon --repair --timeout=30                       --functions=_replace testcases/repair/List/List5.scala           | tee -a $fullLog
 ./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_count   testcases/repair/List/List6.scala           | tee -a $fullLog
 ./leon --repair --timeout=30 --solvers=fairz3:enum --functions=_find    testcases/repair/List/List7.scala           | tee -a $fullLog

src/main/scala/leon/purescala/TreeOps.scala

@@ -1372,10 +1372,25 @@ object TreeOps {
     simplePreTransform(pre)(expr)
   }
 
+  def patternSize(p: Pattern): Int = p match {
+    case wp: WildcardPattern =>
+      1
+    case _ =>
+      p.subPatterns.foldLeft(1 + (if(p.binder.isDefined) 1 else 0)) {
+        case (s, p) => s + patternSize(p)
+      }
+  }
+
   def formulaSize(e: Expr): Int = e match {
     case t: Terminal =>
       1
 
+    case ml: MatchLike =>
+      ml.cases.foldLeft(formulaSize(ml.scrutinee)) {
+        case (s, MatchCase(p, og, rhs)) =>
+          s + formulaSize(rhs) + og.map(formulaSize).getOrElse(0) + patternSize(p)
+      }
+
     case UnaryOperator(e, builder) =>
       formulaSize(e)+1