From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Fri, 22 Feb 2013 15:52:46 +0000 (-0500)
Subject: Fix for quantifiers containing Boolean terms.
X-Git-Tag: cvc5-1.0.0~7391^2~5
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=f0e49547916c713dc53e81192adde66950caaa9b;p=cvc5.git

Fix for quantifiers containing Boolean terms.
---

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 696622cfe..262244f42 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -39,6 +39,13 @@ static inline bool isBoolean(TNode top, unsigned i) {
   case kind::IMPLIES:
   case kind::OR:
   case kind::XOR:
+  case kind::FORALL:
+  case kind::EXISTS:
+  case kind::REWRITE_RULE:
+  case kind::RR_REWRITE:
+  case kind::RR_DEDUCTION:
+  case kind::RR_REDUCTION:
+  case kind::INST_PATTERN:
     return true;
 
   case kind::ITE:
@@ -289,13 +296,16 @@ Node BooleanTermConverter::rewriteBooleanTerms(TNode top, bool boolParent) throw
   }
   switch(k) {
   case kind::LAMBDA:
-  case kind::FORALL:
-  case kind::EXISTS:
+    Unreachable("not expecting a LAMBDA in boolean-term conversion: %s", top.toString().c_str());
+
+  case kind::BOUND_VAR_LIST:
+    return top;
+
   case kind::REWRITE_RULE:
   case kind::RR_REWRITE:
-  case kind::RR_REDUCTION:
   case kind::RR_DEDUCTION:
-    //Assert(false, "not yet supported");
+  case kind::RR_REDUCTION:
+    // not yet supported
     return top;
 
   default: