fix #6591

- add check for lambdas similar to as-array in context of quantifiers. MBQI is not a decision procedure for this combination and can then incorrectly conclude satisfiabiltiy.

Scenario

The formula contains assertions
 - bv = (map or (lambda ..) t)
 - forall y (not (select bv (pair s y)))

Since bv is extensionally equal to a term that depends on a lambda, MBQI cannot just take the current finite approximation of bv when checking the quantifier for satisfiability.

src/smt/theory_array_full.cpp

@@ -252,6 +252,8 @@ namespace smt {
         else if (m.is_lambda_def(n->get_decl())) {
             instantiate_default_lambda_def_axiom(n);
             d->m_lambdas.push_back(n);
+            m_lambdas.push_back(n);
+            ctx.push_trail(push_back_vector(m_lambdas));
         }
         return r;
     }
@@ -830,6 +832,12 @@ namespace smt {
                     return true;
                 }
         }
+        for (enode* n : m_lambdas) 
+            for (enode* p : n->get_parents())
+                if (!ctx.is_beta_redex(p, n)) {
+                    TRACE("array", tout << "not a beta redex " << enode_pp(p, ctx) << "\n");
+                    return true;
+                }
         return false;
     }
 

src/smt/theory_array_full.h

@@ -86,6 +86,7 @@ namespace smt {
         bool has_unitary_domain(app* array_term);
         std::pair<app*,func_decl*> mk_epsilon(sort* s);
         enode_vector m_as_array;
+        enode_vector m_lambdas;
         bool has_non_beta_as_array();
 
         bool instantiate_select_const_axiom(enode* select, enode* cnst);