message: smt peephole: a \/ ~a -> true
diff: @@ -1206,30 +1206,23 @@ expr expr::operator||(const expr &rhs) const {
  if (rhs.isTrue() || isFalse())
  return rhs;
  + expr n;
  + if ((isNot(n) && n.eq(rhs)) ||
  + (rhs.isNot(n) && eq(n)))
  + return true;
  +
  C(rhs);
  Z3_ast args[] = { ast(), rhs() };
  return Z3_mk_or(ctx(), 2, args);
  }
  void expr::operator&=(const expr &rhs) {
  - if (!isValid() || eq(rhs) || isFalse() || rhs.isTrue()) {
  - // do nothing
  - } else if (!rhs.isValid() || rhs.isFalse() || isTrue()) {
  - *this = rhs;
  - } else {
  *this = *this && rhs;
  }
  -}
  void expr::operator|=(const expr &rhs) {
  - if (!isValid() || eq(rhs) || rhs.isFalse() || isTrue()) {
  - // do nothing
  - } else if (!rhs.isValid() || isFalse() || rhs.isTrue()) {
  - *this = rhs;
  - } else {
  *this = *this || rhs;
  }
  -}
  expr expr::mk_and(const set<expr> &vals) {
  expr ret(true);
  