fix more crashes with invalid SMT exprs
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -158,7 +158,7 @@ expr expr::mkUInt(uint64_t n, Z3_sort sort) {
}
expr expr::mkUInt(uint64_t n, unsigned bits) {
- return mkUInt(n, mkBVSort(bits));
+ return bits ? mkUInt(n, mkBVSort(bits)) : expr();
}
expr expr::mkInt(int64_t n, Z3_sort sort) {
@@ -166,11 +166,11 @@ expr expr::mkInt(int64_t n, Z3_sort sort) {
}
expr expr::mkInt(int64_t n, unsigned bits) {
- return mkInt(n, mkBVSort(bits));
+ return bits ? mkInt(n, mkBVSort(bits)) : expr();
}
expr expr::mkInt(const char *n, unsigned bits) {
- return Z3_mk_numeral(ctx(), n, mkBVSort(bits));
+ return bits ? Z3_mk_numeral(ctx(), n, mkBVSort(bits)) : expr();
}
expr expr::mkConst(Z3_func_decl decl) {
@@ -892,36 +892,6 @@ expr expr::sgt(const expr &rhs) const {
return !sle(rhs);
}
-expr expr::ule(uint64_t rhs) const {
- C();
- return ule(mkUInt(rhs, bits()));
-}
-
-expr expr::ult(uint64_t rhs) const {
- C();
- return ult(mkUInt(rhs, bits()));
-}
-
-expr expr::uge(uint64_t rhs) const {
- C();
- return uge(mkUInt(rhs, bits()));
-}
-
-expr expr::ugt(uint64_t rhs) const {
- C();
- return ugt(mkUInt(rhs, bits()));
-}
-
-expr expr::operator==(uint64_t rhs) const {
- C();
- return *this == mkUInt(rhs, bits());
-}
-
-expr expr::operator!=(uint64_t rhs) const {
- C();
- return *this != mkUInt(rhs, bits());
-}
-
expr expr::sext(unsigned amount) const {
C();
if (amount == 0)

MODIFY
smt/expr.h
smt/expr.h
@@ -176,12 +176,12 @@ public:
expr sge(const expr &rhs) const;
expr sgt(const expr &rhs) const;
- expr ule(uint64_t rhs) const;
- expr ult(uint64_t rhs) const;
- expr uge(uint64_t rhs) const;
- expr ugt(uint64_t rhs) const;
- expr operator==(uint64_t rhs) const;
- expr operator!=(uint64_t rhs) const;
+ expr ule(uint64_t rhs) const { return ule(mkUInt(rhs, bits())); }
+ expr ult(uint64_t rhs) const { return ult(mkUInt(rhs, bits())); }
+ expr uge(uint64_t rhs) const { return uge(mkUInt(rhs, bits())); }
+ expr ugt(uint64_t rhs) const { return ugt(mkUInt(rhs, bits())); }
+ expr operator==(uint64_t rhs) const { return *this == mkUInt(rhs, bits()); }
+ expr operator!=(uint64_t rhs) const { return *this != mkUInt(rhs, bits()); }
expr sext(unsigned amount) const;
expr zext(unsigned amount) const;

fix more crashes with invalid SMT exprs