fix crashes in type inference
MODIFY
ir/instr.cpp
ir/instr.cpp
@@ -329,13 +329,15 @@ StateValue ICmp::toSMT(State &s) const {
}
expr ICmp::getTypeConstraints() const {
- return a.getTypeConstraints() &&
+ return getType().getTypeConstraints() &&
+ a.getTypeConstraints() &&
a.getType() == b.getType() &&
(cond == Any ? cond_var.ule(expr::mkUInt(9, 4))
: cond_var == expr::mkUInt(cond, 4));
}
void ICmp::fixupTypes(const Model &m) {
+ Value::fixupTypes(m);
cond = (Cond)m.getUInt(cond_var);
}

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -252,7 +252,6 @@ bool expr::isInt(int64_t &n) const {
}
bool expr::isNot(expr &neg) const {
- C();
if (auto app = isAppOf(Z3_OP_NOT)) {
neg = Z3_get_app_arg(ctx(), app, 0);
return true;

MODIFY
smt/expr.h
smt/expr.h
@@ -27,7 +27,7 @@ class expr {
Z3_sort sort() const;
Z3_app isApp() const;
- Z3_app isAppOf(int app) const;
+ Z3_app isAppOf(int app_type) const;
expr binop_commutative(const expr &rhs,
uint64_t(*native)(uint64_t, uint64_t),

MODIFY
tools/alive_parser.cpp
tools/alive_parser.cpp
@@ -231,10 +231,7 @@ static unique_ptr<Instr> parse_conversionop(string_view name, token op_token) {
// op ty %op to ty2
auto opty = parse_type();
auto &val = parse_operand(opty.get());
- unique_ptr<Type> ty2;
- if (tokenizer.consumeIf(TO)) {
- ty2 = parse_type(/*optional=*/false);
- }
+ unique_ptr<Type> ty2 = parse_type(/*optional=*/!tokenizer.consumeIf(TO));
ConversionOp::Op op;
switch (op_token) {

fix crashes in type inference