.. I guess this time should be good

src/main/scala/leon/synthesis/LinearEquations.scala

@@ -10,7 +10,7 @@ object LinearEquations {
   //eliminate one variable from normalizedEquation t + a1*x1 + ... + an*xn = 0
   //return a mapping for each of the n variables in (pre, map, freshVars)
   def elimVariable(as: Set[Identifier], normalizedEquation: List[Expr]): (Expr, List[Expr], List[Identifier]) = {
-    println("elim in normalized: " + normalizedEquation)
+    require(normalizedEquation.size > 1)
     require(normalizedEquation.tail.forall{case IntLiteral(i) if i != 0 => true case _ => false})
     val t: Expr = normalizedEquation.head
     val coefsVars: List[Int] = normalizedEquation.tail.map{case IntLiteral(i) => i}

src/main/scala/leon/synthesis/Rules.scala

@@ -578,17 +578,17 @@ class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth
       case Some(normalizedEq0) => {
         val (neqxs, normalizedEq) = eqxs.zip(normalizedEq0.tail).filterNot{ case (_, IntLiteral(0)) => true case _ => false}.unzip
 
-        if(normalizedEq.size == 1) {
+        //if(normalizedEq.size == 1) {
 
 
-        } else {
+        //} else {
 
         val (eqPre, eqWitness, eqFreshVars) = elimVariable(eqas, normalizedEq)
 
         val eqSubstMap: Map[Expr, Expr] = neqxs.zip(eqWitness).map{case (id, e) => (Variable(id), simplify(e))}.toMap
         val freshFormula = simplify(replace(eqSubstMap, And(allOthers)))
-        }
-        (eqPre, freshFormula)
+        //}
+        //(eqPre, freshFormula)
 
         val newProblem = Problem(as, And(eqPre, p.c), freshFormula, eqFreshVars)