move memory var insertion to where refinement is computed
so we can take advantage of constant folds to avoid quantifying
MODIFY
ir/state.cpp
ir/state.cpp
@@ -241,11 +241,6 @@ State::addFnCall(const string &name, vector<StateValue> &&inputs,
return vector<StateValue>(out_types.size());
}
- if (reads_memory) {
- auto &uvs = memory.getUndefVars();
- undef_vars.insert(uvs.begin(), uvs.end());
- }
-
// TODO: this doesn't need to compare the full memory, just a subset of fields
auto call_data_pair
= fn_call_data[name].try_emplace({ move(inputs), move(ptr_inputs),
@@ -439,6 +434,10 @@ void State::mkAxioms(State &tgt) {
auto restrict_ptrs = argmem2 ? &ptr_ins2 : nullptr;
expr mem_refined = mem.refined(mem2, true, restrict_ptrs).first;
refines &= mem_refined;
+ if (!mem_refined.isConst()) {
+ auto &u = mem.getUndefVars();
+ quantified_vars.insert(u.begin(), u.end());
+ }
}
expr ref_expr(true);

move memory var insertion to where refinement is computed
so we can take advantage of constant folds to avoid quantifying