From 03ff3201b90a3aef32c99e9e2d367e7c44260e82 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Sun, 6 Feb 2022 08:57:58 +0200 Subject: [PATCH] block recursive definitions with lambdas until they are properly supported #5813 --- src/ast/recfun_decl_plugin.cpp | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp index 9a8c59ae9a8..0e9c27655b8 100644 --- a/src/ast/recfun_decl_plugin.cpp +++ b/src/ast/recfun_decl_plugin.cpp @@ -225,6 +225,11 @@ namespace recfun { m_vars.append(n_vars, vars); m_rhs = rhs; + if (!is_macro) + for (expr* e : subterms::all(m_rhs)) + if (is_lambda(e)) + throw default_exception("recursive definitions with lambdas are not supported"); + expr_ref_vector conditions(m); // is the function a macro (unconditional body)? @@ -233,6 +238,8 @@ namespace recfun { add_case(name, 0, conditions, rhs); return; } + + // analyze control flow of `rhs`, accumulating guards and // rebuilding a `ite`-free RHS on the fly for each path in `rhs`.