fix #6330

Z3Prover · Sep 9, 2022 · 660bdc3 · 660bdc3
1 parent 058ed3d
commit 660bdc3
Showing 1 changed file with 8 additions and 0 deletions.
diff --git a/src/smt/theory_array_full.cpp b/src/smt/theory_array_full.cpp
@@ -604,6 +604,14 @@ namespace smt {
         for (unsigned i = 0; i < lam->get_num_decls(); ++i) 
             args.push_back(mk_epsilon(lam->get_decl_sort(i)).first);
         expr_ref val(mk_select(args), m);
+        ctx.get_rewriter()(val);
+        if (has_quantifiers(val)) {
+            expr_ref fn(m.mk_fresh_const("lambda-body", m.mk_bool_sort()), m);
+            expr_ref eq(m.mk_eq(fn, val), m);
+            ctx.assert_expr(eq);
+            ctx.internalize_assertions();
+            val = fn;
+        }
         ctx.internalize(def, false);
         ctx.internalize(val.get(), false);
         return try_assign_eq(val.get(), def);