From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 8 Aug 2013 16:23:59 +0000 (-0400)
Subject: Parameterized, uninterpreted sorts need no Boolean-term conversion
X-Git-Tag: cvc5-1.0.0~7287^2~41
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=16c4b88bc10557e884943b9b3ea29f6e9a07c49f;p=cvc5.git

Parameterized, uninterpreted sorts need no Boolean-term conversion
---

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());