Skip to content

Commit

Permalink
fix #7499 - add another way to avoid adding user-defined functions to…
Browse files Browse the repository at this point in the history
… 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
  • Loading branch information
NikolajBjorner committed Jan 16, 2025
1 parent a5e1e7f commit 557c01a
Showing 1 changed file with 3 additions and 1 deletion.
4 changes: 3 additions & 1 deletion src/smt/smt_context.cpp
Original file line number Diff line number Diff line change
Expand Up @@ -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();
}

Expand Down

0 comments on commit 557c01a

Please sign in to comment.