Address the case when fncall's vararg types are different
MODIFY
ir/instr.cpp
ir/instr.cpp
#include "smt/solver.h"
#include "util/compiler.h"
#include <functional>
+#include <sstream>
using namespace smt;
using namespace util;
@@ -1151,15 +1152,18 @@ StateValue FnCall::toSMT(State &s) const {
vector<StateValue> inputs, ptr_inputs;
vector<Type*> out_types;
+ ostringstream fnName_mangled;
+ fnName_mangled << fnName;
for (auto arg : args) {
unpack_inputs(s, arg->getType(), s[*arg], inputs, ptr_inputs);
+ fnName_mangled << "#" << arg->getType().toString();
}
if (!isVoid())
unpack_ret_ty(out_types, getType());
unsigned idx = 0;
- auto ret = s.addFnCall(fnName, move(inputs), move(ptr_inputs), out_types,
- !(flags & NoRead), !(flags & NoWrite),
+ auto ret = s.addFnCall(fnName_mangled.str(), move(inputs), move(ptr_inputs),
+ out_types, !(flags & NoRead), !(flags & NoWrite),
flags & ArgMemOnly);
return isVoid() ? StateValue() : pack_return(getType(), ret, flags, idx);
}

MODIFY
ir/state.cpp
ir/state.cpp
@@ -359,8 +359,7 @@ void State::mkAxioms(State &tgt) {
auto &[ins2, ptr_ins2, mem2, reads2, argmem2] = I2->first;
auto &[rets2, ub2, mem_state2] = I2->second;
- if (reads != reads2 || argmem != argmem2 || ins.size() != ins2.size()
- || ptr_ins.size() != ptr_ins2.size())
+ if (reads != reads2 || argmem != argmem2)
continue;
expr refines(true), is_val_eq(true);

Address the case when fncall's vararg types are different (#274)