smt: add fold (a u% b) == c -> false if c u>= b
MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -451,6 +451,10 @@ bool expr::isAdd(expr &a, expr &b) const {
return isBinOp(a, b, Z3_OP_BADD);
}
+bool expr::isURem(expr &a, expr &b) const {
+ return isBinOp(a, b, Z3_OP_BUREM);
+}
+
bool expr::isBasePlusOffset(expr &base, uint64_t &offset) const {
expr a, b;
if (isAdd(a, b)) {
@@ -1260,6 +1264,13 @@ expr expr::cmp_eq(const expr &rhs, bool simplify) const {
}
}
+ // (a u% b) == c -> false if c u>= b
+ {
+ expr a, b;
+ if (isURem(a, b) && rhs.uge(b).isTrue())
+ return false;
+ }
+
end:
return binop_commutative(rhs, Z3_mk_eq);
}

MODIFY
smt/expr.h
smt/expr.h
@@ -141,6 +141,7 @@ public:
bool isAnd(expr &a, expr &b) const;
bool isNot(expr &neg) const;
bool isAdd(expr &a, expr &b) const;
+ bool isURem(expr &a, expr &b) const;
bool isBasePlusOffset(expr &base, uint64_t &offset) const;
bool isConstArray(expr &val) const;
bool isStore(expr &array, expr &idx, expr &val) const;

smt: add fold (a u% b) == c -> false if c u>= b