QEB.flatMapIns should still return EB

src/main/scala/leon/synthesis/ExamplesBank.scala

@@ -185,16 +185,16 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb:
     QualifiedExamplesBank(nas, xs, eb flatMapIns { (in: Seq[Expr]) => List(toKeep.map(in)) })
   }
 
+  def evalIns: QualifiedExamplesBank = copy( eb = flatMapIns { mapping =>
+    val evalAs = evaluator.evalEnv(mapping)
+    List(as map evalAs)
+  })
+
   /** Filter inputs through expr which is an expression evaluating to a boolean */
   def filterIns(expr: Expr): QualifiedExamplesBank = {
     filterIns(m => evaluator.eval(expr, m).result.contains(BooleanLiteral(true)))
   }
 
-  def evalIns: QualifiedExamplesBank = flatMapIns { mapping =>
-    val evalAs = evaluator.evalEnv(mapping)
-    List(as map evalAs)
-  }
-
   /** Filters inputs through the predicate pred, with an assignment of input variables to expressions. */
   def filterIns(pred: Map[Identifier, Expr] => Boolean): QualifiedExamplesBank = {
     QualifiedExamplesBank(as, xs,
@@ -212,14 +212,14 @@ case class QualifiedExamplesBank(as: List[Identifier], xs: List[Identifier], eb:
   /** Maps inputs through the function f
     *
     * @return A new ExampleBank */
-  def flatMapIns(f: Seq[(Identifier, Expr)] => List[Seq[Expr]]): QualifiedExamplesBank = {
-    copy(eb = eb flatMap {
+  def flatMapIns(f: Seq[(Identifier, Expr)] => List[Seq[Expr]]): ExamplesBank = {
+    eb flatMap {
       case InExample(in) =>
         f(as zip in).map(InExample)
 
       case InOutExample(in, out) =>
         f(as zip in).map(InOutExample(_, out))
-    })
+    }
   }
 }
 

src/main/scala/leon/synthesis/rules/ADTSplit.scala

@@ -100,7 +100,7 @@ case object ADTSplit extends Rule("ADT Split.") {
                 }
               }
             } else {
-              p.qeb
+              p.eb
             }
           }
           val newAs = if (isInputVar) args ::: oas else p.as