diff --git a/src/main/scala/leon/synthesis/FileInterface.scala b/src/main/scala/leon/synthesis/FileInterface.scala
index c2bac94cae74b3e573b56fc3b8754da99dcdd063..02b5f9456426ff5a19bcb62de15709348b71c63b 100644
--- a/src/main/scala/leon/synthesis/FileInterface.scala
+++ b/src/main/scala/leon/synthesis/FileInterface.scala
@@ -58,9 +58,6 @@ class FileInterface(reporter: Reporter) {
         // Get base indentation of last line:
         val lineChars = before.substring(before.lastIndexOf('\n')+1).toList
 
-        println(lineChars)
-        println(lineChars.takeWhile(_ == ' '))
-
         val indent = lineChars.takeWhile(_ == ' ').size
 
         val p = new ScalaPrinter(PrinterOptions())
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index efbc68ef0f3b1537976d2819ead2fb3f4455b1e6..b05db6949b8f07ae23128dbbd2ccc512c29c5d53 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -110,7 +110,13 @@ case object IntegerEquation extends Rule("Integer Equation") {
               None
           }
 
-          List(RuleInstantiation.immediateDecomp(problem, this, List(newProblem), onSuccess, this.name))
+
+          if (subproblemxs.isEmpty) {
+            // we directly solve
+            List(RuleInstantiation.immediateSuccess(problem, this, onSuccess(List(Solution(And(eqPre, problem.pc), Set(), Tuple(Seq())))).get))
+          } else {
+            List(RuleInstantiation.immediateDecomp(problem, this, List(newProblem), onSuccess, this.name))
+          }
         }
       }
     }