In IfSplit, don't split if only one branch is taken

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

@@ -4,6 +4,7 @@ package leon
 package synthesis
 package rules
 
+import leon.solvers._
 import purescala.Expressions._
 import purescala.ExprOps._
 import purescala.Constructors._
@@ -11,7 +12,17 @@ import purescala.Constructors._
 case object IfSplit extends Rule("If-Split") {
   def instantiateOn(implicit hctx: SearchContext, p: Problem): Traversable[RuleInstantiation] = {
 
-    def split(i: IfExpr, description: String): RuleInstantiation = {
+    def split(i: IfExpr, description: String): Option[RuleInstantiation] = {
+
+      val solver = SimpleSolverAPI(SolverFactory.getFromSettings(hctx, hctx.program).withTimeout(1000))
+      if (
+        solver.solveVALID(p.pc implies     i.cond ).contains(true) ||
+        solver.solveVALID(p.pc implies not(i.cond)).contains(true)
+      ){
+        // Condition can only go one way, no reason to split...
+        return None
+      }
+
       val subs = List(
         Problem(p.as, p.ws, p.pc withCond i.cond, replace(Map(i -> i.thenn), p.phi), p.xs),
         Problem(p.as, p.ws, p.pc withCond not(i.cond), replace(Map(i -> i.elze), p.phi), p.xs)
@@ -31,7 +42,7 @@ case object IfSplit extends Rule("If-Split") {
           None
       }
 
-      decomp(subs, onSuccess, description)
+      Some(decomp(subs, onSuccess, description))
     }
 
     val ifs = collect{
@@ -44,9 +55,9 @@ case object IfSplit extends Rule("If-Split") {
     ifs.flatMap { 
       case i @ IfExpr(cond, _, _) =>
         if ((variablesOf(cond) & xsSet).isEmpty) {
-          List(split(i, s"If-Split on '$cond'"))
+          split(i, s"If-Split on '${cond.asString}'")
         } else {
-          Nil
+          None
         }
     }