From 156bf81349038aee1214fce83f17c9a86489af53 Mon Sep 17 00:00:00 2001
From: "github-actions[bot]"
 <41898282+github-actions[bot]@users.noreply.github.com>
Date: Tue, 2 Jun 2026 05:55:22 +0000
Subject: [PATCH] simplify model_core.h: remove unused typedef, fix trailing
 whitespace, simplify get_some_const_interp

- Remove unused i_interp typedef (was never referenced outside of its definition)
- Remove trailing whitespace on m_const_decls, m_func_decls lines
- Simplify get_some_const_interp body using ternary operator

Co-authored-by: Copilot <223556219+Copilot@users.noreply.github.com>
---
 src/model/model_core.h | 14 ++++++--------
 1 file changed, 6 insertions(+), 8 deletions(-)

diff --git a/src/model/model_core.h b/src/model/model_core.h
index 6cc52bbcb9..01640c2c82 100644
--- a/src/model/model_core.h
+++ b/src/model/model_core.h
@@ -25,7 +25,6 @@ Revision History:
 class model_core {
 protected:
     typedef std::pair<unsigned, expr*> i_expr;
-    typedef std::pair<unsigned, func_interp*> i_interp;
     typedef obj_map<func_decl, i_expr>       decl2expr;
     typedef obj_map<func_decl, func_interp*> decl2finterp;
     ast_manager &                 m;
@@ -33,9 +32,9 @@ protected:
     decl2expr                     m_interp;      //!< interpretation for uninterpreted constants
     decl2finterp                  m_finterp;     //!< interpretation for uninterpreted functions
     ptr_vector<func_decl>         m_decls;       //!< domain of m_interp
-    ptr_vector<func_decl>         m_const_decls; 
-    ptr_vector<func_decl>         m_func_decls;  
-    
+    ptr_vector<func_decl>         m_const_decls;
+    ptr_vector<func_decl>         m_func_decls;
+
 public:
     model_core(ast_manager & m):m(m), m_ref_count(0) { }
     virtual ~model_core();
@@ -78,10 +77,9 @@ public:
     virtual expr * get_fresh_value(sort * s) = 0;
     virtual bool get_some_values(sort * s, expr_ref & v1, expr_ref & v2) = 0;
 
-    expr * get_some_const_interp(func_decl * d) { 
-        expr * r = get_const_interp(d); 
-        if (r) return r; 
-        return get_some_value(d->get_range()); 
+    expr * get_some_const_interp(func_decl * d) {
+        expr * r = get_const_interp(d);
+        return r ? r : get_some_value(d->get_range());
     }
     //
     // Reference counting