z3
z3 copied to clipboard
Z3Prover
4.12.2 intermittent crash on M1 macbook with python API
In the following code against 4.12.2, if parallel.enable is set to True, Python crashes the the below stack trace. When set to False, the code does not crash. My requirements.txt file includes z3-solver==4.12.2.0.
I have found if I include a "del ctx" at the end of the script, it crashes less frequently.
This is on a Macbook Pro (arm) with Python 3.11.4. I am running the script from the command line, though it happens in PyCharm too. It did not seem to be a problem with Z3 4.11.2.
import z3
print(z3.get_version_string())
z3.set_option(auto_config=True)
z3.set_option('parallel.enable', True)
ctx = z3.Context()
s = z3.SolverFor(logic="QF_FD", ctx=ctx)
s.set(model=False)
s.set(unsat_core=True)
s.set(':core.minimize', True)
s.set(':threads', 8)
a = z3.Bool('a', ctx)
s.add(a)
status = s.check()
assert(z3.sat == status)
% python3 z3_4_12_2_parallel_bug.py
4.12.2
Python(93047,0x16f913000) malloc: Corruption of free object 0x1398e8190: msizes 0/18 disagree
Python(93047,0x16f913000) malloc: *** set a breakpoint in malloc_error_break to debug
zsh: abort python3 z3_4_12_2_parallel_bug.py
-------------------------------------
Translated Report (Full Report Below)
-------------------------------------
Process: Python [93122]
Path: /opt/homebrew/*/Python.framework/Versions/3.11/Resources/Python.app/Contents/MacOS/Python
Identifier: org.python.python
Version: 3.11.4 (3.11.4)
Code Type: ARM-64 (Native)
Parent Process: zsh [92921]
Responsible: Terminal [16269]
User ID: 503
Date/Time: 2023-09-27 10:48:05.1818 -0700
OS Version: macOS 13.4.1 (22F770820d)
Report Version: 12
Anonymous UUID: DA07B1CF-17BD-9B34-E3C0-4AFAAD55F463
Sleep/Wake UUID: 438735E5-075C-4759-94EA-3DCD5147D947
Time Awake Since Boot: 1900000 seconds
Time Since Wake: 14819 seconds
System Integrity Protection: disabled
Crashed Thread: 0 Dispatch queue: com.apple.main-thread
Exception Type: EXC_CRASH (SIGABRT)
Exception Codes: 0x0000000000000000, 0x0000000000000000
Application Specific Information:
abort() called
Thread 0 Crashed:: Dispatch queue: com.apple.main-thread
0 libsystem_kernel.dylib 0x19f750724 __pthread_kill + 8
1 libsystem_pthread.dylib 0x19f787c28 pthread_kill + 288
2 libsystem_c.dylib 0x19f695ae8 abort + 180
3 libsystem_malloc.dylib 0x19f5b6e28 malloc_vreport + 908
4 libsystem_malloc.dylib 0x19f5cd5d4 malloc_zone_error + 104
5 libsystem_malloc.dylib 0x19f5cd354 _tiny_check_and_zero_inline_meta_from_freelist + 188
6 libsystem_malloc.dylib 0x19f5abea8 tiny_malloc_from_free_list + 440
7 libsystem_malloc.dylib 0x19f5ab670 tiny_malloc_should_clear + 216
8 libsystem_malloc.dylib 0x19f5aa24c szone_malloc_should_clear + 92
9 libz3.4.12.2.0.dylib 0x105f8ba58 memory::allocate(unsigned long) + 112
10 libz3.4.12.2.0.dylib 0x10607b0cc datatype::decl::plugin::u() const + 40
11 libz3.4.12.2.0.dylib 0x106079f88 datatype::decl::plugin::inherit(decl_plugin*, ast_translation&) + 912
12 libz3.4.12.2.0.dylib 0x1060578ec ast_manager::copy_families_plugins(ast_manager const&) + 280
13 libz3.4.12.2.0.dylib 0x1060579b8 ast_translation::ast_translation(ast_manager&, ast_manager&, bool) + 132
14 libz3.4.12.2.0.dylib 0x10634838c parallel_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) + 884
15 libz3.4.12.2.0.dylib 0x106214ce0 exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) + 68
16 libz3.4.12.2.0.dylib 0x106214f10 check_sat(tactic&, ref<goal>&, ref<model>&, labels_vec&, obj_ref<app, ast_manager>&, obj_ref<dependency_manager<ast_manager::expr_dependency_config>::dependency, ast_manager>&, std::__1::basic_string<char, std::__1::char_traits<char>, std::__1::allocator<char>>&) + 152
17 libz3.4.12.2.0.dylib 0x1063693c0 (anonymous namespace)::tactic2solver::check_sat_core2(unsigned int, expr* const*) + 604
18 libz3.4.12.2.0.dylib 0x10635241c solver_na2as::check_sat_core(unsigned int, expr* const*) + 84
19 libz3.4.12.2.0.dylib 0x106346ae4 combined_solver::check_sat_core(unsigned int, expr* const*) + 668
20 libz3.4.12.2.0.dylib 0x1063512e4 solver::check_sat(unsigned int, expr* const*) + 84
21 libz3.4.12.2.0.dylib 0x1068fb91c _solver_check(_Z3_context*, _Z3_solver*, unsigned int, _Z3_ast* const*) + 772
22 libz3.4.12.2.0.dylib 0x1068fbc34 Z3_solver_check_assumptions + 176
23 libffi.dylib 0x1af670050 ffi_call_SYSV + 80
24 libffi.dylib 0x1af678af8 ffi_call_int + 1208
If I run the script enough times, even with parallel.enable set to False, it will still sometimes crash like this. This is with or without the "del ctx" statement.
-------------------------------------
Translated Report (Full Report Below)
-------------------------------------
Process: Python [93450]
Path: /opt/homebrew/*/Python.framework/Versions/3.11/Resources/Python.app/Contents/MacOS/Python
Identifier: org.python.python
Version: 3.11.4 (3.11.4)
Code Type: ARM-64 (Native)
Parent Process: zsh [92921]
Responsible: Terminal [16269]
User ID: 503
Date/Time: 2023-09-27 10:50:46.4620 -0700
OS Version: macOS 13.4.1 (22F770820d)
Report Version: 12
Anonymous UUID: DA07B1CF-17BD-9B34-E3C0-4AFAAD55F463
Sleep/Wake UUID: 438735E5-075C-4759-94EA-3DCD5147D947
Time Awake Since Boot: 1900000 seconds
Time Since Wake: 14981 seconds
System Integrity Protection: disabled
Crashed Thread: 0 Dispatch queue: com.apple.main-thread
Exception Type: EXC_BREAKPOINT (SIGTRAP)
Exception Codes: 0x0000000000000001, 0x000000019f5ce174
Termination Reason: Namespace SIGNAL, Code 5 Trace/BPT trap: 5
Terminating Process: exc handler [93450]
Thread 0 Crashed:: Dispatch queue: com.apple.main-thread
0 libsystem_malloc.dylib 0x19f5ce174 tiny_free_list_remove_ptr.cold.2 + 0
1 libsystem_malloc.dylib 0x19f5aef34 tiny_free_list_remove_ptr + 412
2 libsystem_malloc.dylib 0x19f5ae458 tiny_free_no_lock + 436
3 libsystem_malloc.dylib 0x19f5ae120 free_tiny + 496
4 Python 0x103231e8c _PyObject_Free + 164
5 Python 0x103241c0c type_clear + 32
6 Python 0x10331e8dc gc_collect_main + 1708
7 Python 0x10331f550 _PyGC_CollectNoFail + 52
8 Python 0x1032fd41c finalize_modules + 1844
9 Python 0x1032fc9f4 Py_FinalizeEx + 428
10 Python 0x10331c004 Py_RunMain + 272
11 Python 0x10331d2ec Py_BytesMain + 40
12 dyld 0x19f42ff28 start + 2236
Based on some more experiementation, the issue might be more related to the line s.set(':threads', 8). If I comment that out, I am able to run the script many times without a crash.
"sat.threads" and "parallel.enable" are two different ways to parallelize search. Your stack suggests that core extraction doesn't work with sat.threads. It isn't mainstream use case so I can't say I am surprised it is acting up. It would require a repro setup to effectively debug this.
I had a similar issue, and it seems like replacing threading with multiprocessing can fix the issue, however your program will be a little different than with threading. If you don't want this, then use something like repl.it or trinket.io to run your program instead. You can also add queue to your program to make it work a bit better. Repl.it was what worked for me, and although the formatting is a tiny bit different, it's basically the same as using the program on a normal Python IDLE. Most of the time, it's the Macbook M1 deciding that the program is way too resource intensive, and things like Repl.it are ok with it. Hope this helps you out!
