diff --git a/.gitignore b/.gitignore
index 85f840fd53901b688c0351348cba2504ebf24d52..f7c7dfdee9bfe9bd04725958e074c267605c52ba 100644
--- a/.gitignore
+++ b/.gitignore
@@ -21,12 +21,14 @@ target
 derivation*.dot
 
 # leon
-last.log
-*.last
-*.table
-*.log
-smt-sessions/
-leon.out/
+/last.log
+/*.last
+/*.table
+/*.log
+/smt-sessions/
+/leon.out/
+/repairs.dat
+/tmp
 
 #eclipse
 .cache
@@ -41,13 +43,13 @@ Leon.eml
 Leon.iml
 
 #scripts
-out-classes
+/out-classes
 
 #z3
 .z3-trace
 
 #travis
-travis/builds
+/travis/builds
 
 # Isabelle
 contrib
diff --git a/testcases/repair/features/focusIfCondition.scala b/testcases/repair/features/focusIfCondition.scala
new file mode 100644
index 0000000000000000000000000000000000000000..6209b40362483b327fb9199e6430a8b23cf75fd8
--- /dev/null
+++ b/testcases/repair/features/focusIfCondition.scala
@@ -0,0 +1,11 @@
+object Test {
+  def focusCond(a: BigInt) = {
+    if (a < 0) {
+      -a + 1
+    } else {
+      a
+    }
+  } ensuring {
+    _ > 0
+  }
+}
diff --git a/testcases/repair/features/focusIfElse.scala b/testcases/repair/features/focusIfElse.scala
new file mode 100644
index 0000000000000000000000000000000000000000..f45927f3db178fc72a00757e8034b18558daa546
--- /dev/null
+++ b/testcases/repair/features/focusIfElse.scala
@@ -0,0 +1,11 @@
+object Test {
+  def focusCond(a: BigInt) = {
+    if (a > 0) {
+      a
+    } else {
+      BigInt(-1)
+    }
+  } ensuring {
+    _ > 0
+  }
+}
diff --git a/testcases/repair/features/focusIfThen.scala b/testcases/repair/features/focusIfThen.scala
new file mode 100644
index 0000000000000000000000000000000000000000..211c2b9004c47436140b4e41aaa18f8dfd609ea5
--- /dev/null
+++ b/testcases/repair/features/focusIfThen.scala
@@ -0,0 +1,11 @@
+object Test {
+  def focusCond(a: BigInt) = {
+    if (a <= 0) {
+      BigInt(-1)
+    } else {
+      a
+    }
+  } ensuring {
+    _ > 0
+  }
+}
diff --git a/testcases/repair/features/focusLetBody.scala b/testcases/repair/features/focusLetBody.scala
new file mode 100644
index 0000000000000000000000000000000000000000..2a5ed017d5cd7abf53961135db0bad80a6ae0c1a
--- /dev/null
+++ b/testcases/repair/features/focusLetBody.scala
@@ -0,0 +1,8 @@
+object Test {
+  def focusCond(a: BigInt) = {
+    val tmp = -a
+    tmp
+  } ensuring {
+    _ > 0
+  }
+}
diff --git a/testcases/repair/features/focusMatch.scala b/testcases/repair/features/focusMatch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..7795a975ec8ff53a7404f1f897a1e239865f0a99
--- /dev/null
+++ b/testcases/repair/features/focusMatch.scala
@@ -0,0 +1,16 @@
+import leon.lang._
+
+object Test {
+  def focusMatch(a: BigInt, b: BigInt) = {
+    (a, b) match {
+      case (otherA, BigInt(0)) => otherA
+      case _ => a+1
+    }
+  } ensuring {
+    res => if (b == 0) {
+      res == 0
+    } else {
+      res == a+1
+    }
+  }
+}
diff --git a/testcases/repair/features/splitIf.scala b/testcases/repair/features/splitIf.scala
new file mode 100644
index 0000000000000000000000000000000000000000..18167f777117fb7686c834c324f21c5fe3e8a297
--- /dev/null
+++ b/testcases/repair/features/splitIf.scala
@@ -0,0 +1,11 @@
+object Test {
+  def focusCond(a: BigInt) = {
+    if (a <= 0) {
+      (a, BigInt(0))
+    } else {
+      (a, BigInt(0))
+    }
+  } ensuring {
+    res => res._1 == a && res._2 > 1
+  }
+}
diff --git a/testcases/repair/features/splitMatch.scala b/testcases/repair/features/splitMatch.scala
new file mode 100644
index 0000000000000000000000000000000000000000..5a6a67758d9b35cceae17b172d35690b6d985e44
--- /dev/null
+++ b/testcases/repair/features/splitMatch.scala
@@ -0,0 +1,13 @@
+import leon.lang._
+
+object Test {
+  def focusCond(a: BigInt) = {
+    a match {
+      case BigInt(1) => (BigInt(2), BigInt(0))
+      case BigInt(2) => (BigInt(2), BigInt(0))
+      case _ => (BigInt(0), BigInt(0))
+    }
+  } ensuring {
+    res => res._1 == a && res._2 > 1
+  }
+}