Improvements

src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala

@@ -354,7 +354,7 @@ abstract class SMTLIBSolver(val context: LeonContext,
           case more =>
             val es = freshSym("e")
             SMTLet(VarBinding(es, toSMT(e)), Seq(),
-              Core.Or((oneOf map (FunctionApplication(_, Seq(es:Term)))): _*)
+              Core.Or(oneOf.map(FunctionApplication(_, Seq(es:Term))): _*)
             )
         }
 

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

@@ -33,7 +33,7 @@ case object IntegerInequalities extends Rule("Integer Inequalities") {
 
     val ineqVars = lhsSides.foldLeft(Set[Identifier]())((acc, lhs) => acc ++ variablesOf(lhs))
     val nonIneqVars = exprNotUsed.foldLeft(Set[Identifier]())((acc, x) => acc ++ variablesOf(x))
-    val candidateVars = ineqVars.intersect(problem.xs.toSet).filterNot(nonIneqVars.contains)
+    val candidateVars = ineqVars.intersect(problem.xs.toSet).diff(nonIneqVars)
 
     val processedVars: Set[(Identifier, Int)] = candidateVars.flatMap(v => {
       try {

src/main/scala/leon/utils/ModelEnumerator.scala

@@ -51,11 +51,11 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
         s.check == Some(true)
       }
 
-      def next = {
+      def next() = {
         val sm = s.getModel
-        val model = (ids.map { id =>
+        val model = ids.map { id =>
           id -> sm.getOrElse(id, simplestValue(id.getType))
-        }).toMap
+        }.toMap
 
 
         // Vary the model
@@ -131,7 +131,8 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
         Stream.empty
       } else {
         // Assert a new pivot point
-        val thisTry = getPivot().map { t =>
+        val thisTry = getPivot()
+        thisTry.foreach { t =>
           s.push()
           dir match {
             case Up =>
@@ -145,9 +146,9 @@ class ModelEnumerator(ctx: LeonContext, pgm: Program, sf: SolverFactory[Solver])
         s.check match {
           case Some(true) =>
             val sm = s.getModel
-            val m = (ids.map { id =>
+            val m = ids.map { id =>
               id -> sm.getOrElse(id, simplestValue(id.getType))
-            }).toMap
+            }.toMap
 
             evaluator.eval(measure, m).result match {
               case Some(InfiniteIntegerLiteral(measureVal)) =>