let rec merge p e =   
  assert(Fact.Equal.is_var e);
  let e = Fact.Equal.map (find p) e in        (* get canonical forms *)
    assert(Fact.Equal.both_sides (is_canonical p) e);  
    merge1 p e
          
and merge1 p e =
  let x, y, _ = e in
    if Term.eq x y then () else 
      let (d', ds') = D.merge e p.d in 
        p.d <- d'; 
        V.merge e p.v;
        p.equal <- e :: p.equal;
        p.diseq <- Fact.Diseq.Set.union ds' p.diseq 



(** Create a fresh variable that is smaller than x and y according to variable ordering Var.cmp and which incorporates the intersection of the domains of x and y. *)


and create_fresh_var d x y =
  match Term.Var.is_slack x, Term.Var.is_slack y with
    | false, false -> 
        Term.Var.mk_rename (Name.of_string "w") None (Var.Cnstrnt.Real(d))
    | _ ->
        if Term.Var.is_zero_slack x || Term.Var.is_zero_slack y then
          Term.Var.mk_slack None Var.Zero
        else 
          Term.Var.mk_slack None (Var.Nonneg(d))