diff --git a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala b/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
index cd49ece38c08e681dc5a6abe696112533339f4af..5f23fade21bf4f86c79ef5e9d76abaf219a5b23f 100644
--- a/src/main/scala/leon/solvers/smtlib/SMTLIBSolver.scala
+++ b/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))): _*)
             )
         }
 
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 9bd49fcebfc4f44ed4e874cfc1a7bf00bb0c0991..0c7c8a961814cfc25c7ecbd98acae33d98787c35 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/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 {
diff --git a/src/main/scala/leon/utils/ModelEnumerator.scala b/src/main/scala/leon/utils/ModelEnumerator.scala
index e813d8b504ad7b462a811ddd48ad66091cd17885..2467a902137a37929580e33a04debbf78411069c 100644
--- a/src/main/scala/leon/utils/ModelEnumerator.scala
+++ b/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)) =>