fix assertion crashes in last commit
MODIFY
ir/state_value.cpp
ir/state_value.cpp
@@ -55,7 +55,7 @@ StateValue StateValue::subst(const vector<pair<expr, expr>> &repls) const {
// create dummy expr so we can do a single subst (more efficient than 2)
expr v1 = expr::mkVar("#1", value);
expr v2 = expr::mkVar("#2", non_poison);
- expr val = expr::mkIf(non_poison == v2, value, v1).subst(repls);
+ expr val = expr::mkIf(non_poison.cmp_eq(v2, false), value, v1).subst(repls);
expr cond, then, els, a, b, np;
ENSURE(val.isIf(cond, then, els));

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -966,7 +966,10 @@ expr expr::operator~() const {
return unop_fold(Z3_mk_bvnot);
}
-expr expr::operator==(const expr &rhs) const {
+expr expr::cmp_eq(const expr &rhs, bool simplify) const {
+ if (!simplify)
+ goto end;
+
if (eq(rhs))
return true;
if (isConst()) {
@@ -1012,6 +1015,7 @@ expr expr::operator==(const expr &rhs) const {
}
}
+ {
expr c, t, e;
if (isIf(c, t, e)) {
#if 0
@@ -1025,17 +1029,23 @@ expr expr::operator==(const expr &rhs) const {
e == Z3_get_app_arg(ctx(), rhs_app, 2));
}
#endif
-
// (= (ite c t e) x) -> (ite c (= t x) (= e x))
if (rhs.isConst() || (t.isConst() && e.isConst()))
return mkIf(c, t == rhs, e == rhs);
-
- } else if (rhs.isAppOf(Z3_OP_ITE)) {
+ }
+ else if (rhs.isAppOf(Z3_OP_ITE)) {
return rhs == *this;
}
+ }
+
+end:
return binop_commutative(rhs, Z3_mk_eq);
}
+expr expr::operator==(const expr &rhs) const {
+ return cmp_eq(rhs, true);
+}
+
expr expr::operator!=(const expr &rhs) const {
return !(*this == rhs);
}

MODIFY
smt/expr.h
smt/expr.h
@@ -209,6 +209,7 @@ public:
expr operator!() const;
expr operator~() const;
+ expr cmp_eq(const expr &rhs, bool simplify) const; // same as operator==
expr operator==(const expr &rhs) const;
expr operator!=(const expr &rhs) const;

fix assertion crashes in last commit