ASSERT and python crashes

[smoy]

I am on macos arm and pip install z3-solver version 4.13.0.0. I am debugging how to deal with assertion segfault

 % pip freeze | grep z3
z3-solver==4.13.0.0

python
Python 3.11.6 (v3.11.6:8b6ee5ba3b, Oct  2 2023, 11:18:21) [Clang 13.0.0 (clang-1300.0.29.30)] on darwin
Type "help", "copyright", "credits" or "license" for more information.
>>> from z3 import *
>>> 
>>> solver = Solver()
>>> 
>>> A = SetSort(IntSort())
>>> B = SetSort(IntSort())
>>> 
>>> try:
...   solver.add(IsSubset(A, B) != (Union(A, B) == A))
... except Exception:
...   print("foobar")
... 
ASSERTION VIOLATION
File: ../src/ast/ast.cpp
Line: 388
UNEXPECTED CODE WAS REACHED.
Z3 4.13.0.0
Please file an issue with this message and more detail about how you encountered it at https://github.com/Z3Prover/z3/issues/new

The cited bug (https://github.com/Z3Prover/z3/issues/7158) is fixed but I want to understand in a production environment, when I don't want the assertion to crash the parent python interpreter. I want to catch it as an exception, so I can log the input the z3 solver and reprod. but it seems like the default is crashing the python intrepter without ability to catch exception.

[NikolajBjorner]

yes, the default here was to crash. The API code simply didn't perform sufficient parameter validation before entering internal operation. The API is required to perform sufficient parameter validation.

[smoy]

I am trying to reproduce locally on laptop but no luck yet. I receive report of the ASSERTION VIOLATION in a remote cluster running z3. My first thought is to catch the exception in python and then log the input to z3 only upon crashes. (it's tricky for me to log it ahead of time because of the amount of logs generated in normal run).

however, if the behavior of cpython extension is crashing, the python exception handler does not have a chance to handle it. is there facility within z3 to treat assertion violation as exception, such that the python intepreter can handle it (by logging the input only upon bad z3 input)

[NikolajBjorner]

A patch would be to redirect calls to exit in debug.h under the VERIFY and UNREACHABLE macros to a level of indirection that checks a Boolean flag that gets set by the API. But it is at best a patch, z3 is in an inconsistent state and may segfault for other reasons.