From: Morgan Deters <mdeters@gmail.com>
Date: Thu, 29 Nov 2012 21:34:16 +0000 (+0000)
Subject: fix for andy: boolean terms stuff really shouldn't look at datatypes at all in this... 
X-Git-Tag: cvc5-1.0.0~7529
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=03a8787579038655fff814fbad05047ce24bf532;p=cvc5.git

fix for andy: boolean terms stuff really shouldn't look at datatypes at all in this release
---

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index f90b5ff51..15a1244e2 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -166,6 +166,7 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw
     } else if(t.isRecord()) {
       return top;
     } else if(t.isDatatype()) {
+      return top;// no support for datatypes at present
       const Datatype& dt = t.getConst<Datatype>();
       const Datatype& dt2 = booleanTermsConvertDatatype(dt);
       if(dt != dt2) {
@@ -185,6 +186,7 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw
         return top;
       }
     } else if(t.isConstructor()) {
+      return top;// no support for datatypes at present
       Assert(!boolParent);
       const Datatype& dt = t[t.getNumChildren() - 1].getConst<Datatype>();
       const Datatype& dt2 = booleanTermsConvertDatatype(dt);
@@ -197,6 +199,7 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw
         return top;
       }
     } else if(t.isTester() || t.isSelector()) {
+      return top;// no support for datatypes at present
       Assert(!boolParent);
       const Datatype& dt = t[0].getConst<Datatype>();
       const Datatype& dt2 = booleanTermsConvertDatatype(dt);
@@ -242,6 +245,7 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw
     Debug("bt") << "looking at: " << top << std::endl;
     if(mk == kind::metakind::PARAMETERIZED) {
       if(kindToTheoryId(k) != THEORY_BV &&
+         k != kind::APPLY_TYPE_ASCRIPTION &&
          k != kind::TUPLE_SELECT &&
          k != kind::TUPLE_UPDATE &&
          k != kind::RECORD_SELECT &&