mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 10:55:50 +00:00
Code Activity

fix #7499 - add another way to avoid adding user-defined functions to models if user don't want it

Browse source 
- you can already do model.user_functions=false
- now you can also specify smtlib2_compliant (globally) and get smtlib2 behavior
This commit is contained in:
Nikolaj Bjorner 2025-01-15 19:52:04 -08:00
parent a5e1e7f5d2
commit 557c01a0e5
1 changed files with 3 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

4
src/smt/smt_context.cpp
View file

@ -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();
}