fix printing cex with structs with small ints as fields
MODIFY
ir/type.cpp
ir/type.cpp
@@ -626,7 +626,7 @@ void StructType::printVal(ostream &os, const expr &val) const {
for (size_t i = 0, e = children.size(); i != e; ++i) {
if (!first)
os << ", ";
- getChild(i).printVal(os, extract(val, i));
+ getChild(i).printVal(os, extract(val, i).simplify());
first = false;
}
os << " }";

MODIFY
smt/expr.cpp
smt/expr.cpp
@@ -996,6 +996,10 @@ expr expr::extract(unsigned high, unsigned low) const {
if (low == 0 && high == bits()-1)
return *this;
+ uint64_t n;
+ if (low < 64 && isUInt(n))
+ return mkUInt(n >> low, high - low + 1);
+
{
expr sub;
unsigned high_2, low_2;
@@ -1132,7 +1136,7 @@ expr expr::subst(const expr &from, const expr &to) const {
void expr::printUnsigned(ostream &os) const {
uint64_t num;
- if (isUInt(num)) {
+ if (simplify().isUInt(num)) {
os << num;
return;
}

fix printing cex with structs with small ints as fields