mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-16 13:58:45 +00:00
Code Activity

fix #7609

Browse source
This commit is contained in:
Nikolaj Bjorner 2025-04-04 18:39:48 -07:00
parent 5e10fd39fc
commit 0a3719447e
1 changed files with 4 additions and 1 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

5
src/api/api_goal.cpp
View file

@ -158,7 +158,10 @@ extern "C" {
model_ref new_m;
Z3_model_ref * m_ref = alloc(Z3_model_ref, *mk_c(c));
mk_c(c)->save_object(m_ref);
if (m) m_ref->m_model = to_model_ref(m)->copy();
if (m)
m_ref->m_model = to_model_ref(m)->copy();
else
m_ref->m_model = alloc(model, mk_c(c)->m());
if (to_goal_ref(g)->mc())
(*to_goal_ref(g)->mc())(m_ref->m_model);
RETURN_Z3(of_model(m_ref));