8000 Python Z3 api solver.check() crashes smt::cancel_exception when memory usage is higher than watermark · Issue #7629 · Z3Prover/z3 · GitHub
[go: up one dir, main page]
More Web Proxy on the site http://driver.im/
Skip to content

Python Z3 api solver.check() crashes smt::cancel_exception when memory usage is higher than watermark #7629

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
smoy opened this issue Apr 23, 2025 · 4 comments
Closed

Python Z3 api solver.check() crashes smt::cancel_exception when memory usage is higher than watermark #7629

smoy opened this issue Apr 23, 2025 · 4 comments

Comments

@smoy
Copy link
Contributor
smoy commented Apr 23, 2025

I am trying to isolate a smaller smt file to post

I set a memory_high_watermark_mb to control how much memory usage from Python side. During solver.check(), i did encounter the watermark being passed but instead of a z3. instead of check() termiantes with unknown, process actually crash with this on output

libc++abi: terminating due to uncaught exception of type smt::cancel_exception: smt-canceled
@smoy smoy changed the title Python Z3 api interaction with smt::cancel_exception Python Z3 api solver.check() crashes smt::cancel_exception when memory usage is higher than watermark Apr 23, 2025
@NikolajBjorner
Copy link
Contributor

this exception is thrown when internalizing expressions into the SMT solver.
there is one case in the SMT solver where it bails out on exceptions: if an exception is thrown during a scope pop.
If this is the source, then a way to address it is to disable throwing cancel_exception during the pop operation.
That is a minor code update.
It is more likely this isn't the root cause.
I use mixed-mode debugging of python from VS2022 to identify root causes.

@smoy
Copy link
Contributor Author
smoy commented Apr 23, 2025

@NikolajBjorner Your intuition is correct.

After enabling faulthandler.enabled(), i got the strace trace, it happens in the following

Current thread 0x00000001f3d44c80 (most recent call first):
  File "/Users/smoy/redacted/.venv/lib/python3.12/site-packages/z3/z3core.py", line 4164 in Z3_solver_push
  File "/Users/smoy/redacted/.venv/lib/python3.12/site-packages/z3/z3.py", line 7068 in push

this is in python3.12 on macos apple silicon

if solver.push went over memory watermark, can we catch and rethrow python z3 exception, so the caller can discard the solver, while continue to use the global context. (I have spawn a child process to handle z3 calculation via a process pool, so if can simply let the solver goes out of scope and create a new solver. all the while using the global context, then i don't have to perform additional process manipulation).

Thank you for your insight.

@NikolajBjorner
Copy link
Contributor

The wrapper in z3core.py (which is auto-generated) is supposed to check the error code and throw Z3Exception.
You say this is not the case.

@NikolajBjorner
Copy link
Contributor

I see the culprit;

api_util.h:#define Z3_CATCH_CORE(CODE) } catch (z3_exception & ex) { mk_c(c)->handle_exception(ex); CODE }

cancel_exception does not inherit from z3_excption but only std::exception

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
@smoy @NikolajBjorner
0