8000 Z3_solver_set_initial_value unhappy if called before any assertions · Issue #7616 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Z3_solver_set_initial_value unhappy if called before any assertions #7616

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 8, 2025 · 0 comments
Closed

Z3_solver_set_initial_value unhappy if called before any assertions #7616

jberdine opened this issue Apr 8, 2025 · 0 comments

Comments

@jberdine
Copy link
Contributor
jberdine commented Apr 8, 2025

I'm not sure what the desired change is, but Z3_solver_set_initial_value can crash if called before anything is asserted to the solver. For contrast, it looks like cmd_context::set_initial_value builds a set of pending assignments in this case.

See test_solver_set_initial_value.c.txt for a small repro.

This is easy to work around, so FWIW definitely not blocking anything.
arbipher pushed a commit to arbipher/z3 that referenced this issue Apr 17, 2025
@NikolajBjorner @arbipher
fix Z3Prover#7616
9c9bcbb
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
1 participant
@jberdine
0