diff --git a/src/main/scala/leon/synthesis/Rules.scala b/src/main/scala/leon/synthesis/Rules.scala
index af348baf8edc03ba210a9e0b66d96f7dad78439d..3d24a3c2d11e782c7531e623892eac901bed93bd 100644
--- a/src/main/scala/leon/synthesis/Rules.scala
+++ b/src/main/scala/leon/synthesis/Rules.scala
@@ -75,7 +75,7 @@ object RuleInstantiation {
   }
 }
 
-abstract class Rule(val name: String, val priority: Priority) {
+abstract class Rule(val name: String) {
   def instantiateOn(scrx: SynthesisContext, problem: Problem): Traversable[RuleInstantiation]
 
   def subst(what: Tuple2[Identifier, Expr], in: Expr): Expr = replace(Map(Variable(what._1) -> what._2), in)
diff --git a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
index bd86955401230656104e4e97ab96d3e3af9fb0f0..adcbb72a2625d67c79f6adeaa1c6923065737f6e 100644
--- a/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/ADTInduction.scala
@@ -9,7 +9,7 @@ import purescala.TreeOps._
 import purescala.TypeTrees._
 import purescala.Definitions._
 
-case object ADTInduction extends Rule("ADT Induction", 80) with Heuristic {
+case object ADTInduction extends Rule("ADT Induction") with Heuristic {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val candidates = p.as.collect {
         case IsTyped(origId, AbstractClassType(cd)) => (origId, cd)
diff --git a/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala b/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala
index 5b50ac758c7b9779cbf86e9590cad010dfe12ecf..b2782c5dc3d7dbb1d3a3979a06bf9065df0a68f0 100644
--- a/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala
+++ b/src/main/scala/leon/synthesis/heuristics/InnerCaseSplit.scala
@@ -6,7 +6,7 @@ import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
 
-case object InnerCaseSplit extends Rule("Inner-Case-Split", 200) with Heuristic {
+case object InnerCaseSplit extends Rule("Inner-Case-Split") with Heuristic {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     p.phi match {
       case Or(_) =>
diff --git a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
index a4c7f9cf2eb6704df288b0300c994f7f40557200..fdcc626c4d258c6e4bb0fb787ac97be52ae5526e 100644
--- a/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
+++ b/src/main/scala/leon/synthesis/heuristics/IntInduction.scala
@@ -9,7 +9,7 @@ import purescala.TreeOps._
 import purescala.TypeTrees._
 import purescala.Definitions._
 
-case object IntInduction extends Rule("Int Induction", 50) with Heuristic {
+case object IntInduction extends Rule("Int Induction") with Heuristic {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     p.as match {
       case List(IsTyped(origId, Int32Type)) =>
diff --git a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
index 494e0979af3fe28303c93160c83d91df3b373413..a3ecedd7217d7757e7f324bddaf698c97282fc18 100644
--- a/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
+++ b/src/main/scala/leon/synthesis/heuristics/OptimisticInjection.scala
@@ -9,7 +9,7 @@ import purescala.TreeOps._
 import purescala.TypeTrees._
 import purescala.Definitions._
 
-case object OptimisticInjection extends Rule("Opt. Injection", 50) with Heuristic {
+case object OptimisticInjection extends Rule("Opt. Injection") with Heuristic {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val TopLevelAnds(exprs) = p.phi
 
diff --git a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
index 44ceb787964d3de4097217474b68129d524dd5d7..8e91394f0fc87b33d9ae9bc7aaa2f5724ee809ba 100644
--- a/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
+++ b/src/main/scala/leon/synthesis/heuristics/SelectiveInlining.scala
@@ -9,7 +9,7 @@ import purescala.TreeOps._
 import purescala.TypeTrees._
 import purescala.Definitions._
 
-case object SelectiveInlining extends Rule("Sel. Inlining", 20) with Heuristic {
+case object SelectiveInlining extends Rule("Sel. Inlining") with Heuristic {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val TopLevelAnds(exprs) = p.phi
 
diff --git a/src/main/scala/leon/synthesis/rules/ADTDual.scala b/src/main/scala/leon/synthesis/rules/ADTDual.scala
index 78573c819d24fa57d36c10dc641c7951f365a054..6b6dac90ffe89417e08eb77abd295d0cf3da4ca9 100644
--- a/src/main/scala/leon/synthesis/rules/ADTDual.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTDual.scala
@@ -6,7 +6,7 @@ import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
 
-case object ADTDual extends Rule("ADTDual", 200) {
+case object ADTDual extends Rule("ADTDual") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val xs = p.xs.toSet
     val as = p.as.toSet
diff --git a/src/main/scala/leon/synthesis/rules/ADTSplit.scala b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
index 631fe979a6be3c9934ded19e3898b16542764fbc..e94abd7f1e93160517b56ba45ec6f23980ff8c5c 100644
--- a/src/main/scala/leon/synthesis/rules/ADTSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/ADTSplit.scala
@@ -9,7 +9,7 @@ import purescala.TreeOps._
 import purescala.Extractors._
 import purescala.Definitions._
 
-case object ADTSplit extends Rule("ADT Split.", 70) {
+case object ADTSplit extends Rule("ADT Split.") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation]= {
     val candidates = p.as.collect {
       case IsTyped(id, AbstractClassType(cd)) =>
diff --git a/src/main/scala/leon/synthesis/rules/Assert.scala b/src/main/scala/leon/synthesis/rules/Assert.scala
index 962e090ae850695e9e4c1beae4e2cfb9dd9fda3b..4522067b810caaa610c4339c2fee3a0e0fab143d 100644
--- a/src/main/scala/leon/synthesis/rules/Assert.scala
+++ b/src/main/scala/leon/synthesis/rules/Assert.scala
@@ -6,7 +6,7 @@ import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
 
-case object Assert extends Rule("Assert", 200) {
+case object Assert extends Rule("Assert") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     p.phi match {
       case TopLevelAnds(exprs) =>
diff --git a/src/main/scala/leon/synthesis/rules/CaseSplit.scala b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
index 2375f3375c1f4fc3def4bf5b8e6f826849a352f6..3850b1d745a3d70bf5e0abdf4c410599df539085 100644
--- a/src/main/scala/leon/synthesis/rules/CaseSplit.scala
+++ b/src/main/scala/leon/synthesis/rules/CaseSplit.scala
@@ -6,7 +6,7 @@ import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
 
-case object CaseSplit extends Rule("Case-Split", 200) {
+case object CaseSplit extends Rule("Case-Split") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     p.phi match {
       case Or(os) =>
diff --git a/src/main/scala/leon/synthesis/rules/Cegis.scala b/src/main/scala/leon/synthesis/rules/Cegis.scala
index c2ab7c2532d824f7f8815f87ba07c80cf34bf221..93898bcc81cc390c4e1aeb24b7e74ecce134a23c 100644
--- a/src/main/scala/leon/synthesis/rules/Cegis.scala
+++ b/src/main/scala/leon/synthesis/rules/Cegis.scala
@@ -11,7 +11,7 @@ import purescala.Extractors._
 
 import solvers.z3.FairZ3Solver
 
-case object CEGIS extends Rule("CEGIS", 150) {
+case object CEGIS extends Rule("CEGIS") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     case class Generator(tpe: TypeTree, altBuilder: () => List[(Expr, Set[Identifier])]);
 
diff --git a/src/main/scala/leon/synthesis/rules/Disunification.scala b/src/main/scala/leon/synthesis/rules/Disunification.scala
index 53963b5024792c4a5a1e393bc2ad0b865008343b..9ca48a9f62eb4c9e9aab867555f3ba039bbf939c 100644
--- a/src/main/scala/leon/synthesis/rules/Disunification.scala
+++ b/src/main/scala/leon/synthesis/rules/Disunification.scala
@@ -8,7 +8,7 @@ import purescala.TreeOps._
 import purescala.Extractors._
 
 object Disunification {
-  case object Decomp extends Rule("Disunif. Decomp.", 200) {
+  case object Decomp extends Rule("Disunif. Decomp.") {
     def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
       val TopLevelAnds(exprs) = p.phi
 
diff --git a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
index eebab17e91365a444cb322bc433ce5cc163eec25..bad8bc4c45a0430595499156eeb2a61c80615d6d 100644
--- a/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
+++ b/src/main/scala/leon/synthesis/rules/EqualitySplit.scala
@@ -8,7 +8,7 @@ import purescala.TypeTrees._
 import purescala.TreeOps._
 import purescala.Extractors._
 
-case object EqualitySplit extends Rule("Eq. Split.", 90) {
+case object EqualitySplit extends Rule("Eq. Split.") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val candidates = p.as.groupBy(_.getType).map(_._2.toList).filter {
       case List(a1, a2) =>
diff --git a/src/main/scala/leon/synthesis/rules/Ground.scala b/src/main/scala/leon/synthesis/rules/Ground.scala
index 97c0c836604cfc80a6dbd3fd2db205a4c58cedec..6aefe88a8ca64b76fda97f012a3a7c322f6d8507 100644
--- a/src/main/scala/leon/synthesis/rules/Ground.scala
+++ b/src/main/scala/leon/synthesis/rules/Ground.scala
@@ -7,7 +7,7 @@ import purescala.TypeTrees._
 import purescala.TreeOps._
 import purescala.Extractors._
 
-case object Ground extends Rule("Ground", 500) {
+case object Ground extends Rule("Ground") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     if (p.as.isEmpty) {
 
diff --git a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
index 00d21c6040579704cec09ad16cacb883f7e58bca..eabbfce2e984e913c92dc01b4169a29ed574be78 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerEquation.scala
@@ -11,7 +11,7 @@ import purescala.TypeTrees._
 import purescala.Definitions._
 import LinearEquations.elimVariable
 
-case object IntegerEquation extends Rule("Integer Equation", 600) {
+case object IntegerEquation extends Rule("Integer Equation") {
   def instantiateOn(sctx: SynthesisContext, problem: Problem): Traversable[RuleInstantiation] = if(!problem.xs.exists(_.getType == Int32Type)) Nil else {
 
     val TopLevelAnds(exprs) = problem.phi
diff --git a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
index 7cb6b28cb374f0480c316fa0329b02374f0ed12d..21f9dced181fb1d55161fb6db1600da6230fc8d8 100644
--- a/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
+++ b/src/main/scala/leon/synthesis/rules/IntegerInequalities.scala
@@ -12,7 +12,7 @@ import purescala.Definitions._
 import LinearEquations.elimVariable
 import leon.synthesis.Algebra.lcm
 
-case object IntegerInequalities extends Rule("Integer Inequalities", 600) {
+case object IntegerInequalities extends Rule("Integer Inequalities") {
   def instantiateOn(sctx: SynthesisContext, problem: Problem): Traversable[RuleInstantiation] = {
     val TopLevelAnds(exprs) = problem.phi
 
diff --git a/src/main/scala/leon/synthesis/rules/OnePoint.scala b/src/main/scala/leon/synthesis/rules/OnePoint.scala
index 76aedbdc5216c5a84f735bf705950f1caa24b4da..24eee3336a644b4298ac0fc6107448761db5b537 100644
--- a/src/main/scala/leon/synthesis/rules/OnePoint.scala
+++ b/src/main/scala/leon/synthesis/rules/OnePoint.scala
@@ -6,7 +6,7 @@ import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
 
-case object OnePoint extends Rule("One-point", 300) {
+case object OnePoint extends Rule("One-point") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val TopLevelAnds(exprs) = p.phi
 
diff --git a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
index 0ddce7824f8c403a2504ae866dfcc4927b89663d..460a83fe4f9771fb4a4982df4956d5db2ef6889e 100644
--- a/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
+++ b/src/main/scala/leon/synthesis/rules/OptimisticGround.scala
@@ -7,7 +7,7 @@ import purescala.TypeTrees._
 import purescala.TreeOps._
 import purescala.Extractors._
 
-case object OptimisticGround extends Rule("Optimistic Ground", 150) {
+case object OptimisticGround extends Rule("Optimistic Ground") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     if (!p.as.isEmpty && !p.xs.isEmpty) {
       val xss = p.xs.toSet
diff --git a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
index 808a76dd841cafb89444e94012c383b8437c2f87..7c8d2de15faa8ab3ff577dfc56a4c528f5ec654c 100644
--- a/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnconstrainedOutput.scala
@@ -6,7 +6,7 @@ import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
 
-case object UnconstrainedOutput extends Rule("Unconstr.Output", 100) {
+case object UnconstrainedOutput extends Rule("Unconstr.Output") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val unconstr = p.xs.toSet -- variablesOf(p.phi)
 
diff --git a/src/main/scala/leon/synthesis/rules/Unification.scala b/src/main/scala/leon/synthesis/rules/Unification.scala
index fd278ff24b40852d6e6101419cd99a65360d83ee..5c81516197a52b250611c9aad044c39eb1f49898 100644
--- a/src/main/scala/leon/synthesis/rules/Unification.scala
+++ b/src/main/scala/leon/synthesis/rules/Unification.scala
@@ -8,7 +8,7 @@ import purescala.TreeOps._
 import purescala.Extractors._
 
 object Unification {
-  case object DecompTrivialClash extends Rule("Unif Dec./Clash/Triv.", 200) {
+  case object DecompTrivialClash extends Rule("Unif Dec./Clash/Triv.") {
     def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
       val TopLevelAnds(exprs) = p.phi
 
@@ -36,7 +36,7 @@ object Unification {
 
   // This rule is probably useless; it never happens except in crafted
   // examples, and will be found by OptimisticGround anyway.
-  case object OccursCheck extends Rule("Unif OccursCheck", 200) {
+  case object OccursCheck extends Rule("Unif OccursCheck") {
     def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
       val TopLevelAnds(exprs) = p.phi
 
diff --git a/src/main/scala/leon/synthesis/rules/UnusedInput.scala b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
index d9b26efed9783b6c95f49d1477c7129ce1fe455e..13ba585abf24ec06d6d07b43405f55435571f48d 100644
--- a/src/main/scala/leon/synthesis/rules/UnusedInput.scala
+++ b/src/main/scala/leon/synthesis/rules/UnusedInput.scala
@@ -6,7 +6,7 @@ import purescala.Trees._
 import purescala.TreeOps._
 import purescala.Extractors._
 
-case object UnusedInput extends Rule("UnusedInput", 100) {
+case object UnusedInput extends Rule("UnusedInput") {
   def instantiateOn(sctx: SynthesisContext, p: Problem): Traversable[RuleInstantiation] = {
     val unused = p.as.toSet -- variablesOf(p.phi) -- variablesOf(p.pc)