• English only

# Differences

This shows you the differences between two versions of the page.

leon-repair [2015/02/09 14:58]
ekneuss
leon-repair [2015/02/10 17:14] (current)
ekneuss
Line 47: Line 47:

The version of Leon used to run all these benchmarks is [[https://​github.com/​colder/​leon/​tree/​ddd08e3aac4cc52c51dc60b59867eaea38f3cbf5| publicly available on Github]]. The version of Leon used to run all these benchmarks is [[https://​github.com/​colder/​leon/​tree/​ddd08e3aac4cc52c51dc60b59867eaea38f3cbf5| publicly available on Github]].
+
+
+The following output is produced by the tool:
+
+ %%% Compiler1.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ Plus(desugar(lhs),​ desugar(rhs))
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ @induct
+ def desugar(e : Trees.Expr):​ SimpleE = {
+   e match {
+     case Trees.Plus(lhs,​ rhs) =>
+       Plus(desugar(lhs),​ desugar(rhs))
+     case Trees.Minus(lhs,​ rhs) =>
+       Plus(desugar(lhs),​ Neg(desugar(rhs)))
+     case Trees.LessThan(lhs,​ rhs) =>
+       LessThan(desugar(lhs),​ desugar(rhs))
+     case Trees.And(lhs,​ rhs) =>
+       Ite(desugar(lhs),​ desugar(rhs),​ Literal(0))
+     case Trees.Or(lhs,​ rhs) =>
+       Ite(desugar(lhs),​ Literal(1), desugar(rhs))
+     case Trees.Not(e) =>
+       Ite(desugar(e),​ Literal(0), Literal(1))
+     case Trees.Eq(lhs,​ rhs) =>
+       Eq(desugar(lhs),​ desugar(rhs))
+     case Trees.Ite(cond,​ thn, els) =>
+       Ite(desugar(cond),​ desugar(thn),​ desugar(els))
+     case Trees.IntLiteral(v) =>
+       Literal(v)
+     case Trees.BoolLiteral(b) =>
+       Literal(b2i(b))
+   }
+ } ensuring {
+   (res : SimpleE) => (e, res) passes {
+     case Trees.Plus(Trees.IntLiteral(i),​ Trees.Minus(Trees.IntLiteral(j),​ Trees.IntLiteral(42))) =>
+       Plus(Literal(i),​ Plus(Literal(j),​ Neg(Literal(42))))
+   } && sem(res) == semUntyped(e)
+ }
+
+ %%% Compiler2.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ Plus(None[SimpleE]().getOrElse(desugar(lhs)),​ Neg(desugar(rhs)))
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ @induct
+ def desugar(e : Trees.Expr):​ SimpleE = {
+   e match {
+     case Trees.Plus(lhs,​ rhs) =>
+       Plus(desugar(lhs),​ desugar(rhs))
+     case Trees.Minus(lhs,​ rhs) =>
+       Plus(None[SimpleE]().getOrElse(desugar(lhs)),​ Neg(desugar(rhs)))
+     case Trees.LessThan(lhs,​ rhs) =>
+       LessThan(desugar(lhs),​ desugar(rhs))
+     case Trees.And(lhs,​ rhs) =>
+       Ite(desugar(lhs),​ desugar(rhs),​ Literal(0))
+     case Trees.Or(lhs,​ rhs) =>
+       Ite(desugar(lhs),​ Literal(1), desugar(rhs))
+     case Trees.Not(e) =>
+       Ite(desugar(e),​ Literal(0), Literal(1))
+     case Trees.Eq(lhs,​ rhs) =>
+       Eq(desugar(lhs),​ desugar(rhs))
+     case Trees.Ite(cond,​ thn, els) =>
+       Ite(desugar(cond),​ desugar(thn),​ desugar(els))
+     case Trees.IntLiteral(v) =>
+       Literal(v)
+     case Trees.BoolLiteral(b) =>
+       Literal(b2i(b))
+   }
+ } ensuring {
+   (res : SimpleE) => sem(res) == semUntyped(e) && (e, res) passes {
+     case Trees.Minus(Trees.IntLiteral(42),​ Trees.IntLiteral(i)) =>
+       Plus(Literal(42),​ Neg(Literal(i)))
+   }
+ }
+
+ %%% Compiler3.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ Ite(desugar(cond),​ desugar(thn),​ desugar(els))
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ @induct
+ def desugar(e : Trees.Expr):​ SimpleE = {
+   e match {
+     case Trees.Plus(lhs,​ rhs) =>
+       Plus(desugar(lhs),​ desugar(rhs))
+     case Trees.Minus(lhs,​ rhs) =>
+       Plus(desugar(lhs),​ Neg(desugar(rhs)))
+     case Trees.LessThan(lhs,​ rhs) =>
+       LessThan(desugar(lhs),​ desugar(rhs))
+     case Trees.And(lhs,​ rhs) =>
+       Ite(desugar(lhs),​ desugar(rhs),​ Literal(0))
+     case Trees.Or(lhs,​ rhs) =>
+       Ite(desugar(lhs),​ Literal(1), desugar(rhs))
+     case Trees.Not(e) =>
+       Ite(desugar(e),​ Literal(0), Literal(1))
+     case Trees.Eq(lhs,​ rhs) =>
+       Eq(desugar(lhs),​ desugar(rhs))
+     case Trees.Ite(cond,​ thn, els) =>
+       Ite(desugar(cond),​ desugar(thn),​ desugar(els))
+     case Trees.IntLiteral(v) =>
+       Literal(v)
+     case Trees.BoolLiteral(b) =>
+       Literal(b2i(b))
+   }
+ } ensuring {
+   (res : SimpleE) => sem(res) == semUntyped(e)
+ }
+
+ %%% Compiler4.scala
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ Ite(desugar(e),​ Literal(0), Literal(1))
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ @induct
+ def desugar(e : Trees.Expr):​ SimpleE = {
+   e match {
+     case Trees.Plus(lhs,​ rhs) =>
+       Plus(desugar(lhs),​ desugar(rhs))
+     case Trees.Minus(lhs,​ rhs) =>
+       Plus(desugar(lhs),​ Neg(desugar(rhs)))
+     case Trees.LessThan(lhs,​ rhs) =>
+       LessThan(desugar(lhs),​ desugar(rhs))
+     case Trees.And(lhs,​ rhs) =>
+       Ite(desugar(lhs),​ desugar(rhs),​ Literal(0))
+     case Trees.Or(lhs,​ rhs) =>
+       Ite(desugar(lhs),​ Literal(1), desugar(rhs))
+     case Trees.Not(e) =>
+       Ite(desugar(e),​ Literal(0), Literal(1))
+     case Trees.Eq(lhs,​ rhs) =>
+       Eq(desugar(lhs),​ desugar(rhs))
+     case Trees.Ite(cond,​ thn, els) =>
+       Ite(desugar(cond),​ desugar(thn),​ desugar(els))
+     case Trees.IntLiteral(v) =>
+       Literal(v)
+     case Trees.BoolLiteral(b) =>
+       Literal(b2i(b))
+   }
+ } ensuring {
+   (res : SimpleE) => sem(res) == semUntyped(e)
+ }
+
+ %%% Compiler5.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ e match {
+   case Plus(lhs, rhs) =>
+     Plus(desugar(lhs),​ desugar(rhs))
+   case Minus(lhs, rhs) =>
+     Plus(desugar(lhs),​ Neg(desugar(rhs)))
+   case LessThan(lhs,​ rhs) =>
+     LessThan(desugar(lhs),​ desugar(rhs))
+   case And(lhs, rhs) =>
+     Ite(desugar(lhs),​ desugar(rhs),​ Literal(0))
+   case Or(lhs, rhs) =>
+     Ite(desugar(lhs),​ Literal(1), desugar(rhs))
+   case Not(e) =>
+     Ite(desugar(e),​ Literal(0), Literal(1))
+   case Eq(lhs, rhs) =>
+     Eq(desugar(lhs),​ desugar(rhs))
+   case Ite(cond, thn, els) =>
+     Ite(desugar(cond),​ desugar(thn),​ desugar(els))
+   case IntLiteral(v) =>
+     Literal(v)
+   case BoolLiteral(b) =>
+     Literal(b2i(b))
+ }
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ @induct
+ def desugar(e : Trees.Expr):​ SimpleE = {
+   e match {
+     case Trees.Plus(lhs,​ rhs) =>
+       Plus(desugar(lhs),​ desugar(rhs))
+     case Trees.Minus(lhs,​ rhs) =>
+       Plus(desugar(lhs),​ Neg(desugar(rhs)))
+     case Trees.LessThan(lhs,​ rhs) =>
+       LessThan(desugar(lhs),​ desugar(rhs))
+     case Trees.And(lhs,​ rhs) =>
+       Ite(desugar(lhs),​ desugar(rhs),​ Literal(0))
+     case Trees.Or(lhs,​ rhs) =>
+       Ite(desugar(lhs),​ Literal(1), desugar(rhs))
+     case Trees.Not(e) =>
+       Ite(desugar(e),​ Literal(0), Literal(1))
+     case Trees.Eq(lhs,​ rhs) =>
+       Eq(desugar(lhs),​ desugar(rhs))
+     case Trees.Ite(cond,​ thn, els) =>
+       Ite(desugar(cond),​ desugar(thn),​ desugar(els))
+     case Trees.IntLiteral(v) =>
+       Literal(v)
+     case Trees.BoolLiteral(b) =>
+       Literal(b2i(b))
+   }
+ } ensuring {
+   (res : SimpleE) => sem(res) == semUntyped(e)
+ }
+
+ %%% Compiler6.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ IntLiteral(a + b)
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ @induct
+ def simplify(e : Trees.Expr):​ Trees.Expr = {
+   e match {
+     case Trees.And(Trees.BoolLiteral(false),​ _) =>
+       Trees.BoolLiteral(false)
+     case Trees.Or(Trees.BoolLiteral(true),​ _) =>
+       Trees.BoolLiteral(true)
+     case Trees.Plus(Trees.IntLiteral(a),​ Trees.IntLiteral(b)) =>
+       Trees.IntLiteral(a + b)
+     case Trees.Not(Trees.Not(Trees.Not(a))) =>
+       Trees.Not(a)
+     case e =>
+       e
+   }
+ } ensuring {
+   (res : Trees.Expr) => eval(res) == eval(e)
+ }
+
+ %%% Compiler7.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ BoolLiteral(true)
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ @induct
+ def simplify(e : Trees.Expr):​ Trees.Expr = {
+   e match {
+     case Trees.And(Trees.BoolLiteral(false),​ _) =>
+       Trees.BoolLiteral(false)
+     case Trees.Or(Trees.BoolLiteral(true),​ _) =>
+       Trees.BoolLiteral(true)
+     case Trees.Plus(Trees.IntLiteral(a),​ Trees.IntLiteral(b)) =>
+       Trees.IntLiteral(a + b)
+     case Trees.Not(Trees.Not(Trees.Not(a))) =>
+       Trees.Not(a)
+     case e =>
+       e
+   }
+ } ensuring {
+   (res : Trees.Expr) => eval(res) == eval(e) && (e, res) passes {
+     case Trees.Or(Trees.BoolLiteral(true),​ e) =>
+       Trees.BoolLiteral(true)
+   }
+ }
+
+ %%% Heap1.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ v2 >= v1
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def merge(h1 : Heap, h2 : Heap): Heap = {
+   require(hasLeftistProperty(h1) && hasLeftistProperty(h2) && hasHeapProperty(h1) && hasHeapProperty(h2))
+   (h1, h2) match {
+     case (Leaf(), _) =>
+       h2
+     case (_, Leaf()) =>
+       h1
+     case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+       if (v2 >= v1) {
+         makeN(v2, l2, merge(h1, r2))
+       } else {
+         makeN(v1, l1, merge(r1, h2))
+       }
+   }
+ } ensuring {
+   (res : Heap) => hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(h1) + heapSize(h2) == heapSize(res) && h1.content() ++ h2.content() == res.content()
+ }
+
+ %%% Heap2.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ h1
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def merge(h1 : Heap, h2 : Heap): Heap = {
+   require(hasLeftistProperty(h1) && hasLeftistProperty(h2) && hasHeapProperty(h1) && hasHeapProperty(h2))
+   (h1, h2) match {
+     case (Leaf(), _) =>
+       h2
+     case (_, Leaf()) =>
+       h1
+     case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+       if (v1 >= v2) {
+         makeN(v1, l1, merge(r1, h2))
+       } else {
+         makeN(v2, l2, merge(h1, r2))
+       }
+   }
+ } ensuring {
+   (res : Heap) => hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(h1) + heapSize(h2) == heapSize(res) && h1.content() ++ h2.content() == res.content()
+ }
+
+ %%% Heap3.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ v2 <= v1
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def merge(h1 : Heap, h2 : Heap): Heap = {
+   require(hasLeftistProperty(h1) && hasLeftistProperty(h2) && hasHeapProperty(h1) && hasHeapProperty(h2))
+   (h1, h2) match {
+     case (Leaf(), _) =>
+       h2
+     case (_, Leaf()) =>
+       h1
+     case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+       if (v2 <= v1) {
+         makeN(v1, l1, merge(r1, h2))
+       } else {
+         makeN(v2, l2, merge(h1, r2))
+       }
+   }
+ } ensuring {
+   (res : Heap) => hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(h1) + heapSize(h2) == heapSize(res) && h1.content() ++ h2.content() == res.content()
+ }
+
+ %%% Heap4.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ makeN(v2, l2, merge(h1, r2))
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def merge(h1 : Heap, h2 : Heap): Heap = {
+   require(hasLeftistProperty(h1) && hasLeftistProperty(h2) && hasHeapProperty(h1) && hasHeapProperty(h2))
+   (h1, h2) match {
+     case (Leaf(), _) =>
+       h2
+     case (_, Leaf()) =>
+       h1
+     case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+       if (v1 >= v2) {
+         makeN(v1, l1, merge(r1, h2))
+       } else {
+         makeN(v2, l2, merge(h1, r2))
+       }
+   }
+ } ensuring {
+   (res : Heap) => hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(h1) + heapSize(h2) == heapSize(res) && h1.content() ++ h2.content() == res.content()
+ }
+
+ %%% Heap5.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ v1 + v2 > v2 + v2
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def merge(h1 : Heap, h2 : Heap): Heap = {
+   require(hasLeftistProperty(h1) && hasLeftistProperty(h2) && hasHeapProperty(h1) && hasHeapProperty(h2))
+   (h1, h2) match {
+     case (Leaf(), _) =>
+       h2
+     case (_, Leaf()) =>
+       h1
+     case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+       if (v1 + v2 > v2 + v2) {
+         makeN(v1, l1, merge(r1, h2))
+       } else {
+         makeN(v2, l2, merge(h1, r2))
+       }
+   }
+ } ensuring {
+   (res : Heap) => hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(h1) + heapSize(h2) == heapSize(res) && h1.content() ++ h2.content() == res.content()
+ }
+
+ %%% Heap6.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ merge(Node(element,​ Leaf(), Leaf()), heap)
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def insert(element : Int, heap : Heap): Heap = {
+   require(hasLeftistProperty(heap) && hasHeapProperty(heap))
+   merge(Node(element,​ Leaf(), Leaf()), heap)
+ } ensuring {
+   (res : Heap) => hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(res) == heapSize(heap) + 1 && res.content() == heap.content() ++ Set[Int](element)
+ }
+
+ %%% Heap7.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ left.rank() >= right.rank()
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def makeN(value : Int, left : Heap, right : Heap): Heap = {
+   require(hasLeftistProperty(left) && hasLeftistProperty(right))
+   if (left.rank() >= right.rank()) {
+     Node(value, left, right)
+   } else {
+     Node(value, right, left)
+   }
+ } ensuring {
+   (res : Heap) => hasLeftistProperty(res)
+ }
+
+ Solution is not trusted!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ (h1, h2) match {
+   case (Leaf(), _) =>
+     h2
+   case (_, Leaf()) =>
+     h1
+   case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+     if (v1 >= v2) {
+       makeN(v1, l1, merge(r1, h2))
+     } else {
+       makeN(v2, merge(h1, r2), l2)
+     }
+ }
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def merge(h1 : Heap, h2 : Heap): Heap = {
+   require(hasLeftistProperty(h1) && hasLeftistProperty(h2) && hasHeapProperty(h1) && hasHeapProperty(h2))
+   (h1, h2) match {
+     case (Leaf(), _) =>
+       h2
+     case (_, Leaf()) =>
+       h1
+     case (Node(v1, l1, r1), Node(v2, l2, r2)) =>
+       if (v1 >= v2) {
+         makeN(v1, l1, merge(r1, h2))
+       } else {
+         makeN(v2, merge(h1, r2), l2)
+       }
+   }
+ } ensuring {
+   (res : Heap) => hasLeftistProperty(res) && hasHeapProperty(res) && heapSize(h1) + heapSize(h2) == heapSize(res) && h1.content() ++ h2.content() == res.content()
+ }
+
+ %%% PropLogic1.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ nnf(Not(e))
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def nnf(formula : Formula): Formula = {
+   formula match {
+     case Not(And(lhs,​ rhs)) =>
+       Or(nnf(Not(lhs)),​ nnf(Not(rhs)))
+     case Not(Or(lhs, rhs)) =>
+       And(nnf(Not(lhs)),​ nnf(Not(rhs)))
+     case Not(Const(v)) =>
+       Const(!v)
+     case Not(Not(e)) =>
+       nnf(Not(e))
+     case And(lhs, rhs) =>
+       And(nnf(lhs),​ nnf(rhs))
+     case Or(lhs, rhs) =>
+       Or(nnf(lhs),​ nnf(rhs))
+     case other =>
+       other
+   }
+ } ensuring {
+   (res : Formula) => isNNF(res) && (formula, res) passes {
+     case Not(Not(Not(Const(a)))) =>
+       Const(!a)
+   }
+ }
+
+ %%% PropLogic2.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ other match {
+   case Const(v) =>
+     Literal(1)
+   case Literal(id) =>
+     Const(false)
+   case Not(f) =>
+     nnf(f)
+ }
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def nnf(formula : Formula): Formula = {
+   formula match {
+     case Not(And(lhs,​ rhs)) =>
+       Or(nnf(Not(lhs)),​ nnf(Not(rhs)))
+     case Not(Or(lhs, rhs)) =>
+       And(nnf(Not(lhs)),​ nnf(Not(rhs)))
+     case Not(Const(v)) =>
+       Const(!v)
+     case And(lhs, rhs) =>
+       And(nnf(lhs),​ nnf(rhs))
+     case Or(lhs, rhs) =>
+       Or(nnf(lhs),​ nnf(rhs))
+     case other =>
+       other match {
+         case Const(v) =>
+           Literal(1)
+         case Literal(id) =>
+           Const(false)
+         case Not(f) =>
+           nnf(f)
+       }
+   }
+ } ensuring {
+   (res : Formula) => isNNF(res) && (formula, res) passes {
+     case Not(Not(Not(Const(a)))) =>
+       Const(!a)
+   }
+ }
+
+ %%% PropLogic3.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ Const(false == v)
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def nnf(formula : Formula): Formula = {
+   formula match {
+     case Not(And(lhs,​ rhs)) =>
+       Or(nnf(Not(lhs)),​ nnf(Not(rhs)))
+     case Not(Or(lhs, rhs)) =>
+       And(nnf(Not(lhs)),​ nnf(Not(rhs)))
+     case Not(Const(v)) =>
+       Const(false == v)
+     case Not(Not(e)) =>
+       nnf(e)
+     case And(lhs, rhs) =>
+       And(nnf(lhs),​ nnf(rhs))
+     case Or(lhs, rhs) =>
+       Or(nnf(lhs),​ nnf(rhs))
+     case other =>
+       other
+   }
+ } ensuring {
+   (res : Formula) => isNNF(res) && (formula, res) passes {
+     case Not(Const(true)) =>
+       Const(false)
+     case Not(Const(false)) =>
+       Const(true)
+   }
+ }
+
+ %%% PropLogic4.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ Or(nnf(lhs),​ nnf(rhs))
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def nnf(formula : Formula): Formula = {
+   formula match {
+     case Not(And(lhs,​ rhs)) =>
+       Or(nnf(Not(lhs)),​ nnf(Not(rhs)))
+     case Not(Or(lhs, rhs)) =>
+       And(nnf(Not(lhs)),​ nnf(Not(rhs)))
+     case Not(Const(v)) =>
+       Const(!v)
+     case Not(Not(e)) =>
+       nnf(e)
+     case And(lhs, rhs) =>
+       And(nnf(lhs),​ nnf(rhs))
+     case Or(lhs, rhs) =>
+       Or(nnf(lhs),​ nnf(rhs))
+     case other =>
+       other
+   }
+ } ensuring {
+   (res : Formula) => isNNF(res) && (formula, res) passes {
+     case Or(Not(Const(c)),​ Not(Literal(l))) =>
+       Or(Const(!c),​ Not(Literal(l)))
+   }
+ }
+
+ %%% PropLogic5.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ Or(nnf(lhs),​ nnf(rhs))
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def nnf(formula : Formula): Formula = {
+   formula match {
+     case Not(And(lhs,​ rhs)) =>
+       Or(nnf(Not(lhs)),​ nnf(Not(rhs)))
+     case Not(Or(lhs, rhs)) =>
+       And(nnf(Not(lhs)),​ nnf(Not(rhs)))
+     case Not(Const(v)) =>
+       Const(!v)
+     case Not(Not(e)) =>
+       nnf(e)
+     case And(lhs, rhs) =>
+       And(nnf(lhs),​ nnf(rhs))
+     case Or(lhs, rhs) =>
+       Or(nnf(lhs),​ nnf(rhs))
+     case other =>
+       other
+   }
+ } ensuring {
+   (res : Formula) => isNNF(res) && (formula, res) passes {
+     case Or(Not(Const(c)),​ Not(Literal(l))) =>
+       Or(Const(!c),​ Not(Literal(l)))
+   }
+ }
+
+ %%% List1.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def List0\$pad[T](\$this : List0[T], s : Int, e : T): List0[T] = {
+   (\$this, s) match {
+     case (_, s) if s <= 0 =>
+       \$this
+     case (Nil0(), s) =>
+       Cons0[T](e, Nil0[T]().pad(s - 1, e))
+     case (Cons0(h, t), s) =>
+   }
+ } ensuring {
+   (res : List0[T]) => ((\$this, s, e), res) passes {
+     case (Cons0(a, Nil0()), 2, x) =>
+       Cons0[T](a, Cons0[T](x, Cons0[T](x, Nil0[T]())))
+   }
+ }
+
+ %%% List2.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ Cons0[T](x,​ xs ++ that)
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def List0\$\$plus\$plus[T](\$this : List0[T], that : List0[T]): List0[T] = {
+   \$this match {
+     case Nil0() =>
+       that
+     case Cons0(x, xs) =>
+       Cons0[T](x, xs ++ that)
+   }
+ } ensuring {
+   (res : List0[T]) => res.content() == \$this.content() ++ that.content() && res.size() == \$this.size() + that.size()
+ }
+
+ %%% List3.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ Cons0[T](t,​ Nil0[T]())
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def List0\$ap[T](\$this : List0[T], t : T): List0[T] = {
+   \$this match {
+     case Nil0() =>
+       Cons0[T](t, Nil0[T]())
+     case Cons0(x, xs) =>
+       Cons0[T](x, xs.ap(t))
+   }
+ } ensuring {
+   (res : List0[T]) => res.size() == \$this.size() + 1 && res.content() == \$this.content() ++ Set[T](t)
+ }
+
+ %%% List4.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ if (h == from) {
+   Cons0[T](to,​ t.replace(h,​ to))
+ } else {
+   Cons0[T](h, r)
+ }
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def List0\$replace[T](\$this : List0[T], from : T, to : T): List0[T] = {
+   \$this match {
+     case Nil0() =>
+       Nil0[T]()
+     case Cons0(h, t) =>
+       val r = t.replace(from,​ to);
+       if (h == from) {
+         Cons0[T](to,​ t.replace(h,​ to))
+       } else {
+         Cons0[T](h, r)
+       }
+   }
+ } ensuring {
+   (res : List0[T]) => \$this.content() -- Set[T](from) ++ (if (\$this.content().contains(e)) {
+     Set[T](to)
+   } else {
+     Set[T]()
+   }) == res.content() && res.size() == \$this.size()
+ }
+
+ %%% List5.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ t.count(h) + 1
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def List0\$count[T](\$this : List0[T], e : T): Int = {
+   \$this match {
+     case Cons0(h, t) =>
+       if (h == e) {
+         t.count(h) + 1
+       } else {
+         t.count(e)
+       }
+     case Nil0() =>
+       0
+   }
+ } ensuring {
+   (x\$2 : Int) => ((\$this, e), x\$2) passes {
+     case (Cons0(a, Cons0(b, Cons0(a1, Cons0(b2, Nil0())))), a2) if a == a1 && a == a2 && b != a2 && b2 != a2 =>
+       2
+     case (Cons0(a, Cons0(b, Nil0())), c) if a != c && b != c =>
+       0
+   }
+ }
+
+ %%% List6.scala %%%
+ Solution is not trusted!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ Some[Int](i + 1)
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def List0\$find[T](\$this : List0[T], e : T): Option[Int] = {
+   \$this match {
+     case Nil0() =>
+       None[Int]()
+     case Cons0(h, t) =>
+       if (h == e) {
+         Some[Int](0)
+       } else {
+         t.find(e) match {
+           case None() =>
+             None[Int]()
+           case Some(i) =>
+             Some[Int](i + 1)
+         }
+       }
+   }
+ } ensuring {
+   (res : Option[Int]) => if (\$this.content().contains(e)) {
+     res.isDefined() && \$this.size() > res.get() && \$this.apply(res.get()) == e
+   } else {
+     res.isEmpty()
+   }
+ }
+
+ %%% List7.scala %%%
+ Solution is not trusted!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ Some[Int]((i + 2) - 1)
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def List0\$find[T](\$this : List0[T], e : T): Option[Int] = {
+   \$this match {
+     case Nil0() =>
+       None[Int]()
+     case Cons0(h, t) =>
+       if (h == e) {
+         Some[Int](0)
+       } else {
+         t.find(e) match {
+           case None() =>
+             None[Int]()
+           case Some(i) =>
+             Some[Int]((i + 2) - 1)
+         }
+       }
+   }
+ } ensuring {
+   (res : Option[Int]) => if (\$this.content().contains(e)) {
+     res.isDefined() && \$this.size() > res.get() && \$this.apply(res.get()) == e
+   } else {
+     res.isEmpty()
+   }
+ }
+
+ %%% List8.scala %%%
+ Solution is not trusted!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ if (e == h) {
+   Some[Int](0)
+ } else {
+   t.find(e) match {
+     case None() =>
+       None[Int]()
+     case Some(i) =>
+       Some[Int](i + 1)
+   }
+ }
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def List0\$find[T](\$this : List0[T], e : T): Option[Int] = {
+   \$this match {
+     case Nil0() =>
+       None[Int]()
+     case Cons0(h, t) =>
+       if (e == h) {
+         Some[Int](0)
+       } else {
+         t.find(e) match {
+           case None() =>
+             None[Int]()
+           case Some(i) =>
+             Some[Int](i + 1)
+         }
+       }
+   }
+ } ensuring {
+   (res : Option[Int]) => if (\$this.content().contains(e)) {
+     res.isDefined() && \$this.size() > res.get() && \$this.apply(res.get()) == e
+   } else {
+     res.isEmpty()
+   }
+ }
+
+ %%% List9.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ 1 + t.size()
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def List0\$size[T](\$this : List0[T]): Int = {
+   \$this match {
+     case Nil0() =>
+       0
+     case Cons0(h, t) =>
+       1 + t.size()
+   }
+ } ensuring {
+   (x\$1 : Int) => (\$this, x\$1) passes {
+     case Cons0(_, Nil0()) =>
+       1
+     case Nil0() =>
+       0
+   }
+ }
+
+ %%% List10.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ h + sum(t)
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def sum(l : List0[Int]):​ Int = {
+   l match {
+     case Nil0() =>
+       0
+     case Cons0(h, t) =>
+       h + sum(t)
+   }
+ } ensuring {
+   (x\$2 : Int) => (l, x\$2) passes {
+     case Cons0(a, Nil0()) =>
+       a
+     case Cons0(a, Cons0(b, Nil0())) =>
+       a + b
+   }
+ }
+
+ %%% List11.scala %%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ t - e
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def List0\$\$minus[T](\$this : List0[T], e : T): List0[T] = {
+   \$this match {
+     case Cons0(h, t) =>
+       if (e == h) {
+         t - e
+       } else {
+         Cons0[T](h, t - e)
+       }
+     case Nil0() =>
+       Nil0[T]()
+   }
+ } ensuring {
+   (res : List0[T]) => res.content() == \$this.content() -- Set[T](e)
+ }
+
+ %%% List12.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ val scrut = (\$this, i);
+   scrut match {
+     case (Nil0(), _) =>
+       Nil0[T]()
+     case (Cons0(h, t), 0) =>
+       scrut._1
+     case (Cons0(_, t), i) =>
+       t.drop(2)
+   }
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def List0\$drop[T](\$this : List0[T], i : Int): List0[T] = {
+   val scrut = (\$this, i);
+   scrut match {
+     case (Nil0(), _) =>
+       Nil0[T]()
+     case (Cons0(h, t), 0) =>
+       scrut._1
+     case (Cons0(_, t), i) =>
+       t.drop(2)
+   }
+ } ensuring {
+   (res : List0[T]) => ((\$this, i), res) passes {
+     case (Cons0(_, Nil0()), 42) =>
+       Nil0[T]()
+     case (l @ Cons0(_, _), 0) =>
+       l
+     case (Cons0(a, Cons0(b, Nil0())), 1) =>
+       Cons0[T](b, Nil0[T]())
+     case (Cons0(a, Cons0(b, Cons0(c, Nil0()))), 2) =>
+       Cons0[T](c, Nil0[T]())
+   }
+ }
+
+ %%% Numerical1.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ power(base,​ p - 1) * base
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def power(base : Int, p : Int): Int = {
+   require(p >= 0)
+   if (p == 0) {
+     1
+   } else {
+     if (p % 2 == 0) {
+       power(base * base, p / 2)
+     } else {
+       power(base, p - 1) * base
+     }
+   }
+ } ensuring {
+   (res : Int) => ((base, p), res) passes {
+     case (_, 0) =>
+       1
+     case (b, 1) =>
+       b
+     case (2, 7) =>
+       128
+     case (2, 10) =>
+       1024
+   }
+ }
+
+ %%% Numerical2.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ (a, 0)
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def moddiv(a : Int, b : Int): (Int, Int) = {
+   require(a >= 0 && b > 0)
+   if (b > a) {
+     (a, 0)
+   } else {
+     {val x\$1 = {
+       moddiv(a - b, b) match {
+         case (r1, r2) =>
+           (r1, r2)
+       }
+     }
+     val r1 = {
+       x\$1._1
+     }
+     val r2 = x\$1._2;
+     (r1, (r2 + 1))}
+   }
+ } ensuring {
+   (res : (Int, Int)) => b * res._2 + res._1 == a
+ }
+
+ %%% MergeSort1.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ (Cons(b, rec1), Cons(a, rec2))
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def split(l : List): (List, List) = {
+   l match {
+     case Cons(a, Cons(b, t)) =>
+       val x\$1 = {
+         split(t) match {
+           case (rec1, rec2) =>
+             (rec1, rec2)
+         }
+       }
+       val rec1 = {
+         x\$1._1
+       }
+       val rec2 = x\$1._2;
+       (Cons(b, rec1), Cons(a, rec2))
+     case other =>
+       (other, Nil())
+   }
+ } ensuring {
+   (res : (List, List)) => val x\$2 = {
+     res match {
+       case (l1, l2) =>
+         (l1, l2)
+     }
+   }
+   val l1 = {
+     x\$2._1
+   }
+   val l2 = x\$2._2;
+   l1.size() >= l2.size() && l1.size() <= l2.size() + 1 && l1.size() + l2.size() == l.size() && l1.content() ++ l2.content() == l.content()
+ }
+
+ %%% MergeSort2.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ Cons[Int](h2,​ merge(l1, t2))
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def merge(l1 : List[Int], l2 : List[Int]): List[Int] = {
+   require(isSorted(l1) && isSorted(l2))
+   (l1, l2) match {
+     case (Cons(h1, t1), Cons(h2, t2)) =>
+       if (h1 <= h2) {
+         Cons[Int](h1,​ merge(t1, l2))
+       } else {
+         Cons[Int](h2,​ merge(l1, t2))
+       }
+     case (Nil(), _) =>
+       l2
+     case (_, Nil()) =>
+       l1
+   }
+ } ensuring {
+   (res : List[Int]) => isSorted(res) && res.size() == l1.size() + l2.size() && res.content() == l1.content() ++ l2.content()
+ }
+
+ %%% MergeSort3.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ h2 >= h1
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def merge(l1 : List[Int], l2 : List[Int]): List[Int] = {
+   require(isSorted(l1) && isSorted(l2))
+   (l1, l2) match {
+     case (Cons(h1, t1), Cons(h2, t2)) =>
+       if (h2 >= h1) {
+         Cons[Int](h1,​ merge(t1, l2))
+       } else {
+         Cons[Int](h2,​ merge(l1, t2))
+       }
+     case (Nil(), _) =>
+       l2
+     case (_, Nil()) =>
+       l1
+   }
+ } ensuring {
+   (res : List[Int]) => isSorted(res) && res.size() == l1.size() + l2.size() && res.content() == l1.content() ++ l2.content()
+ }
+
+ %%% MergeSort4.scala %%%
+ Found trusted solution!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ h2 :: merge(l1, t2)
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def merge(l1 : List[Int], l2 : List[Int]): List[Int] = {
+   require(isSorted(l1) && isSorted(l2))
+   (l1, l2) match {
+     case (Cons(h1, t1), Cons(h2, t2)) =>
+       if (h1 <= h2) {
+         Cons[Int](h1,​ merge(t1, l2))
+       } else {
+         h2 :: merge(l1, t2)
+       }
+     case (Nil(), _) =>
+       l2
+     case (_, Nil()) =>
+       l1
+   }
+ } ensuring {
+   (res : List[Int]) => isSorted(res) && res.size() == l1.size() + l2.size() && res.content() == l1.content() ++ l2.content()
+ }
+
+ %%% MergeSort5.scala %%%
+ Solution is not trusted!
+ ============================== Repair successful: ==============================
+ --------------------------------- Solution 1: ---------------------------------
+ (l1, l2) match {
+   case (Nil(), _) =>
+     l2
+   case (_, Nil()) =>
+     l1
+   case (Cons(h1, t1), Cons(h2, t2)) =>
+     if (h1 <= h2) {
+       Cons[Int](h1,​ merge(t1, l2))
+     } else {
+       Cons[Int](h2,​ merge(l1, t2))
+     }
+ }
+ ================================= In context: =================================
+ --------------------------------- Solution 1: ---------------------------------
+ def merge(l1 : List[Int], l2 : List[Int]): List[Int] = {
+   require(isSorted(l1) && isSorted(l2))
+   (l1, l2) match {
+     case (Nil(), _) =>
+       l2
+     case (_, Nil()) =>
+       l1
+     case (Cons(h1, t1), Cons(h2, t2)) =>
+       if (h1 <= h2) {
+         Cons[Int](h1,​ merge(t1, l2))
+       } else {
+         Cons[Int](h2,​ merge(l1, t2))
+       }
+   }
+ } ensuring {
+   (res : List[Int]) => isSorted(res) && res.size() == l1.size() + l2.size() && res.content() == l1.content() ++ l2.content()
+ }