From 406c0792f16d881c88149d73b610b7d400d92aa7 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 5 Apr 2020 14:04:00 -0700
Subject: [PATCH] fix #3775

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/muz/base/dl_rule.cpp | 9 +++++----
 src/muz/base/dl_rule.h   | 9 +++++----
 2 files changed, 10 insertions(+), 8 deletions(-)

diff --git a/src/muz/base/dl_rule.cpp b/src/muz/base/dl_rule.cpp
index 1b9a5cce8..6ca1cf7ab 100644
--- a/src/muz/base/dl_rule.cpp
+++ b/src/muz/base/dl_rule.cpp
@@ -912,7 +912,7 @@ namespace datalog {
     // Quantifiers may appear only in the interpreted tail, it is therefore
     // sufficient only to check the interpreted tail.
     //
-    void rule_manager::has_quantifiers(rule const& r, bool& existential, bool& universal) const {
+    void rule_manager::has_quantifiers(rule const& r, bool& existential, bool& universal, bool& lam) const {
         unsigned sz = r.get_tail_size();
         m_qproc.reset();
         m_visited.reset();
@@ -921,12 +921,13 @@ namespace datalog {
         }
         existential = m_qproc.m_exist;
         universal = m_qproc.m_univ;
+        lam = m_qproc.m_lambda;
     }
 
     bool rule_manager::has_quantifiers(rule const& r) const {
-        bool exist, univ;
-        has_quantifiers(r, exist, univ);
-        return exist || univ;
+        bool exist, univ, lam;
+        has_quantifiers(r, exist, univ, lam);
+        return exist || univ || lam;
     }
 
     bool rule_manager::is_finite_domain(rule const& r) const {
diff --git a/src/muz/base/dl_rule.h b/src/muz/base/dl_rule.h
index 1c17b8b3a..55e482bb7 100644
--- a/src/muz/base/dl_rule.h
+++ b/src/muz/base/dl_rule.h
@@ -79,17 +79,18 @@ namespace datalog {
     struct quantifier_finder_proc {
         bool m_exist;
         bool m_univ;
-        quantifier_finder_proc() : m_exist(false), m_univ(false) {}
+        bool m_lambda;
+        quantifier_finder_proc() : m_exist(false), m_univ(false), m_lambda(false) {}
         void operator()(var * n) { }
         void operator()(quantifier * n) {
             switch (n->get_kind()) {
             case forall_k: m_univ = true; break;
             case exists_k: m_exist = true; break;
-            case lambda_k: UNREACHABLE();
+            case lambda_k: m_lambda = true; break;
             }
         }
         void operator()(app * n) { }
-        void reset() { m_exist = m_univ = false; }
+        void reset() { m_exist = m_univ = m_lambda = false; }
     };
 
     struct fd_finder_proc {
@@ -278,7 +279,7 @@ namespace datalog {
         std::ostream& display_smt2(rule const& r, std::ostream & out);
 
         bool has_uninterpreted_non_predicates(rule const& r, func_decl*& f) const;
-        void has_quantifiers(rule const& r, bool& existential, bool& universal) const;
+        void has_quantifiers(rule const& r, bool& existential, bool& universal, bool& lam) const;
         bool has_quantifiers(rule const& r) const;
         bool is_finite_domain(rule const& r) const;