diff --git a/examples/flatzinc/calvin_puzzle.fzn b/examples/flatzinc/calvin_puzzle.fzn
index b3280ba642..eea870020e 100644
--- a/examples/flatzinc/calvin_puzzle.fzn
+++ b/examples/flatzinc/calvin_puzzle.fzn
@@ -1378,4 +1378,5 @@ constraint set_in(b____00584, {-3, -2, 0, 2, 3});
 constraint set_in(b____00613, {-3, -2, 0, 2, 3});
 constraint set_in(b____00642, {-3, -2, 0, 2, 3});
 constraint set_in(b____00671, {-3, -2, 0, 2, 3});
+constraint int_eq(x[1], 1);
 solve  :: int_search([x[1], x[2], x[3], x[4], x[5], x[6], x[7], x[8], x[9], x[10], x[11], x[12], x[13], x[14], x[15], x[16], x[17], x[18], x[19], x[20], x[21], x[22], x[23], x[24], x[25]], occurrence, indomain_median, complete) satisfy;
diff --git a/src/constraint_solver/element.cc b/src/constraint_solver/element.cc
index a3e2252dec..ba8a41f444 100644
--- a/src/constraint_solver/element.cc
+++ b/src/constraint_solver/element.cc
@@ -1266,7 +1266,7 @@ class IntExprArrayElementCstCt : public Constraint {
   std::vector<Demon*> demons_;
 };
 
-// This constraint implements vars[index] == constant.
+// This constraint implements index == position(constant in vars).
 
 class IntExprArrayPositionCt : public Constraint {
  public:
diff --git a/src/constraint_solver/expr_array.cc b/src/constraint_solver/expr_array.cc
index 014627cea3..500378ba32 100644
--- a/src/constraint_solver/expr_array.cc
+++ b/src/constraint_solver/expr_array.cc
@@ -2388,7 +2388,7 @@ Constraint* MakeScalProdGreaterOrEqualFct(Solver* solver,
   for (int i = 0; i < size; ++i) {
     terms.push_back(solver->MakeProd(vars[i], coefficients[i])->Var());
   }
-  return solver->MakeGreaterOrEqual(solver->MakeSum(terms), cst);
+  return solver->MakeSumGreaterOrEqual(terms, cst);
 }
 }  // namespace
 
diff --git a/src/constraint_solver/search.cc b/src/constraint_solver/search.cc
index d05dcbde2e..82385b8f8b 100644
--- a/src/constraint_solver/search.cc
+++ b/src/constraint_solver/search.cc
@@ -1287,12 +1287,12 @@ int64 CenterValueSelector::Select(const IntVar* const v, int64 id) {
   }
   const int64 diameter = vmax - mid;  // always greater than mid - vmix.
   for (int64 i = 1; i <= diameter; ++i) {
-    if (v->Contains(mid + i)) {
-      return mid + i;
-    }
     if (v->Contains(mid - i)) {
       return mid - i;
     }
+    if (v->Contains(mid + i)) {
+      return mid + i;
+    }
   }
   return 0LL;
 }
diff --git a/src/flatzinc/flatzinc.cc b/src/flatzinc/flatzinc.cc
index 8ea4f30b85..5aa47efacf 100644
--- a/src/flatzinc/flatzinc.cc
+++ b/src/flatzinc/flatzinc.cc
@@ -302,16 +302,16 @@ void FlatZincModel::CreateDecisionBuilders(bool ignore_unknown,
   } else {
     free_search_ = true;
   }
-  builders_.push_back(solver_.MakePhase(active_variables_,
-                                        Solver::CHOOSE_FIRST_UNBOUND,
-                                        Solver::ASSIGN_MIN_VALUE));
-  VLOG(1) << "Decision builder = " << builders_.back()->DebugString();
-  if (!introduced_variables_.empty()) {
-    builders_.push_back(solver_.MakePhase(introduced_variables_,
-                                          Solver::CHOOSE_FIRST_UNBOUND,
-                                          Solver::ASSIGN_MIN_VALUE));
-    VLOG(1) << "Decision builder = " << builders_.back()->DebugString();
-  }
+  // builders_.push_back(solver_.MakePhase(active_variables_,
+  //                                       Solver::CHOOSE_FIRST_UNBOUND,
+  //                                       Solver::ASSIGN_MIN_VALUE));
+  // VLOG(1) << "Decision builder = " << builders_.back()->DebugString();
+  // if (!introduced_variables_.empty()) {
+  //   builders_.push_back(solver_.MakePhase(introduced_variables_,
+  //                                         Solver::CHOOSE_FIRST_UNBOUND,
+  //                                         Solver::ASSIGN_MIN_VALUE));
+  //   VLOG(1) << "Decision builder = " << builders_.back()->DebugString();
+  // }
 }
 
 void FlatZincModel::Satisfy(AST::Array* const annotations) {
diff --git a/src/flatzinc/parser.cc b/src/flatzinc/parser.cc
index 141010840f..e2a823a924 100644
--- a/src/flatzinc/parser.cc
+++ b/src/flatzinc/parser.cc
@@ -72,11 +72,7 @@ int ParserState::FindTarget(AST::Node* const annotations) const {
       if (ann_array->a[0]->isCall("defines_var")) {
         AST::Call* const call = ann_array->a[0]->getCall();
         AST::Node* const args = call->args;
-        if (args->isIntVar()) {
-          return args->getIntVar();
-        } else if (args->isBoolVar()) {
-          return int_variables_.size() + args->getBoolVar();
-        }
+        return VarIndex(args);
       }
     }
   }
@@ -97,13 +93,8 @@ void ParserState::CollectRequired(AST::Array* const args,
     AST::Node* const node = args->a[i];
     if (node->isArray()) {
       CollectRequired(node->getArray(), candidates, require);
-    } else if (node->isIntVar()) {
-      const int req = node->getIntVar();
-      if (ContainsKey(candidates, req)) {
-        require->insert(req);
-      }
-    } else if (node->isBoolVar()) {
-      const int req = node->getBoolVar() + int_variables_.size();
+    } else if (node->isIntVar() || node->isBoolVar()) {
+      const int req = VarIndex(node);
       if (ContainsKey(candidates, req)) {
         require->insert(req);
       }
@@ -142,15 +133,16 @@ void ParserState::ComputeViableTarget(
     // Defines a bool var.
     const int bool_define = FindTarget(spec->annotations());
     if (bool_define != CtSpec::kNoDefinition) {
-      CHECK(bool_variables_[bool_define - int_variables_.size()]->introduced);
+      CHECK(bool_variables_[BoolFromVarIndex(bool_define)]->introduced);
       candidates->insert(bool_define);
       VLOG(2) << id << " -> insert " << bool_define;
     }
   } else if (id == "int2int") {
-    candidates->insert(spec->Arg(1)->getIntVar());
-    VLOG(2) << id << " -> insert " << spec->Arg(1)->getIntVar();
+    const int int_define = VarIndex(spec->Arg(1));
+    candidates->insert(int_define);
+    VLOG(2) << id << " -> insert " << int_define;
   } else if (id == "bool2bool") {
-    const int bool_define = spec->Arg(1)->getBoolVar() + int_variables_.size();
+    const int bool_define = VarIndex(spec->Arg(1));
     candidates->insert(bool_define);
     VLOG(2) << id << " -> insert " << bool_define;
   }
@@ -198,15 +190,28 @@ void MarkComputedVariables(CtSpec* const spec, hash_set<int>* const computed) {
   }
 }
 
+void ParserState::Sanitize(CtSpec* const spec) {
+  if (spec->Id() == "int_lin_eq" && StrongPropagation(spec->annotations())) {
+    VLOG(1) << "## Presolve ## Remove defines part on " << spec->DebugString();
+    // Remove defines_var part.
+    spec->RemoveDefines();
+  }
+}
+
 void ParserState::CreateModel() {
   hash_set<int> candidates;
   hash_set<int> computed_variables;
 
-  // Find orphans (is_defined && not a target).
+  // Sanity.
+  for (int i = 0; i < constraints_.size(); ++i) {
+    Sanitize(constraints_[i]);
+  }
+  // Find orphans (is_defined && not a viable target).
   hash_set<int> targets;
   for (int i = 0; i < constraints_.size(); ++i) {
     const int target = FindTarget(constraints_[i]->annotations());
     if (target != CtSpec::kNoDefinition) {
+      VLOG(1) << "## Presolve ## Mark xi(" << target << ") as defined";
       targets.insert(target);
     }
   }
@@ -214,6 +219,7 @@ void ParserState::CreateModel() {
     IntVarSpec* const spec = int_variables_[i];
     if (spec->introduced && !ContainsKey(targets, i)) {
       orphans_.insert(i);
+      VLOG(1) << "## Presolve ## Mark xi(" << i << ") as orphan";
     }
   }
 
@@ -226,7 +232,7 @@ void ParserState::CreateModel() {
       if (spec->Nullified()) {
         continue;
       }
-      if (Propagate(spec)) {
+      if (Presolve(spec)) {
         repeat = true;
       }
     }
@@ -258,7 +264,7 @@ void ParserState::CreateModel() {
                                           "bool2bool",
                                           args,
                                           NULL);
-      alias_ct->set_defines(i + int_variables_.size());
+      alias_ct->set_defines(VarIndex(args->a[1]));
       constraints_.push_back(alias_ct);
     }
   }
@@ -452,13 +458,16 @@ void ParserState::CreateModel() {
   for (unsigned int i = int_domain_constraints_.size(); i--;) {
     if (!hadError) {
       const int var_id = int_domain_constraints_[i].first;
+      IntVar* const var = model_->IntegerVariable(var_id);
       AST::SetLit* const dom = int_domain_constraints_[i].second;
-      VLOG(1) << "Reduce integer variable " << var_id
-              << " to " << dom->DebugString();
-      if (dom->interval) {
-        model_->IntegerVariable(var_id)->SetRange(dom->min, dom->max);
-      } else {
-        model_->IntegerVariable(var_id)->SetValues(dom->s);
+      if (dom->interval && (dom->min > var->Min() || dom->max < var->Max())) {
+        VLOG(1) << "Reduce integer variable " << var_id
+                << " to " << dom->DebugString();
+        var->SetRange(dom->min, dom->max);
+      } else if (!dom->interval) {
+        VLOG(1) << "Reduce integer variable " << var_id
+                << " to " << dom->DebugString();
+        var->SetValues(dom->s);
       }
     }
   }
@@ -553,21 +562,11 @@ int ParserState::FindEndIntegerVariable(int index) {
   return index;
 }
 
-bool ParserState::IsReifTrue(CtSpec* const spec) const {
-  AST::Node* const node = spec->LastArg();
-  if (node->isBool() && node->getBool() == 1) {
-    return true;
-  }
-  if (node->isBoolVar()) {
-    const int boolvar = node->getBoolVar();
-    return bool_variables_[boolvar]->IsTrue();
-  }
-  return false;
-}
-
 bool ParserState::IsBound(AST::Node* const node) const {
   return node->isInt() ||
-      (node->isIntVar() && int_variables_[node->getIntVar()]->IsBound());
+      (node->isIntVar() && int_variables_[node->getIntVar()]->IsBound()) ||
+      node->isBool() ||
+      (node->isBoolVar() && bool_variables_[node->getBoolVar()]->IsBound());
 }
 
 int ParserState::GetBound(AST::Node* const node) const {
@@ -577,10 +576,16 @@ int ParserState::GetBound(AST::Node* const node) const {
   if (node->isIntVar()) {
     return int_variables_[node->getIntVar()]->GetBound();
   }
+  if (node->isBool()) {
+    return node->getBool();
+  }
+  if (node->isBoolVar()) {
+    return bool_variables_[node->getBoolVar()]->GetBound();
+  }
   return 0;
 }
 
-bool ParserState::AllDifferent(AST::Node* const node) const {
+bool ParserState::IsAllDifferent(AST::Node* const node) const {
   AST::Array* const array_variables = node->getArray();
   const int size = array_variables->a.size();
   std::vector<int> variables(size);
@@ -614,10 +619,10 @@ bool ParserState::AllDifferent(AST::Node* const node) const {
   return false;
 }
 
-bool ParserState::Propagate(CtSpec* const spec) {
+bool ParserState::Presolve(CtSpec* const spec) {
   const string& id = spec->Id();
   const int index = spec->Index();
-  if (id == "int_le" || (id == "int_le_reif" && IsReifTrue(spec))) {
+  if (id == "int_le") {
     if (spec->Arg(0)->isIntVar() && IsBound(spec->Arg(1))) {
       IntVarSpec* const var_spec =
           int_variables_[FindEndIntegerVariable(spec->Arg(0)->getIntVar())];
@@ -642,7 +647,7 @@ bool ParserState::Propagate(CtSpec* const spec) {
       return ok;
     }
   }
-  if (id == "int_eq" || (id == "int_eq_reif" && IsReifTrue(spec))) {
+  if (id == "int_eq") {
     if (spec->Arg(0)->isIntVar() && IsBound(spec->Arg(1))) {
       IntVarSpec* const var_spec =
           int_variables_[FindEndIntegerVariable(spec->Arg(0)->getIntVar())];
@@ -668,30 +673,34 @@ bool ParserState::Propagate(CtSpec* const spec) {
     } else if (spec->Arg(0)->isIntVar() &&
                spec->Arg(1)->isIntVar() &&
                spec->annotations() == NULL &&
+               !ContainsKey(stored_constraints_, index) &&
                (ContainsKey(orphans_, spec->Arg(0)->getIntVar()) ||
                 ContainsKey(orphans_, spec->Arg(1)->getIntVar()))) {
+      stored_constraints_.insert(index);
       const int var0 = spec->Arg(0)->getIntVar();
       const int var1 = spec->Arg(1)->getIntVar();
-      if (ContainsKey(orphans_, var0) && !ContainsKey(orphans_, var1)) {
+      if (ContainsKey(orphans_, var0)) {
         IntVarSpec* const spec0 = int_variables_[FindEndIntegerVariable(var0)];
         AST::Call* const call =
             new AST::Call("defines_var", new AST::IntVar(var0));
         spec->AddAnnotation(call);
         VLOG(1) << "## Presolve ##  Aliasing xi(" << var0 << ") to xi("
                 << var1 << ")";
+        orphans_.erase(var0);
         return true;
-      } else if (!ContainsKey(orphans_, var0) && ContainsKey(orphans_, var1)) {
+      } else if (ContainsKey(orphans_, var1)) {
         IntVarSpec* const spec1 = int_variables_[FindEndIntegerVariable(var1)];
         AST::Call* const call =
             new AST::Call("defines_var", new AST::IntVar(var1));
         spec->AddAnnotation(call);
         VLOG(1) << "## Presolve ##  Aliasing xi(" << var1 << ") to xi("
                 << var0 << ")";
+        orphans_.erase(var1);
         return true;
       }
     }
   }
-  if (id == "set_in" || (id == "set_in_reif" && IsReifTrue(spec))) {
+  if (id == "set_in") {
     if (spec->Arg(0)->isIntVar() && spec->Arg(1)->isSet()) {
       IntVarSpec* const var_spec =
           int_variables_[FindEndIntegerVariable(spec->Arg(0)->getIntVar())];
@@ -710,7 +719,9 @@ bool ParserState::Propagate(CtSpec* const spec) {
       return ok;
     }
   }
-  if (id == "array_bool_and" && IsReifTrue(spec)) {
+  if (id == "array_bool_and" &&
+      IsBound(spec->Arg(1)) &&
+      GetBound(spec->Arg(1)) == 1) {
     VLOG(1) << "## Presolve ##  Forcing array_bool_and to 1 on "
             << spec->DebugString();
     AST::Array* const array_variables = spec->Arg(0)->getArray();
@@ -724,7 +735,9 @@ bool ParserState::Propagate(CtSpec* const spec) {
     spec->Nullify();
     return true;
   }
-  if (id.find("_reif") != string::npos && IsReifTrue(spec)) {
+  if (id.find("_reif") != string::npos &&
+      IsBound(spec->LastArg()) &&
+      GetBound(spec->LastArg()) == 1) {
     VLOG(1) << "## Presolve ##  Unreify " << spec->DebugString();
     spec->Unreify();
     return true;
@@ -749,7 +762,7 @@ bool ParserState::Propagate(CtSpec* const spec) {
   }
   if (id == "array_var_int_element" &&
       IsBound(spec->Arg(2)) &&
-      AllDifferent(spec->Arg(1))) {
+      IsAllDifferent(spec->Arg(1))) {
     VLOG(1) << "## Presolve ##  Reinforce " << spec->DebugString()
             << " to array_var_int_position";
     spec->SetId("array_var_int_position");
@@ -757,10 +770,6 @@ bool ParserState::Propagate(CtSpec* const spec) {
     spec->ReplaceArg(2, new AST::IntLit(bound));
     return true;
   }
-  if (id == "array_var_int_position" &&
-      !ContainsKey(stored_constraints_, index)) {
-
-  }
   return false;
 }
 
diff --git a/src/flatzinc/parser.h b/src/flatzinc/parser.h
index dfe4308f98..373bf71d4a 100644
--- a/src/flatzinc/parser.h
+++ b/src/flatzinc/parser.h
@@ -161,16 +161,29 @@ class ParserState {
                      AST::Node* const annotations);
   void InitModel();
   void FillOutput(operations_research::FlatZincModel& m);
-  bool Propagate(CtSpec* const spec);
-  bool IsReifTrue(CtSpec* const spec) const;
+  bool Presolve(CtSpec* const spec);
   bool IsBound(AST::Node* const node) const;
   int GetBound(AST::Node* const node) const;
-  bool AllDifferent(AST::Node* const node) const;
+  bool IsAllDifferent(AST::Node* const node) const;
 
   FlatZincModel* model() const {
     return model_;
   }
 
+  int VarIndex(AST::Node* const node) const {
+    if (node->isIntVar()) {
+      return node->getIntVar();
+    } else if (node->isBoolVar()) {
+      return node->getBoolVar() + int_variables_.size();
+    } else {
+      return -1;
+    }
+  }
+
+  int BoolFromVarIndex(int index) const {
+    return index - int_variables_.size();
+  }
+
  private:
 
   int FindEndIntegerVariable(int index);
@@ -182,6 +195,7 @@ class ParserState {
                            CtSpec* const spec) const;
   void ComputeViableTarget(CtSpec* const spec,
                            hash_set<int>* const candidates) const;
+  void Sanitize(CtSpec* const spec);
 
   operations_research::FlatZincModel* model_;
   std::vector<std::pair<std::string,AST::Node*> > output_;
diff --git a/src/flatzinc/registry.cc b/src/flatzinc/registry.cc
index 52c9dd3637..d8f9dcf54b 100644
--- a/src/flatzinc/registry.cc
+++ b/src/flatzinc/registry.cc
@@ -116,14 +116,14 @@ void p_int_eq(FlatZincModel* const model, CtSpec* const spec) {
   if (spec->Arg(0)->isIntVar() &&
       spec->defines() == spec->Arg(0)->getIntVar()) {
     IntVar* const right = model->GetIntVar(spec->Arg(1));
-    VLOG(1) << "  - creating " << spec->Arg(0)->DebugString() << " == "
+    VLOG(1) << "  - creating " << spec->Arg(0)->DebugString() << " := "
             << right->DebugString();
     CHECK(model->IntegerVariable(spec->Arg(0)->getIntVar()) == NULL);
     model->SetIntegerVariable(spec->Arg(0)->getIntVar(), right);
   } else if (spec->Arg(1)->isIntVar() &&
       spec->defines() == spec->Arg(1)->getIntVar()) {
     IntVar* const left = model->GetIntVar(spec->Arg(0));
-    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " == "
+    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " := "
             << left->DebugString();
     CHECK(model->IntegerVariable(spec->Arg(1)->getIntVar()) == NULL);
     model->SetIntegerVariable(spec->Arg(1)->getIntVar(), left);
@@ -193,8 +193,8 @@ void p_int_eq_reif(FlatZincModel* const model, CtSpec* const spec) {
         node_right->isInt() ?
         solver->MakeIsEqualCstVar(left, node_right->getInt()) :
         solver->MakeIsEqualVar(left, model->GetIntVar(node_right));
-    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " -> "
-            << boolvar->DebugString();;
+    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
+            << boolvar->DebugString();
     CHECK(model->BooleanVariable(node_boolvar->getBoolVar()) == NULL);
     model->SetBooleanVariable(node_boolvar->getBoolVar(), boolvar);
     CHECK_NOTNULL(boolvar);
@@ -215,8 +215,8 @@ void p_int_ne_reif(FlatZincModel* const model, CtSpec* const spec) {
   if (node_boolvar->isBoolVar() &&
       node_boolvar->getBoolVar() + model->IntVarCount() == spec->defines()) {
     IntVar* const boolvar = solver->MakeIsDifferentVar(left, right);
-    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " -> "
-            << boolvar->DebugString();;
+    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
+            << boolvar->DebugString();
     CHECK(model->BooleanVariable(node_boolvar->getBoolVar()) == NULL);
     model->SetBooleanVariable(node_boolvar->getBoolVar(), boolvar);
     CHECK_NOTNULL(boolvar);
@@ -308,7 +308,7 @@ void p_int_lin_eq(FlatZincModel* const model, CtSpec* const spec) {
     }
     IntVar* const target =
         solver->MakeScalProd(variables, coefficients)->Var();
-    VLOG(1) << "  - creating xi(" << spec->defines() << ") -> "
+    VLOG(1) << "  - creating xi(" << spec->defines() << ") := "
             << target->DebugString();
     CHECK(model->IntegerVariable(spec->defines()) == NULL);
     model->SetIntegerVariable(spec->defines(), target);
@@ -348,8 +348,8 @@ void p_int_lin_eq_reif(FlatZincModel* const model, CtSpec* const spec) {
   if (node_boolvar->isBoolVar() &&
       node_boolvar->getBoolVar() + model->IntVarCount() == spec->defines()) {
     IntVar* const boolvar = solver->MakeIsEqualCstVar(var, rhs);
-    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " -> "
-            << boolvar->DebugString();;
+    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
+            << boolvar->DebugString();
     CHECK(model->BooleanVariable(node_boolvar->getBoolVar()) == NULL);
     model->SetBooleanVariable(node_boolvar->getBoolVar(), boolvar);
   } else {
@@ -610,7 +610,7 @@ void p_int_plus(FlatZincModel* const model, CtSpec* const spec) {
     IntVar* const right = model->GetIntVar(spec->Arg(1));
     IntVar* const target = model->GetIntVar(spec->Arg(2));
     IntVar* const left = solver->MakeDifference(target, right)->Var();
-    VLOG(1) << "  - creating " << spec->Arg(0)->DebugString() << " == "
+    VLOG(1) << "  - creating " << spec->Arg(0)->DebugString() << " := "
             << left->DebugString();
     CHECK(model->IntegerVariable(spec->Arg(0)->getIntVar()) == NULL);
     model->SetIntegerVariable(spec->Arg(0)->getIntVar(), left);
@@ -619,7 +619,7 @@ void p_int_plus(FlatZincModel* const model, CtSpec* const spec) {
     IntVar* const left = model->GetIntVar(spec->Arg(0));
     IntVar* const target = model->GetIntVar(spec->Arg(2));
     IntVar* const right = solver->MakeDifference(target, left)->Var();
-    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " == "
+    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " := "
             << right->DebugString();
     CHECK(model->IntegerVariable(spec->Arg(1)->getIntVar()) == NULL);
     model->SetIntegerVariable(spec->Arg(1)->getIntVar(), right);
@@ -628,7 +628,7 @@ void p_int_plus(FlatZincModel* const model, CtSpec* const spec) {
     IntVar* const left = model->GetIntVar(spec->Arg(0));
     IntVar* const right = model->GetIntVar(spec->Arg(1));
     IntVar* const target = solver->MakeSum(left, right)->Var();
-    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " == "
+    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
             << target->DebugString();
     CHECK(model->IntegerVariable(spec->Arg(2)->getIntVar()) == NULL);
     model->SetIntegerVariable(spec->Arg(2)->getIntVar(), target);
@@ -650,7 +650,7 @@ void p_int_minus(FlatZincModel* const model, CtSpec* const spec) {
   if (spec->Arg(2)->isIntVar() &&
       spec->defines() == spec->Arg(2)->getIntVar()) {
     IntVar* const target = solver->MakeDifference(left, right)->Var();
-    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " -> "
+    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
             << target->DebugString();
     CHECK(model->IntegerVariable(spec->Arg(2)->getIntVar()) == NULL);
     model->SetIntegerVariable(spec->Arg(2)->getIntVar(), target);
@@ -671,7 +671,7 @@ void p_int_times(FlatZincModel* const model, CtSpec* const spec) {
   if (spec->Arg(2)->isIntVar() &&
       spec->defines() == spec->Arg(2)->getIntVar()) {
     IntVar* const target = solver->MakeProd(left, right)->Var();
-    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " -> "
+    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
             << target->DebugString();
     CHECK(model->IntegerVariable(spec->Arg(2)->getIntVar()) == NULL);
     model->SetIntegerVariable(spec->Arg(2)->getIntVar(), target);
@@ -728,7 +728,7 @@ void p_int_min(FlatZincModel* const model, CtSpec* const spec) {
   if (spec->Arg(2)->isIntVar() &&
       spec->defines() == spec->Arg(2)->getIntVar()) {
     IntVar* const target = solver->MakeMin(left, right)->Var();
-    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " -> "
+    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
             << target->DebugString();
     CHECK(model->IntegerVariable(spec->Arg(2)->getIntVar()) == NULL);
     model->SetIntegerVariable(spec->Arg(2)->getIntVar(), target);
@@ -748,7 +748,7 @@ void p_int_max(FlatZincModel* const model, CtSpec* const spec) {
   if (spec->Arg(2)->isIntVar() &&
       spec->defines() == spec->Arg(2)->getIntVar()) {
     IntVar* const target = solver->MakeMax(left, right)->Var();
-    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " -> "
+    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
             << target->DebugString();
     CHECK(model->IntegerVariable(spec->Arg(2)->getIntVar()) == NULL);
     model->SetIntegerVariable(spec->Arg(2)->getIntVar(), target);
@@ -784,7 +784,7 @@ void p_array_bool_and(FlatZincModel* const model, CtSpec* const spec) {
   if (node_boolvar->isBoolVar() &&
       node_boolvar->getBoolVar() + model->IntVarCount() == spec->defines()) {
     IntVar* const boolvar = solver->MakeMin(variables)->Var();
-    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " -> "
+    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
             << boolvar->DebugString();
     CHECK(model->BooleanVariable(node_boolvar->getBoolVar()) == NULL);
     model->SetBooleanVariable(node_boolvar->getBoolVar(), boolvar);
@@ -815,7 +815,7 @@ void p_array_bool_or(FlatZincModel* const model, CtSpec* const spec) {
   if (node_boolvar->isBoolVar() &&
       node_boolvar->getBoolVar() + model->IntVarCount() == spec->defines()) {
     IntVar* const boolvar = solver->MakeMax(variables)->Var();
-    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " -> "
+    VLOG(1) << "  - creating " << node_boolvar->DebugString() << " := "
             << boolvar->DebugString();
     CHECK(model->BooleanVariable(node_boolvar->getBoolVar()) == NULL);
     model->SetBooleanVariable(node_boolvar->getBoolVar(), boolvar);
@@ -904,7 +904,7 @@ void p_array_int_element(FlatZincModel* const model, CtSpec* const spec) {
       spec->defines() == spec->Arg(2)->getIntVar()) {
     IntVar* const target =
         solver->MakeElement(coefficients, shifted_index)->Var();
-    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " -> "
+    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
             << target->DebugString();
     CHECK(model->IntegerVariable(spec->Arg(2)->getIntVar()) == NULL);
     model->SetIntegerVariable(spec->Arg(2)->getIntVar(), target);
@@ -930,7 +930,7 @@ void p_array_var_int_element(FlatZincModel* const model, CtSpec* const spec) {
   if (spec->Arg(2)->isIntVar() &&
       spec->defines() == spec->Arg(2)->getIntVar()) {
     IntVar* const target = solver->MakeElement(variables, shifted_index)->Var();
-    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " -> "
+    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
             << target->DebugString();
     CHECK(model->IntegerVariable(spec->Arg(2)->getIntVar()) == NULL);
     model->SetIntegerVariable(spec->Arg(2)->getIntVar(), target);
@@ -975,7 +975,7 @@ void p_array_bool_element(FlatZincModel* const model, CtSpec* const spec) {
       spec->defines() == spec->Arg(2)->getBoolVar() + model->IntVarCount()) {
     IntVar* const target =
         solver->MakeElement(coefficients, shifted_index)->Var();
-    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " -> "
+    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
             << target->DebugString();
     CHECK(model->BooleanVariable(spec->Arg(2)->getBoolVar()) == NULL);
     model->SetBooleanVariable(spec->Arg(2)->getBoolVar(), target);
@@ -1001,7 +1001,7 @@ void p_array_var_bool_element(FlatZincModel* const model, CtSpec* const spec) {
   if (spec->Arg(2)->isBoolVar() &&
       spec->defines() == spec->Arg(2)->getBoolVar() + model->IntVarCount()) {
     IntVar* const target = solver->MakeElement(variables, shifted_index)->Var();
-    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " -> "
+    VLOG(1) << "  - creating " << spec->Arg(2)->DebugString() << " := "
             << target->DebugString();
     CHECK(model->BooleanVariable(spec->Arg(2)->getBoolVar()) == NULL);
     model->SetBooleanVariable(spec->Arg(2)->getBoolVar(), target);
@@ -1022,7 +1022,7 @@ void p_bool2int(FlatZincModel* const model, CtSpec* const spec) {
   IntVar* const left = model->GetIntVar(spec->Arg(0));
   if (spec->Arg(1)->isIntVar() &&
       spec->defines() == spec->Arg(1)->getIntVar()) {
-    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " -> "
+    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " := "
             << left->DebugString();
     CHECK(model->IntegerVariable(spec->defines()) == NULL);
     model->SetIntegerVariable(spec->defines(), left);
@@ -1040,7 +1040,7 @@ void p_bool2bool(FlatZincModel* const model, CtSpec* const spec) {
   CHECK_NOTNULL(left);
   if (spec->Arg(1)->isBoolVar() &&
       spec->defines() == spec->Arg(1)->getBoolVar() + model->IntVarCount()) {
-    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " -> "
+    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " := "
             << left->DebugString();
     CHECK(model->BooleanVariable(spec->Arg(1)->getBoolVar()) == NULL);
     model->SetBooleanVariable(spec->Arg(1)->getBoolVar(), left);
@@ -1057,7 +1057,7 @@ void p_int2int(FlatZincModel* const model, CtSpec* const spec) {
   IntVar* const left = model->GetIntVar(spec->Arg(0));
   if (spec->Arg(1)->isIntVar() &&
       spec->defines() == spec->Arg(1)->getIntVar()) {
-    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " -> "
+    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " := "
             << left->DebugString();
     CHECK(model->IntegerVariable(spec->defines()) == NULL);
     model->SetIntegerVariable(spec->defines(), left);
@@ -1098,7 +1098,7 @@ void p_abs(FlatZincModel* const model, CtSpec* const spec) {
       spec->defines() == spec->Arg(1)->getIntVar()) {
     CHECK(model->IntegerVariable(spec->defines()) == NULL);
     IntVar* const target = solver->MakeAbs(left)->Var();
-    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " -> "
+    VLOG(1) << "  - creating " << spec->Arg(1)->DebugString() << " := "
             << target->DebugString();
     model->SetIntegerVariable(spec->defines(), target);
   } else {
diff --git a/src/flatzinc/spec.h b/src/flatzinc/spec.h
index bbf549b6c2..d27e5df97d 100644
--- a/src/flatzinc/spec.h
+++ b/src/flatzinc/spec.h
@@ -281,6 +281,15 @@ class BoolVarSpec : public VarSpec {
     return (assigned && i == false);
   }
 
+  bool IsBound() const {
+    return IsTrue() || IsFalse();
+  }
+
+  int GetBound() const {
+    CHECK(IsBound());
+    return IsTrue();
+  }
+
   virtual string DebugString() const {
     if (alias) {
       return StringPrintf(
@@ -517,6 +526,19 @@ class CtSpec {
     }
   }
 
+  void RemoveDefines() {
+    if (annotations_ != NULL) {
+      AST::Array* const ann_array = annotations_->getArray();
+      if (ann_array->a[0]->isCall("defines_var")) {
+        delete ann_array->a[0];
+        for (int i = 0; i < ann_array->a.size() - 1; ++i) {
+          ann_array->a[i] = ann_array->a[i + 1];
+        }
+        ann_array->a.pop_back();
+      }
+    }
+  }
+
  private:
   const int index_;
   std::string id_;