diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-15 18:10:42 -0600 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2016-02-15 18:10:42 -0600 |
| commit | 80daa7fd5917526513a510261fd3901f03949dfa (patch) | |
| tree | 7fa74722e30c6e5cc59d96b045273c2bdaf27701 /src/compat/cvc3_compat.cpp | |
| parent | f31163c1f6bb1816365e9f22505d9558a7bc1802 (diff) | |
More simplification to internal implementation of tuples and records.
Diffstat (limited to 'src/compat/cvc3_compat.cpp')
| -rw-r--r-- | src/compat/cvc3_compat.cpp | 3 |
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); } |