let sub c1 c2 =
    match c1, c2 with
      | _, Unconstrained -> true
      | Real(d1), Real(d2) -> Dom.sub d1 d2
      | Bitvector(n1), Bitvector(n2) -> n1 = n2
      | _ -> false