From 557c01a0e5a7aa0b3edd634fcf9cbfe3efedba55 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 15 Jan 2025 19:52:04 -0800 Subject: [PATCH] fix #7499 - add another way to avoid adding user-defined functions to models if user don't want it - you can already do model.user_functions=false - now you can also specify smtlib2_compliant (globally) and get smtlib2 behavior --- src/smt/smt_context.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) diff --git a/src/smt/smt_context.cpp b/src/smt/smt_context.cpp index 153dcae18..20a4bdde1 100644 --- a/src/smt/smt_context.cpp +++ b/src/smt/smt_context.cpp @@ -4787,7 +4787,9 @@ namespace smt { void context::add_rec_funs_to_model() { model_params p; - if (m_model && p.user_functions()) + auto smtlib2_compliant = gparams::get_value("smtlib2_compliant"); + + if (m_model && p.user_functions() && smtlib2_compliant != "true") m_model->add_rec_funs(); }