summaryrefslogtreecommitdiff
path: root/src/compat
diff options
context:
space:
mode:
Diffstat (limited to 'src/compat')
-rw-r--r--src/compat/cvc3_compat.cpp3
1 files changed, 1 insertions, 2 deletions
diff --git a/src/compat/cvc3_compat.cpp b/src/compat/cvc3_compat.cpp
index 52174dce0..a9982e336 100644
--- a/src/compat/cvc3_compat.cpp
+++ b/src/compat/cvc3_compat.cpp
@@ -1818,8 +1818,7 @@ Expr ValidityChecker::recordExpr(const std::vector<std::string>& fields,
Expr ValidityChecker::recSelectExpr(const Expr& record, const std::string& field) {
Type t = record.getType();
const CVC4::Datatype& dt = ((CVC4::DatatypeType)t).getDatatype();
- const CVC4::Record& rec = ((CVC4::DatatypeType)t).getRecord();
- unsigned index = rec.getIndex(field);
+ unsigned index = CVC4::Datatype::indexOf( dt[0].getSelector(field) );
return d_em->mkExpr(CVC4::kind::APPLY_SELECTOR_TOTAL, dt[0][index].getSelector(), record);
}
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback