fix cex printing of registers when they become undef
it used to print 0 due to model completion
fixes
MODIFY
smt/solver.cpp
smt/solver.cpp
@@ -164,9 +164,10 @@ void Model::operator=(Model &&other) {
swap(other.m, m);
}
-expr Model::operator[](const expr &var) const {
+expr Model::eval(const expr &var, bool complete) const {
Z3_ast val;
- return Z3_model_eval(ctx(), m, var(), true, &val) ? val : expr();
+ ENSURE(Z3_model_eval(ctx(), m, var(), complete, &val));
+ return val;
}
uint64_t Model::getUInt(const expr &var) const {

MODIFY
smt/solver.h
smt/solver.h
@@ -31,7 +31,8 @@ public:
void operator=(Model &&other);
- expr operator[](const expr &var) const;
+ expr operator[](const expr &var) const { return eval(var, true); }
+ expr eval(const expr &var, bool complete = false) const;
uint64_t getUInt(const expr &var) const;
int64_t getInt(const expr &var) const;

MODIFY
tools/transform.cpp
tools/transform.cpp
@@ -21,7 +21,11 @@ using namespace std;
static void print_varval(ostream &s, const Model &m, const Value *var,
const StateValue &val) {
- if (m[val.non_poison].isFalse()) {
+ // if the model is partial, we don't know for sure if it's poison or not
+ // this happens if the poison constraint depends on an undef
+ // however, cexs are usually triggered by the worst case, which is poison
+ if (auto v = m.eval(val.non_poison);
+ (!v.isConst() || v.isFalse())) {
s << "poison";
return;
}
@@ -36,7 +40,13 @@ static void print_varval(ostream &s, const Model &m, const Value *var,
assert(n == 0);
}
- expr e = m[val.value];
+ expr e = m.eval(val.value);
+ // undef variables may not have a model since each read uses a copy
+ if (!e.isConst()) {
+ s << "undef";
+ return;
+ }
+
e.printHexadecimal(s);
s << " (";
e.printUnsigned(s);

fix cex printing of registers when they become undef
it used to print 0 due to model completion
fixes #42