From b76afedab3a23525da478ba4a8687c882793ea81 Mon Sep 17 00:00:00 2001
From: Morgan Deters <mdeters@cs.nyu.edu>
Date: Thu, 11 Jul 2013 16:47:27 -0400
Subject: [PATCH] Fix for Boolean-term rewriting and LAMBDAs

---
 src/smt/boolean_terms.cpp | 3 ---
 1 file changed, 3 deletions(-)

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