From d64ce41b2e31bbc5bfd24b05d4fbb385f3105f27 Mon Sep 17 00:00:00 2001
From: Copilot <198982749+Copilot@users.noreply.github.com>
Date: Wed, 3 Jun 2026 08:16:46 -0700
Subject: [PATCH] Remove unused defined_names artifacts and simplify
 fingerprint_set::contains (#9702)
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

Cleans up dead code left by the "remove side definitions" refactoring
(a0a3047).

- **`smt_model_checker.cpp`** — Remove `defined_names dn(m)` variable
that was declared but never used
- **`smt_model_checker.h`** — Drop the now-unnecessary `#include
"ast/normal_forms/defined_names.h"`
- **`fingerprints.cpp`** — Collapse redundant tail in
`fingerprint_set::contains`:
  ```cpp
  // Before
  if (m_set.contains(d))
      return true;
  return false;

  // After
  return m_set.contains(d);
  ```

---------

Co-authored-by: copilot-swe-agent[bot] <198982749+Copilot@users.noreply.github.com>
---
 src/smt/fingerprints.cpp      | 4 +---
 src/smt/smt_model_checker.cpp | 1 -
 src/smt/smt_model_checker.h   | 1 -
 3 files changed, 1 insertion(+), 5 deletions(-)

diff --git a/src/smt/fingerprints.cpp b/src/smt/fingerprints.cpp
index 4550d22b5..d41e01573 100644
--- a/src/smt/fingerprints.cpp
+++ b/src/smt/fingerprints.cpp
@@ -104,9 +104,7 @@ namespace smt {
             return true;
         for (unsigned i = 0; i < num_args; ++i)
             d->m_args[i] = d->m_args[i]->get_root();
-        if (m_set.contains(d))
-            return true;
-        return false;
+        return m_set.contains(d);
     }
     
     void fingerprint_set::reset() {
diff --git a/src/smt/smt_model_checker.cpp b/src/smt/smt_model_checker.cpp
index 0037bb3da..c23cfe01e 100644
--- a/src/smt/smt_model_checker.cpp
+++ b/src/smt/smt_model_checker.cpp
@@ -258,7 +258,6 @@ namespace smt {
                 svector<symbol> names;
                 for (unsigned i = 0; i < f->get_arity(); ++i) 
                     names.push_back(symbol(i));
-                defined_names dn(m);
                 body = replace_value_from_ctx(body);
                 body = m.mk_lambda(sorts.size(), sorts.data(), names.data(), body);
                 sk_term = body;
diff --git a/src/smt/smt_model_checker.h b/src/smt/smt_model_checker.h
index c816b3cc0..3a8e81639 100644
--- a/src/smt/smt_model_checker.h
+++ b/src/smt/smt_model_checker.h
@@ -23,7 +23,6 @@ Revision History:
 #include "util/obj_hashtable.h"
 #include "ast/ast.h"
 #include "ast/array_decl_plugin.h"
-#include "ast/normal_forms/defined_names.h"
 #include "params/qi_params.h"
 #include "params/smt_params.h"