More simplification to internal implementation of tuples and records.

1 files changed, 0 insertions, 20 deletions

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 07d78a6fd..1adc71d70 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -137,26 +137,6 @@ Node BooleanTermConverter::rewriteAs(TNode in, TypeNode as, std::map< TypeNode,
   TypeNode in_t = in.getType();
   if( processing.find( in_t )==processing.end() ){
     processing[in_t] = true;
-    if(in.getType().isRecord()) {
-      Assert(as.isRecord());
-      const Record& inRec = in.getType().getRecord();
-      const Record& asRec = as.getRecord();
-      Assert(inRec.getNumFields() == asRec.getNumFields());
-      const Datatype & dt = ((DatatypeType)in.getType().toType()).getDatatype();
-      NodeBuilder<> nb(kind::APPLY_CONSTRUCTOR);
-      nb << NodeManager::currentNM()->mkConst(asRec);
-      for(size_t i = 0; i < asRec.getNumFields(); ++i) {
-        Assert(inRec[i].first == asRec[i].first);
-        Node arg = NodeManager::currentNM()->mkNode(kind::APPLY_SELECTOR_TOTAL, dt[0][i].getSelector(), in);
-        if(inRec[i].second != asRec[i].second) {
-          arg = rewriteAs(arg, TypeNode::fromType(asRec[i].second), processing);
-        }
-        nb << arg;
-      }
-      Node out = nb;
-      processing.erase( in_t );
-      return out;
-    }
     if(in.getType().isDatatype()) {
       if(as.isBoolean() && in.getType().hasAttribute(BooleanTermAttr())) {
         processing.erase( in_t );