fix bugs in undef quantifiers
MODIFY
ir/state.cpp
ir/state.cpp
@@ -67,6 +67,7 @@ const StateValue& State::operator[](const Value &val) {
++VI;
}
}
+ undef_vars.insert(VI, VE);
if (repls.empty())
return sval;
@@ -121,6 +122,7 @@ void State::addUndefVar(const expr &var) {
}
void State::resetUndefVars() {
+ quantified_vars.insert(undef_vars.begin(), undef_vars.end());
undef_vars.clear();
}

MODIFY
ir/type.cpp
ir/type.cpp
@@ -11,7 +11,7 @@ using namespace smt;
using namespace std;
static constexpr unsigned var_type_bits = 3;
-static constexpr unsigned var_bw_bits = 10;
+static constexpr unsigned var_bw_bits = 8;
namespace IR {

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -63,8 +63,10 @@ Errors TransformVerify::verify() const {
continue;
// TODO: add data-flow domain tracking for Alive, but not for TV
- check_refinement(s, errs, tgt_state.getQuantVars(),
+ check_refinement(s, errs, src_state.getQuantVars(),
true, val, true, tgt_state.at(*tgt_vals.at(name)));
+ if (errs)
+ return errs;
}
}
@@ -75,7 +77,7 @@ Errors TransformVerify::verify() const {
errs.add("Target returns but source doesn't");
} else if (src_state.fnReturned()) {
- check_refinement(s, errs, tgt_state.getQuantVars(),
+ check_refinement(s, errs, src_state.getQuantVars(),
src_state.returnDomain(), src_state.returnVal(),
tgt_state.returnDomain(), tgt_state.returnVal());
}

fix bugs in undef quantifiers