diff --git a/runTests.sh b/runTests.sh
index d7ca90f21334d35a15a25a50cf2a3366e1a51942..e792db1f35d5769668b68cf8fbfdc2a974dfacf0 100755
--- a/runTests.sh
+++ b/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
diff --git a/src/main/scala/leon/purescala/TreeOps.scala b/src/main/scala/leon/purescala/TreeOps.scala
index 8cc5f31fa8c74f4ed7ef450ddf607f33634f9759..ebba57547887f478615193f3b1e8de6950018395 100644
--- a/src/main/scala/leon/purescala/TreeOps.scala
+++ b/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