Chased the Set.empty[Int] vs. Set() subtelty.

src/main/scala/leon/synthesis/Rules.scala

@@ -441,6 +441,8 @@ class CEGIS(synth: Synthesizer) extends Rule("CEGIS", synth, 150) {
                 result = Some(RuleSuccess(Solution(BooleanLiteral(true), Set(), Tuple(p.xs.map(valuateWithModel(mapping))).setType(tpe))))
 
               case _ =>
+                reporter.warning("Solver returned 'UNKNOWN' in a CEGIS iteration.")
+                continue = false
             }
 
           case (Some(false), _) =>
@@ -479,12 +481,14 @@ class OptimisticGround(synth: Synthesizer) extends Rule("Optimistic Ground", syn
 
       while (result.isEmpty && i < maxTries) {
         val phi = And(p.phi +: predicates)
+        //println("SOLVING " + phi + " ...")
         synth.solver.solveSAT(phi) match {
           case (Some(true), satModel) =>
             val satXsModel = satModel.filterKeys(xss) 
 
             val newPhi = valuateWithModelIn(phi, xss, satModel)
 
+            //println("REFUTING " + Not(newPhi) + "...")
             synth.solver.solveSAT(Not(newPhi)) match {
               case (Some(true), invalidModel) =>
                 // Found as such as the xs break, refine predicates
@@ -535,7 +539,7 @@ class EqualitySplit(synth: Synthesizer) extends Rule("Eq. Split.", synth, 90) {
       )
     }
 
-    val candidate = p.as.groupBy(_.getType).map(_._2.toList).find{
+    val candidate = p.as.groupBy(_.getType).map(_._2.toList).find {
       case List(a1, a2) => (pres & combinations(a1, a2)).isEmpty
       case _ => false
     }

testcases/synthesis/ADTInduction.scala

@@ -16,11 +16,21 @@ object SortedList {
   //def sizeSynth(l: List): Int = choose{ (i: Int) => i >= 0 && sizeSynth(Cons(0, l)) == i + 1}
 
   def content(l: List): Set[Int] = l match {
-    case Nil() => Set()
+    case Nil() => Set.empty[Int]
     case Cons(i, t) => Set(i) ++ content(t)
   }
 
-  def deleteSynth(in: List, v: Int) = choose{ (out: List) => !(content(out) contains v) && size(out)+1 >= size(in) }
+  //def artifialSubcase(v : Int) = choose {
+  //  (out : List) =>
+  //    content(out) == (content(Nil()) -- Set(v))
+  //}
+
+  def deleteSynth(in: List, v: Int) = choose {
+    (out: List) =>
+      // This spec is too weak. Maybe use later as bad example?
+      //!(content(out) contains v) && size(out)+1 >= size(in)
+      (content(out) == (content(in) -- Set(v)))
+  }
 
   def isSorted(l: List): Boolean = l match {
     case Nil() => true