From 530c6fc625d85ed8b22d27e0b066896f1b669f28 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Wed, 20 Mar 2024 22:05:30 -0700
Subject: [PATCH] fix ##7175 - don't add user macros/functions when
 smtlib2_compliant=true

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/cmd_context/cmd_context.cpp | 5 +++++
 1 file changed, 5 insertions(+)

diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 019b7fd4f..e883d0e9d 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -1894,6 +1894,8 @@ void cmd_context::add_declared_functions(model& mdl) {
     model_params p;
     if (!p.user_functions())
         return;
+    if (m_params.m_smtlib2_compliant)
+        return;
     for (auto const& kv : m_func_decls) {
         func_decl* f = kv.m_value.first();
         if (f->get_family_id() == null_family_id && !mdl.has_interpretation(f)) {
@@ -2066,7 +2068,10 @@ void cmd_context::complete_model(model_ref& md) const {
                 
             if (m_macros.find(k, decls)) 
                 body = decls.find(f->get_arity(), f->get_domain());
+            if (body && m_params.m_smtlib2_compliant)
+                continue;
             sort * range = f->get_range();
+            
             if (!body)
                 body = m().get_some_value(range);
             if (f->get_arity() > 0) {