Some small benchmark changes

testcases/synthesis/repair/DaysToYears/DaysToYears1.scala

@@ -22,8 +22,9 @@ object DaysToYears {
     res._2 >  0   && 
     res._1 >= base &&
     (((year,days), res) passes { 
-      case (1980, 366 ) => (1980, 366)
-      case (1980, 1000) => (1982, 269)
+      case (1999, 14 )  => (1999, 14)
+      case (1980, 366)  => (1980, 366)
+      case (1981, 634)  => (1982, 269)
     })
   } 
 

testcases/synthesis/repair/Desugar/Desugar1.scala

@@ -145,7 +145,7 @@ object Desugar {
 
   @induct
   def desugar(e : Trees.Expr) : SimpleE = { e match {
-    case Trees.Plus (lhs, rhs) => Neg(desugar(lhs)) // FIXME: Complete nonsense. Leon can't disprove it so it's happy...
+    case Trees.Plus (lhs, rhs) => Neg(desugar(lhs)) // FIXME: Complete nonsense. Leon can't disprove it, uses example...
     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)) 
@@ -157,7 +157,6 @@ object Desugar {
     case Trees.IntLiteral(v)  => Literal(v)
     case Trees.BoolLiteral(b) => Literal(b2i(b))
   }} ensuring { res =>
-    // TODO: Z3 fails to disprove this!
     ((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))))

testcases/synthesis/repair/RedBlackTree/RedBlackTree.scala

@@ -82,62 +82,20 @@ object RedBlackTree {
     makeBlack(ins(x, t))
   } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res) && blackBalanced(res) )
   
-//  def buggyAdd(x: Int, t: Tree): Tree = {
-//    require(redNodesHaveBlackChildren(t))
-//    // makeBlack(ins(x, t))
-//    ins(x, t)
-//  } ensuring (res => content(res) == content(t) ++ Set(x) && redNodesHaveBlackChildren(res))
   
   def balance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
-    // require(
-    //   Node(c,a,x,b) match {
-    //     case Node(Black,Node(Red,Node(Red,a,_,b),_,c),_,d) =>
-    //       redNodesHaveBlackChildren(a) &&
-    //       redNodesHaveBlackChildren(b) &&
-    //       redNodesHaveBlackChildren(c) &&
-    //       redNodesHaveBlackChildren(d)
-    //     case Node(Black,Node(Red,a,_,Node(Red,b,_,c)),_,d) =>
-    //       redNodesHaveBlackChildren(a) &&
-    //       redNodesHaveBlackChildren(b) &&
-    //       redNodesHaveBlackChildren(c) &&
-    //       redNodesHaveBlackChildren(d)
-    //     case Node(Black,a,_,Node(Red,Node(Red,b,_,c),_,d)) => 
-    //       redNodesHaveBlackChildren(a) &&
-    //       redNodesHaveBlackChildren(b) &&
-    //       redNodesHaveBlackChildren(c) &&
-    //       redNodesHaveBlackChildren(d)
-    //     case Node(Black,a,_,Node(Red,b,_,Node(Red,c,_,d))) => 
-    //       redNodesHaveBlackChildren(a) &&
-    //       redNodesHaveBlackChildren(b) &&
-    //       redNodesHaveBlackChildren(c) &&
-    //       redNodesHaveBlackChildren(d)
-    //     case t => redDescHaveBlackChildren(t)
-    //   }
-    // )
-    Node(c,a,x,b) match {
-      case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) => 
+
+    (c,a,x,b) match {
+      case (Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) => 
         Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
-      case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) => 
+      case (Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) => 
         Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
-      case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) => 
+      case (Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) => 
         Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
-      case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) => 
+      case (Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) => 
         Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
-      case Node(c,a,xV,b) => Node(c,a,xV,b)
+      case (c,a,xV,b) => Node(c,a,xV,b)
     }
-  } ensuring (res => content(res) == content(Node(c,a,x,b)) )// && redDescHaveBlackChildren(res))
-
-  // def buggyBalance(c: Color, a: Tree, x: Int, b: Tree): Tree = {
-  //   Node(c,a,x,b) match {
-  //     case Node(Black,Node(Red,Node(Red,a,xV,b),yV,c),zV,d) => 
-  //       Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
-  //     case Node(Black,Node(Red,a,xV,Node(Red,b,yV,c)),zV,d) => 
-  //       Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
-  //     case Node(Black,a,xV,Node(Red,Node(Red,b,yV,c),zV,d)) => 
-  //       Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
-  //     case Node(Black,a,xV,Node(Red,b,yV,Node(Red,c,zV,d))) => 
-  //       Node(Red,Node(Black,a,xV,b),yV,Node(Black,c,zV,d))
-  //   }
-  // } ensuring (res => content(res) == content(Node(c,a,x,b)) ) // && redDescHaveBlackChildren(res))
+  } ensuring (res => content(res) == content(Node(c,a,x,b)))// && redDescHaveBlackChildren(res))
 
 }