From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 11 Jul 2013 20:47:27 +0000 (-0400)
Subject: Fix for Boolean-term rewriting and LAMBDAs
X-Git-Tag: cvc5-1.0.0~7287^2~69
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=b76afedab3a23525da478ba4a8687c882793ea81;p=cvc5.git

Fix for Boolean-term rewriting and LAMBDAs
---

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 80518fcdf..a7fb09432 100644
--- a/src/smt/boolean_terms.cpp
+++ b/src/smt/boolean_terms.cpp
@@ -649,9 +649,6 @@ Node BooleanTermConverter::rewriteBooleanTermsRec(TNode top, theory::TheoryId pa
         goto next_worklist;
       }
       switch(k) {
-      case kind::LAMBDA:
-        Unreachable("not expecting a LAMBDA in boolean-term conversion: %s", top.toString().c_str());
-
       case kind::BOUND_VAR_LIST:
         result.top() << top;
         worklist.pop();