From 1d3e9fb76c9a8cf5f88f0e56a1ab9e087dd5e2e0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 15 Feb 2020 21:30:09 -1000
Subject: [PATCH] fix #3009

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/qe/qsat.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/qe/qsat.cpp b/src/qe/qsat.cpp
index 650ad91bb..f24a4cbba 100644
--- a/src/qe/qsat.cpp
+++ b/src/qe/qsat.cpp
@@ -1007,6 +1007,11 @@ namespace qe {
                     break;
                 }
                 case AST_QUANTIFIER: {
+                    if (is_lambda(e)) {
+                        visited.insert(e, e);
+                        todo.pop_back();
+                        break;
+                    }
                     SASSERT(!is_lambda(e));
                     app_ref_vector vars(m);
                     quantifier* q = to_quantifier(e);