Fix for Boolean-term rewriting and LAMBDAs

diff --git a/src/smt/boolean_terms.cpp b/src/smt/boolean_terms.cpp
index 80518fcdf80ef78876640733e2b790de56498d40..a7fb0943262b60ba17b7bef86f46b54c288858da 100644 (file)
--- 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();