message: smt expr: fold a + b == rhs -> false when applicable
diff: @@ -1189,6 +1189,8 @@ expr expr::cmp_eq(const expr &rhs, bool simplify) const {
  return false;
  return rhs == *this;
  }
  + // constants on rhs from now.
  +
  if (rhs.isTrue())
  return *this;
  if (rhs.isFalse())
  @@ -1215,6 +1217,7 @@ expr expr::cmp_eq(const expr &rhs, bool simplify) const {
  if (auto app = isAppOf(Z3_OP_CONCAT)) {
  unsigned num_args = Z3_get_app_num_args(ctx(), app);
  + // (concat x y) == const -> x == const[..] /\ y == const[..]
  if (rhs.isConst()) {
  AndExpr eqs;
  unsigned high = bits();
  @@ -1227,6 +1230,7 @@ expr expr::cmp_eq(const expr &rhs, bool simplify) const {
  return eqs();
  }
  + // (concat ..) == (concat ..)
  if (auto app_rhs = rhs.isAppOf(Z3_OP_CONCAT);
  app_rhs != nullptr &&
  num_args == Z3_get_app_num_args(ctx(), app_rhs)) {
  @@ -1287,6 +1291,18 @@ expr expr::cmp_eq(const expr &rhs, bool simplify) const {
  }
  }
  + {
  + expr a, b;
  + if (isAdd(a, b)) {
  + // Pre: a >= 0, b >= 0, rhs u< b
  + // a + b == rhs -> false
  + if (a.isNegative().isFalse() &&
  + b.isNegative().isFalse() &&
  + (rhs.ult(a).isTrue() || rhs.ult(b).isTrue()))
  + return false;
  + }
  + }
  +
  // (a u% b) == c -> false if c u>= b
  {
  expr a, b;
  