From 16c4b88bc10557e884943b9b3ea29f6e9a07c49f Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 8 Aug 2013 12:23:59 -0400
Subject: [PATCH] Parameterized, uninterpreted sorts need no Boolean-term
 conversion

---
 src/smt/boolean_terms.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index a7fb09432..9f1b9c1a6 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -288,7 +288,7 @@ TypeNode BooleanTermConverter::convertType(TypeNode type, bool datatypesContext)
     }
     return newRec;
   }
-  if(type.getNumChildren() > 0) {
+  if(!type.isSort() && type.getNumChildren() > 0) {
     Debug("boolean-terms") << "here at A for " << type << ":" << type.getId() << endl;
     // This should handle tuples and arrays ok.
     // Might handle function types too, but they can't go
@@ -626,7 +626,7 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
             worklist.pop();
             goto next_worklist;
           }
-        } else if(t.getNumChildren() > 0) {
+        } else if(!t.isSort() && t.getNumChildren() > 0) {
           for(TypeNode::iterator i = t.begin(); i != t.end(); ++i) {
             if((*i).isBoolean()) {
               vector<TypeNode> argTypes(t.begin(), t.end());
-- 
2.30.2