diff --git a/src/main/scala/leon/synthesis/LinearEquations.scala b/src/main/scala/leon/synthesis/LinearEquations.scala
index a3ebe75da74da3b9db54207889b66736889a9d3d..3d9eb6230bd9ad18c1b41da40de1aa07d754c354 100644
--- a/src/main/scala/leon/synthesis/LinearEquations.scala
+++ b/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}
diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index 36576a1f4ac9e59a298598270568424f0a0a0f56..70bfbea92737651e26904e7663086eacc22762c6 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -547,40 +547,64 @@ class IntegerEquation(synth: Synthesizer) extends Rule("Integer Equation", synth
     val formula = p.phi
 
     val (eqs, others) = exprs.partition(_.isInstanceOf[Equals])
+    var candidates: Seq[Expr] = eqs
+    var allOthers: Seq[Expr] = others
+
+    var vars: Set[Identifier] = Set()
+    var eqas: Set[Identifier] = Set()
+    var eqxs: List[Identifier] = List()
+    var ys: Set[Identifier] = Set()
+
+    var optionNormalizedEq: Option[List[Expr]] = None
+    while(!candidates.isEmpty && optionNormalizedEq == None) {
+      val eq@Equals(_,_) = candidates.head
+      candidates = candidates.tail
+      
+      vars = variablesOf(eq)
+      eqas = as.toSet.intersect(vars)
+
+      eqxs = xs.toSet.intersect(vars).toList
+      ys = xs.toSet.diff(vars)
+
+      try {
+        optionNormalizedEq = Some(ArithmeticNormalization(Minus(eq.left, eq.right), eqxs.toArray).toList)
+      } catch {
+        case ArithmeticNormalization.NonLinearExpressionException(_) =>
+      }
+    }
 
-    if (!eqs.isEmpty) {
+    optionNormalizedEq match {
+      case None => RuleInapplicable
+      case Some(normalizedEq0) => {
+        val (neqxs, normalizedEq) = eqxs.zip(normalizedEq0.tail).filterNot{ case (_, IntLiteral(0)) => true case _ => false}.unzip
 
-      val (eq@Equals(_,_), rest) = (eqs.head, eqs.tail)
-      val allOthers = rest ++ others
+        //if(normalizedEq.size == 1) {
 
-      val vars: Set[Identifier] = variablesOf(eq)
-      val eqas: Set[Identifier] = as.toSet.intersect(vars)
 
-      val eqxs: List[Identifier] = xs.toSet.intersect(vars).toList
-      val ys: Set[Identifier] = xs.toSet.diff(vars)
+        //} else {
 
-      val normalizedEq: List[Expr] = ArithmeticNormalization(Minus(eq.left, eq.right), eqxs.toArray).toList
-      val (eqPre, eqWitness, eqFreshVars) = elimVariable(eqas, normalizedEq)
+        val (eqPre, eqWitness, eqFreshVars) = elimVariable(eqas, normalizedEq)
 
-      val eqSubstMap: Map[Expr, Expr] = eqxs.zip(eqWitness).map{case (id, e) => (Variable(id), simplify(e))}.toMap
-      val freshFormula = simplify(replace(eqSubstMap, And(allOthers)))
-      (eqPre, freshFormula)
+        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)
 
-      val newProblem = Problem(as, And(eqPre, p.c), freshFormula, eqFreshVars)
+        val newProblem = Problem(as, And(eqPre, p.c), freshFormula, eqFreshVars)
 
-      val onSuccess: List[Solution] => Solution = { 
-        case List(Solution(pre, defs, term)) =>
-          if (eqFreshVars.isEmpty) {
-            Solution(pre, defs, replace(eqSubstMap, Tuple(eqxs.map(Variable(_)))))
-          } else {
-            Solution(pre, defs, LetTuple(eqFreshVars, term, replace(eqSubstMap, Tuple(eqxs.map(Variable(_))))))
-          }
-        case _ => Solution.none
-      }
+        val onSuccess: List[Solution] => Solution = { 
+          case List(Solution(pre, defs, term)) =>
+            if (eqFreshVars.isEmpty) {
+              Solution(pre, defs, replace(eqSubstMap, Tuple(neqxs.map(Variable(_)))))
+            } else {
+              Solution(pre, defs, LetTuple(eqFreshVars, term, replace(eqSubstMap, Tuple(neqxs.map(Variable(_))))))
+            }
+          case _ => Solution.none
+        }
 
-      RuleStep(List(newProblem), onSuccess)
-    } else {
-      RuleInapplicable
+        RuleStep(List(newProblem), onSuccess)
+      }
     }
+
   }
 }
diff --git a/testcases/synthesis/ChooseArith.scala b/testcases/synthesis/ChooseArith.scala
new file mode 100644
index 0000000000000000000000000000000000000000..b910cd4ea699d51566f69f6b2aff3d43c6e6c2c8
--- /dev/null
+++ b/testcases/synthesis/ChooseArith.scala
@@ -0,0 +1,6 @@
+import leon.Utils._
+
+object ChooseArith {
+  def c1(a : Int) : (Int, Int) = 
+    choose((x:Int,y:Int) => 2*x + 4*a == -y)
+}