8000 Z3_goal_convert_model given a NULL model can crash · Issue #7609 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Z3_goal_convert_model given a NULL model can crash #7609

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom
Closed
jberdine opened this issue Apr 4, 2025 · 2 comments
Closed

Z3_goal_convert_model given a NULL model can crash #7609

jberdine opened this issue Apr 4, 2025 · 2 comments

Comments

@jberdine
Copy link
Contributor
jberdine commented Apr 4, 2025

I don't know if there is an issue or I am using the API incorrectly, but I'm having trouble with Z3_goal_convert_model when giving it a NULL model. I could be misunderstanding the API docs:

Convert a model of the formulas of a goal to a model of an original goal.
The model may be null, in which case the returned model is valid if the goal was
established satisfiable.

To be concrete, consider the attached program test_convert_model.c.txt (with extra .txt to appease github). This program sets up a small instance and calls Z3_goal_convert_model in a way that makes Z3 unhappy, see the comment pointing to the call that crashes.
@NikolajBjorner
Copy link
Contributor

it should be

Z3_model Z3_API Z3_goal_convert_model(Z3_context c, Z3_goal g, Z3_model m) {
    Z3_TRY;
    LOG_Z3_goal_convert_model(c, g, m);
    RESET_ERROR_CODE();
    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();
    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));
    Z3_CATCH_RETURN(nullptr);
}

@jberdine
Copy link
Contributor Author
jberdine commented Apr 5, 2025

Thanks!

arbipher pushed a commit to arbipher/z3 that referenced this issue Apr 17, 2025
@NikolajBjorner @arbipher
fix Z3Prover#7609
49b8d69
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@jberdine @NikolajBjorner
0