From c6cd25c822a552d0caf813d33b89e086d05750d9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Tue, 8 Oct 2024 09:10:02 -0700
Subject: [PATCH] mico-tuning

---
 src/ast/normal_forms/nnf.cpp   |  5 +++--
 src/ast/recfun_decl_plugin.cpp | 16 +++++-----------
 2 files changed, 8 insertions(+), 13 deletions(-)

diff --git a/src/ast/normal_forms/nnf.cpp b/src/ast/normal_forms/nnf.cpp
index 1f0ce6781..9b4ea1346 100644
--- a/src/ast/normal_forms/nnf.cpp
+++ b/src/ast/normal_forms/nnf.cpp
@@ -69,6 +69,7 @@ class skolemizer {
     typedef act_cache cache;
 
     ast_manager & m;
+    var_subst     m_subst;
     symbol        m_sk_hack;
     bool          m_sk_hack_enabled;
     cache         m_cache;
@@ -128,7 +129,6 @@ class skolemizer {
         //
         // (VAR 0) should be in the last position of substitution.
         //
-        var_subst s(m);
         SASSERT(is_well_sorted(m, q->get_expr()));
         expr_ref tmp(m);
         expr * body = q->get_expr();
@@ -146,7 +146,7 @@ class skolemizer {
                 }
             }
         }
-        r = s(body, substitution);
+        r = m_subst(body, substitution);
         p = nullptr;
         if (m_proofs_enabled) {
             if (q->get_kind() == forall_k) 
@@ -159,6 +159,7 @@ class skolemizer {
 public:
     skolemizer(ast_manager & m):
         m(m),
+        m_subst(m),
         m_sk_hack("sk_hack"),
         m_sk_hack_enabled(false),
         m_cache(m),
diff --git a/src/ast/recfun_decl_plugin.cpp b/src/ast/recfun_decl_plugin.cpp
index cba1932be..79c6fa066 100644
--- a/src/ast/recfun_decl_plugin.cpp
+++ b/src/ast/recfun_decl_plugin.cpp
@@ -240,23 +240,18 @@ namespace recfun {
     {
         VERIFY(m_cases.empty() && "cases cannot already be computed");
         SASSERT(n_vars == m_domain.size());
-
         TRACEFN("compute cases " << mk_pp(rhs, m));
 
-        unsigned case_idx = 0;
-
-        std::string name("case-");       
-        name.append(m_name.str());
-
-        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");
-        
+
+
+        unsigned case_idx = 0;
         expr_ref_vector conditions(m);
+        m_vars.append(n_vars, vars);
+        m_rhs = rhs;        
 
         // is the function a macro (unconditional body)?
         if (is_macro || n_vars == 0 || !contains_ite(u, rhs)) {
@@ -265,7 +260,6 @@ namespace recfun {
             return;
         }
 
-
         
         // analyze control flow of `rhs`, accumulating guards and
         // rebuilding a `ite`-free RHS on the fly for each path in `rhs`.