Skip to content
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

Segmentation fault while using python API solver.check() in linux #7117

Closed
rammohan02 opened this issue Feb 10, 2024 · 3 comments
Closed

Segmentation fault while using python API solver.check() in linux #7117

rammohan02 opened this issue Feb 10, 2024 · 3 comments

Comments

@rammohan02
Copy link

rammohan02 commented Feb 10, 2024 •
edited
Loading

Hello,

When I have too many variables (around 2^17) to be given to the solver, it results in "Program terminated with signal SIGSEGV, Segmentation fault.". I have tried the same test case in Windows and it is running without any segmentation fault. I am using python 3.10 in linux (Ubuntu) and python 3.11 in windows.

This is the gdb trace for the core dump:

GNU gdb (GDB) 11.2
Copyright (C) 2022 Free Software Foundation, Inc.
License GPLv3+: GNU GPL version 3 or later <http://gnu.org/licenses/gpl.html>
This is free software: you are free to change and redistribute it.
There is NO WARRANTY, to the extent permitted by law.
Type "show copying" and "show warranty" for details.
This GDB was configured as "x86_64-conda-linux-gnu".
Type "show configuration" for configuration details.
For bug reporting instructions, please see:
<https://www.gnu.org/software/gdb/bugs/>.
Find the GDB manual and other documentation resources online at:
    <http://www.gnu.org/software/gdb/documentation/>.

For help, type "help".
Type "apropos word" to search for commands related to "word"...
Reading symbols from python...

warning: core file may not match specified executable file.
[New LWP 119110]
[New LWP 16150]
[Thread debugging using libthread_db enabled]
Using host libthread_db library "/lib64/libthread_db.so.1".
Core was generated by `python smt_pattern_heu_routing.py'.
Program terminated with signal SIGSEGV, Segmentation fault.

#0  0x00002ac1786c0b90 in ast_manager::register_node_core(ast*) () from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#1  0x00002ac1786c70b3 in ast_manager::mk_app_core(func_decl*, unsigned int, expr* const*) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#2  0x00002ac1782a6ace in rewriter_tpl<(anonymous namespace)::th_rewriter_cfg>::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#3  0x00002ac1782a8a85 in th_rewriter::operator()(expr*, obj_ref<expr, ast_manager>&, obj_ref<app, ast_manager>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#4  0x00002ac177f3430a in (anonymous namespace)::propagate_values_tactic::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#5  0x00002ac1780fbaac in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#6  0x00002ac1780fc06a in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#7  0x00002ac1780fc06a in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#8  0x00002ac1780fc06a in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#9  0x00002ac1780f9b3c in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#10 0x00002ac1780fc06a in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#11 0x00002ac1780fc06a in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#12 0x00002ac1780fc06a in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#13 0x00002ac1780f92c4 in annotate_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#14 0x00002ac1780f9ad4 in or_else_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#15 0x00002ac1780fc06a in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#16 0x00002ac1780fc06a in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#17 0x00002ac1780fc06a in and_then_tactical::operator()(ref<goal> const&, sref_buffer<goal, 16u>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#18 0x00002ac178100617 in exec(tactic&, ref<goal> const&, sref_buffer<goal, 16u>&) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#19 0x00002ac178100c0a in 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::string&) () from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#20 0x00002ac178084c2a in (anonymous namespace)::tactic2solver::check_sat_core2(unsigned int, expr* const*) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#21 0x00002ac17806a5f2 in solver_na2as::check_sat_core(unsigned int, expr* const*) ()
   from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#22 0x00002ac17805e5f4 in solver::check_sat(unsigned int, expr* const*) () from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#23 0x00002ac1774cbe1c in _solver_check () from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#24 0x00002ac1774ccadd in Z3_solver_check_assumptions () from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/lib/libz3.so
#25 0x00002ac16fba6052 in ffi_call_unix64 () from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/lib-dynload/../../libffi.so.8
#26 0x00002ac16fba4925 in ffi_call_int () from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/lib-dynload/../../libffi.so.8
#27 0x00002ac16fba506e in ffi_call () from /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/lib-dynload/../../libffi.so.8
#28 0x00002ac16fa791e7 in _call_function_pointer (argtypecount=<optimized out>, argcount=4, resmem=0x7ffc420be120, restype=<optimized out>, atypes=<optimized out>,
    avalues=<optimized out>, pProc=0x2ac1774cca90 <Z3_solver_check_assumptions>, flags=4353) at /usr/local/src/conda/python-3.10.13/Modules/_ctypes/callproc.c:916
#29 _ctypes_callproc (pProc=0x2ac1774cca90 <Z3_solver_check_assumptions>,
    argtuple=(<ContextObj at remote 0x2ac177232e40>, <SolverObj at remote 0x2ac17ae49fc0>, 0, <Ast_Array_0 at remote 0x2ac17ae37f40>), flags=4353,
    argtypes=<optimized out>, restype=<_ctypes.PyCSimpleType at remote 0x1f5b710>, checker=0x0) at /usr/local/src/conda/python-3.10.13/Modules/_ctypes/callproc.c:1262
#30 0x00002ac16fa8223e in PyCFuncPtr_call (self=<optimized out>, inargs=<optimized out>, kwds=0x0) at /usr/local/src/conda/python-3.10.13/Modules/_ctypes/_ctypes.c:4221
#31 0x00000000004f614b in _PyObject_MakeTpCall (tstate=0x1e34730, callable=<_FuncPtr(__name__='Z3_solver_check_assumptions') at remote 0x2ac178edc580>,
--Type <RET> for more, q to quit, c to continue without paging--c
    args=<optimized out>, nargs=<optimized out>, keywords=0x0) at /usr/local/src/conda/python-3.10.13/Objects/call.c:215
#32 0x00000000004f2376 in _PyObject_VectorcallTstate (kwnames=0x0, nargsf=<optimized out>, args=0x2ac1770db660, callable=<_FuncPtr(__name__='Z3_solver_check_assumptions') at remote 0x2ac178edc580>, tstate=<optimized out>) at /usr/local/src/conda/python-3.10.13/Include/cpython/abstract.h:112
#33 _PyObject_VectorcallTstate (kwnames=0x0, nargsf=<optimized out>, args=0x2ac1770db660, callable=<_FuncPtr(__name__='Z3_solver_check_assumptions') at remote 0x2ac178edc580>, tstate=<optimized out>) at /usr/local/src/conda/python-3.10.13/Include/cpython/abstract.h:99
#34 PyObject_Vectorcall (kwnames=0x0, nargsf=<optimized out>, args=0x2ac1770db660, callable=<_FuncPtr(__name__='Z3_solver_check_assumptions') at remote 0x2ac178edc580>) at /usr/local/src/conda/python-3.10.13/Include/cpython/abstract.h:123
#35 call_function (kwnames=0x0, oparg=<optimized out>, pp_stack=<synthetic pointer>, trace_info=0x7ffc420be470, tstate=<optimized out>) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:5893
#36 _PyEval_EvalFrameDefault (tstate=<optimized out>, f=Frame 0x2ac1770db4c0, for file /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/z3core.py, line 4235, in Z3_solver_check_assumptions (a0=<ContextObj at remote 0x2ac177232e40>, a1=<SolverObj at remote 0x2ac17ae49fc0>, a2=0, a3=<Ast_Array_0 at remote 0x2ac17ae37f40>, _elems=<Elementaries(f=<_FuncPtr(__name__='Z3_solver_check_assumptions') at remote 0x2ac178edc580>, get_error_code=<_FuncPtr(__name__='Z3_get_error_code') at remote 0x2ac178ebaec0>, get_error_message=<_FuncPtr(__name__='Z3_get_error_msg') at remote 0x2ac178ebb040>, OK=0, Exception=<type at remote 0x201a120>) at remote 0x2ac178f2b130>), throwflag=<optimized out>) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:4181
#37 0x00000000004fcadf in _PyEval_EvalFrame (throwflag=0, f=Frame 0x2ac1770db4c0, for file /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/z3core.py, line 4235, in Z3_solver_check_assumptions (a0=<ContextObj at remote 0x2ac177232e40>, a1=<SolverObj at remote 0x2ac17ae49fc0>, a2=0, a3=<Ast_Array_0 at remote 0x2ac17ae37f40>, _elems=<Elementaries(f=<_FuncPtr(__name__='Z3_solver_check_assumptions') at remote 0x2ac178edc580>, get_error_code=<_FuncPtr(__name__='Z3_get_error_code') at remote 0x2ac178ebaec0>, get_error_message=<_FuncPtr(__name__='Z3_get_error_msg') at remote 0x2ac178ebb040>, OK=0, Exception=<type at remote 0x201a120>) at remote 0x2ac178f2b130>), tstate=0x1e34730) at /usr/local/src/conda/python-3.10.13/Include/internal/pycore_ceval.h:46
#38 _PyEval_Vector (kwnames=<optimized out>, argcount=<optimized out>, args=<optimized out>, locals=0x0, con=0x2ac178f305f0, tstate=0x1e34730) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:5067
#39 _PyFunction_Vectorcall (func=<function at remote 0x2ac178f305e0>, stack=<optimized out>, nargsf=<optimized out>, kwnames=<optimized out>) at /usr/local/src/conda/python-3.10.13/Objects/call.c:342
#40 0x00000000004ed2bf in _PyObject_VectorcallTstate (kwnames=0x0, nargsf=<optimized out>, args=0x2ac1770db480, callable=<function at remote 0x2ac178f305e0>, tstate=0x1e34730) at /usr/local/src/conda/python-3.10.13/Include/cpython/abstract.h:114
#41 PyObject_Vectorcall (kwnames=0x0, nargsf=<optimized out>, args=0x2ac1770db480, callable=<function at remote 0x2ac178f305e0>) at /usr/local/src/conda/python-3.10.13/Include/cpython/abstract.h:123
#42 call_function (kwnames=0x0, oparg=<optimized out>, pp_stack=<synthetic pointer>, trace_info=0x7ffc420be630, tstate=<optimized out>) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:5893
#43 _PyEval_EvalFrameDefault (tstate=<optimized out>, f=Frame 0x2ac1770db2e0, for file /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/z3.py, line 7174, in check (self=<Solver(ctx=<Context(ctx=<ContextObj at remote 0x2ac177232e40>, owner=True, eh=<CFunctionType at remote 0x2ac178f69000>) at remote 0x2ac178f93940>, backtrack_level=4000000000, solver=<SolverObj at remote 0x2ac17ae49fc0>) at remote 0x2ac17ae07b80>, assumptions=(), s=<BoolSortRef(ast=<Sort at remote 0x2ac17ae37d40>, ctx=<...>) at remote 0x2ac17ae473a0>, num=0, _assumptions=<Ast_Array_0 at remote 0x2ac17ae37f40>), throwflag=<optimized out>) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:4213
#44 0x00000000004fcadf in _PyEval_EvalFrame (throwflag=0, f=Frame 0x2ac1770db2e0, for file /home/jmayank/anaconda3/envs/ethernet_env/lib/python3.10/site-packages/z3/z3.py, line 7174, in check (self=<Solver(ctx=<Context(ctx=<ContextObj at remote 0x2ac177232e40>, owner=True, eh=<CFunctionType at remote 0x2ac178f69000>) at remote 0x2ac178f93940>, backtrack_level=4000000000, solver=<SolverObj at remote 0x2ac17ae49fc0>) at remote 0x2ac17ae07b80>, assumptions=(), s=<BoolSortRef(ast=<Sort at remote 0x2ac17ae37d40>, ctx=<...>) at remote 0x2ac17ae473a0>, num=0, _assumptions=<Ast_Array_0 at remote 0x2ac17ae37f40>), tstate=0x1e34730) at /usr/local/src/conda/python-3.10.13/Include/internal/pycore_ceval.h:46
#45 _PyEval_Vector (kwnames=<optimized out>, argcount=<optimized out>, args=<optimized out>, locals=0x0, con=0x2ac178fff6e0, tstate=0x1e34730) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:5067
#46 _PyFunction_Vectorcall (func=<function at remote 0x2ac178fff6d0>, stack=<optimized out>, nargsf=<optimized out>, kwnames=<optimized out>) at /usr/local/src/conda/python-3.10.13/Objects/call.c:342
#47 0x00000000004ed6d1 in _PyObject_VectorcallTstate (kwnames=0x0, nargsf=<optimized out>, args=0x211e118, callable=<function at remote 0x2ac178fff6d0>, tstate=0x1e34730) at /usr/local/src/conda/python-3.10.13/Include/cpython/abstract.h:114
#48 PyObject_Vectorcall (kwnames=0x0, nargsf=<optimized out>, args=0x211e118, callable=<function at remote 0x2ac178fff6d0>) at /usr/local/src/conda/python-3.10.13/Include/cpython/abstract.h:123
#49 call_function (kwnames=0x0, oparg=<optimized out>, pp_stack=<synthetic pointer>, trace_info=0x7ffc420be7f0, tstate=<optimized out>) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:5893
#50 _PyEval_EvalFrameDefault (tstate=<optimized out>, f=Frame 0x211de00, for file /home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py, line 189, in solve (msgInputs={8: [[1, 5, 5, 200, 2, 5], [2, 5, 7, 200, 2, 6]]}, ETHERNET_MAX_PAYLOAD=1500, networkInputs={1: ['v1', 0, 1, 1, 0, 0, 0, 0, 0, 0, 0], 2: ['v2', 1, 0, 0, 1, 1, 0, 0, 0, 0, 0], 3: ['v3', 1, 0, 0, 0, 1, 0, 0, 0, 0, 0], 4: ['v4', 0, 1, 0, 0, 0, 1, 1, 0, 0, 0], 5: ['v5', 0, 1, 1, 0, 0, 0, 1, 0, 0, 0], 6: ['v6', 0, 0, 0, 1, 0, 0, 0, 1, 1, 0], 7: ['v7', 0, 0, 0, 1, 1, 0, 0, 0, 1, 0], 8: ['v8', 0, 0, 0, 0, 0, 1, 0, 0, 0, 1], 9: ['v9', 0, 0, 0, 0, 0, 1, 1, 0, 0, 1], 10: ['v10', 0, 0, 0, 0, 0, 0, 0, 1, 1, 0]}, td=<float at remote 0x2ac16fb99c50>, fd=<float at remote 0x2ac17721ccf0>, START_TIME=<float at remote 0x2ac178f8d010>, distinctGateWays=<dict_keys at remote 0x2ac176fc9960>, N_can=1, F_i_CAN={8: 2}, H_i={8: 1050}, HPrime_i={8: 1050}, J_i_c={8: {1: 25, 2: 42}}, M_ic={8: {1: 210, 2: 150}}, j_i={8: 210}, h_i={8: 5}, des_i={8: 5}, distinctVertices=<dict_keys at remote 0x2ac...(truncated), throwflag=<optimized out>) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:4198
#51 0x00000000004fcadf in _PyEval_EvalFrame (throwflag=0, f=Frame 0x211de00, for file /home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py, line 189, in solve (msgInputs={8: [[1, 5, 5, 200, 2, 5], [2, 5, 7, 200, 2, 6]]}, ETHERNET_MAX_PAYLOAD=1500, networkInputs={1: ['v1', 0, 1, 1, 0, 0, 0, 0, 0, 0, 0], 2: ['v2', 1, 0, 0, 1, 1, 0, 0, 0, 0, 0], 3: ['v3', 1, 0, 0, 0, 1, 0, 0, 0, 0, 0], 4: ['v4', 0, 1, 0, 0, 0, 1, 1, 0, 0, 0], 5: ['v5', 0, 1, 1, 0, 0, 0, 1, 0, 0, 0], 6: ['v6', 0, 0, 0, 1, 0, 0, 0, 1, 1, 0], 7: ['v7', 0, 0, 0, 1, 1, 0, 0, 0, 1, 0], 8: ['v8', 0, 0, 0, 0, 0, 1, 0, 0, 0, 1], 9: ['v9', 0, 0, 0, 0, 0, 1, 1, 0, 0, 1], 10: ['v10', 0, 0, 0, 0, 0, 0, 0, 1, 1, 0]}, td=<float at remote 0x2ac16fb99c50>, fd=<float at remote 0x2ac17721ccf0>, START_TIME=<float at remote 0x2ac178f8d010>, distinctGateWays=<dict_keys at remote 0x2ac176fc9960>, N_can=1, F_i_CAN={8: 2}, H_i={8: 1050}, HPrime_i={8: 1050}, J_i_c={8: {1: 25, 2: 42}}, M_ic={8: {1: 210, 2: 150}}, j_i={8: 210}, h_i={8: 5}, des_i={8: 5}, distinctVertices=<dict_keys at remote 0x2ac...(truncated), tstate=0x1e34730) at /usr/local/src/conda/python-3.10.13/Include/internal/pycore_ceval.h:46
#52 _PyEval_Vector (kwnames=<optimized out>, argcount=<optimized out>, args=<optimized out>, locals=0x0, con=0x2ac176fa5e20, tstate=0x1e34730) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:5067
#53 _PyFunction_Vectorcall (func=<function at remote 0x2ac176fa5e10>, stack=<optimized out>, nargsf=<optimized out>, kwnames=<optimized out>) at /usr/local/src/conda/python-3.10.13/Objects/call.c:342
#54 0x00000000004ed2bf in _PyObject_VectorcallTstate (kwnames=0x0, nargsf=<optimized out>, args=0x20675f0, callable=<function at remote 0x2ac176fa5e10>, tstate=0x1e34730) at /usr/local/src/conda/python-3.10.13/Include/cpython/abstract.h:114
#55 PyObject_Vectorcall (kwnames=0x0, nargsf=<optimized out>, args=0x20675f0, callable=<function at remote 0x2ac176fa5e10>) at /usr/local/src/conda/python-3.10.13/Include/cpython/abstract.h:123
#56 call_function (kwnames=0x0, oparg=<optimized out>, pp_stack=<synthetic pointer>, trace_info=0x7ffc420be9b0, tstate=<optimized out>) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:5893
#57 _PyEval_EvalFrameDefault (tstate=<optimized out>, f=Frame 0x20673e0, for file /home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py, line 354, in main (START=<float at remote 0x2ac178f8d030>, CANInputFilesFolderPath='../../inputs/', CANInputFileEntries=<posix.ScandirIterator at remote 0x2ac17725ad40>, CANInputFiles=['../../input_messages_failing_smt.txt'], fileVsExecutionResult={}, successFileCount=0, totalFileCount=1, file='../../input_messages_failing_smt.txt', msgInputFile='../../input_messages_failing_smt.txt', msgInputs=[[8, 5, 5, 200, 2, 5], [8, 5, 7, 200, 2, 6]], modifiedMsgInputs={8: [[1, 5, 5, 200, 2, 5], [2, 5, 7, 200, 2, 6]]}, ETHERNET_MAXPAYLOAD=1500, networkInputFile='../../network_input.txt', networkInputs=[['v1', '0', '1', '1', '0', '0', '0', '0', '0', '0', '0'], ['v2', '1', '0', '0', '1', '1', '0', '0', '0', '0', '0'], ['v3', '1', '0', '0', '0', '1', '0', '0', '0', '0', '0'], ['v4', '0', '1', '0', '0', '0', '1', '1', '0', '0', '0'], ['v5', '0', '1', '1', '0', '0', '0', '1', '0', '0', '0'], ['v6', '0', '0', '0'...(truncated), throwflag=<optimized out>) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:4213
#58 0x00000000004fcadf in _PyEval_EvalFrame (throwflag=0, f=Frame 0x20673e0, for file /home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py, line 354, in main (START=<float at remote 0x2ac178f8d030>, CANInputFilesFolderPath='../../inputs/', CANInputFileEntries=<posix.ScandirIterator at remote 0x2ac17725ad40>, CANInputFiles=['../../input_messages_failing_smt.txt'], fileVsExecutionResult={}, successFileCount=0, totalFileCount=1, file='../../input_messages_failing_smt.txt', msgInputFile='../../input_messages_failing_smt.txt', msgInputs=[[8, 5, 5, 200, 2, 5], [8, 5, 7, 200, 2, 6]], modifiedMsgInputs={8: [[1, 5, 5, 200, 2, 5], [2, 5, 7, 200, 2, 6]]}, ETHERNET_MAXPAYLOAD=1500, networkInputFile='../../network_input.txt', networkInputs=[['v1', '0', '1', '1', '0', '0', '0', '0', '0', '0', '0'], ['v2', '1', '0', '0', '1', '1', '0', '0', '0', '0', '0'], ['v3', '1', '0', '0', '0', '1', '0', '0', '0', '0', '0'], ['v4', '0', '1', '0', '0', '0', '1', '1', '0', '0', '0'], ['v5', '0', '1', '1', '0', '0', '0', '1', '0', '0', '0'], ['v6', '0', '0', '0'...(truncated), tstate=0x1e34730) at /usr/local/src/conda/python-3.10.13/Include/internal/pycore_ceval.h:46
#59 _PyEval_Vector (kwnames=<optimized out>, argcount=<optimized out>, args=<optimized out>, locals=0x0, con=0x2ac179029760, tstate=0x1e34730) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:5067
#60 _PyFunction_Vectorcall (func=<function at remote 0x2ac179029750>, stack=<optimized out>, nargsf=<optimized out>, kwnames=<optimized out>) at /usr/local/src/conda/python-3.10.13/Objects/call.c:342
#61 0x00000000004ed2bf in _PyObject_VectorcallTstate (kwnames=0x0, nargsf=<optimized out>, args=0x2ac16fac5ba8, callable=<function at remote 0x2ac179029750>, tstate=0x1e34730) at /usr/local/src/conda/python-3.10.13/Include/cpython/abstract.h:114
#62 PyObject_Vectorcall (kwnames=0x0, nargsf=<optimized out>, args=0x2ac16fac5ba8, callable=<function at remote 0x2ac179029750>) at /usr/local/src/conda/python-3.10.13/Include/cpython/abstract.h:123
#63 call_function (kwnames=0x0, oparg=<optimized out>, pp_stack=<synthetic pointer>, trace_info=0x7ffc420beb70, tstate=<optimized out>) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:5893
#64 _PyEval_EvalFrameDefault (tstate=<optimized out>, f=Frame 0x2ac16fac5a40, for file /home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py, line 376, in <module> (), throwflag=<optimized out>) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:4213
#65 0x0000000000591d92 in _PyEval_EvalFrame (throwflag=0, f=Frame 0x2ac16fac5a40, for file /home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py, line 376, in <module> (), tstate=0x1e34730) at /usr/local/src/conda/python-3.10.13/Include/internal/pycore_ceval.h:46
#66 _PyEval_Vector (tstate=0x1e34730, con=<optimized out>, locals=<optimized out>, args=<optimized out>, argcount=<optimized out>, kwnames=<optimized out>) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:5067
#67 0x0000000000591cd7 in PyEval_EvalCode (co=co@entry=<code at remote 0x2ac176f496e0>, globals=globals@entry={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py') at remote 0x2ac176ec1180>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x2ac16fb34900>, '__file__': '/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py', '__cached__': None, 'z3types': <module at remote 0x2ac1771f9f80>, 'z3consts': <module at remote 0x2ac177218400>, 'z3core': <module at remote 0x2ac177065b70>, 'z3printer': <module at remote 0x2ac1770f7c40>, 'z3': <module at remote 0x2ac176fc4360>, 'atexit': <module at remote 0x2ac177089850>, 'sys': <module at remote 0x2ac16fb1e390>, 'os': <module at remote 0x2ac176ee4540>, 'contextlib': <module at remote 0x2ac176f3a4d0>, 'ctypes': <module at remote 0x2ac177089800>, 'importlib_resources': <module at remote 0x2ac177089f80>, 'Z3Exception': <type at remote 0x201a120>, 'ContextObj': <_ctypes...(truncated), locals=locals@entry={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py') at remote 0x2ac176ec1180>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x2ac16fb34900>, '__file__': '/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py', '__cached__': None, 'z3types': <module at remote 0x2ac1771f9f80>, 'z3consts': <module at remote 0x2ac177218400>, 'z3core': <module at remote 0x2ac177065b70>, 'z3printer': <module at remote 0x2ac1770f7c40>, 'z3': <module at remote 0x2ac176fc4360>, 'atexit': <module at remote 0x2ac177089850>, 'sys': <module at remote 0x2ac16fb1e390>, 'os': <module at remote 0x2ac176ee4540>, 'contextlib': <module at remote 0x2ac176f3a4d0>, 'ctypes': <module at remote 0x2ac177089800>, 'importlib_resources': <module at remote 0x2ac177089f80>, 'Z3Exception': <type at remote 0x201a120>, 'ContextObj': <_ctypes...(truncated)) at /usr/local/src/conda/python-3.10.13/Python/ceval.c:1134
#68 0x00000000005c2967 in run_eval_code_obj (tstate=0x1e34730, co=0x2ac176f496e0, globals={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py') at remote 0x2ac176ec1180>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x2ac16fb34900>, '__file__': '/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py', '__cached__': None, 'z3types': <module at remote 0x2ac1771f9f80>, 'z3consts': <module at remote 0x2ac177218400>, 'z3core': <module at remote 0x2ac177065b70>, 'z3printer': <module at remote 0x2ac1770f7c40>, 'z3': <module at remote 0x2ac176fc4360>, 'atexit': <module at remote 0x2ac177089850>, 'sys': <module at remote 0x2ac16fb1e390>, 'os': <module at remote 0x2ac176ee4540>, 'contextlib': <module at remote 0x2ac176f3a4d0>, 'ctypes': <module at remote 0x2ac177089800>, 'importlib_resources': <module at remote 0x2ac177089f80>, 'Z3Exception': <type at remote 0x201a120>, 'ContextObj': <_ctypes...(truncated), locals={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py') at remote 0x2ac176ec1180>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x2ac16fb34900>, '__file__': '/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py', '__cached__': None, 'z3types': <module at remote 0x2ac1771f9f80>, 'z3consts': <module at remote 0x2ac177218400>, 'z3core': <module at remote 0x2ac177065b70>, 'z3printer': <module at remote 0x2ac1770f7c40>, 'z3': <module at remote 0x2ac176fc4360>, 'atexit': <module at remote 0x2ac177089850>, 'sys': <module at remote 0x2ac16fb1e390>, 'os': <module at remote 0x2ac176ee4540>, 'contextlib': <module at remote 0x2ac176f3a4d0>, 'ctypes': <module at remote 0x2ac177089800>, 'importlib_resources': <module at remote 0x2ac177089f80>, 'Z3Exception': <type at remote 0x201a120>, 'ContextObj': <_ctypes...(truncated)) at /usr/local/src/conda/python-3.10.13/Python/pythonrun.c:1291
#69 0x00000000005bdad0 in run_mod (mod=<optimized out>, filename=<optimized out>, globals={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py') at remote 0x2ac176ec1180>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x2ac16fb34900>, '__file__': '/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py', '__cached__': None, 'z3types': <module at remote 0x2ac1771f9f80>, 'z3consts': <module at remote 0x2ac177218400>, 'z3core': <module at remote 0x2ac177065b70>, 'z3printer': <module at remote 0x2ac1770f7c40>, 'z3': <module at remote 0x2ac176fc4360>, 'atexit': <module at remote 0x2ac177089850>, 'sys': <module at remote 0x2ac16fb1e390>, 'os': <module at remote 0x2ac176ee4540>, 'contextlib': <module at remote 0x2ac176f3a4d0>, 'ctypes': <module at remote 0x2ac177089800>, 'importlib_resources': <module at remote 0x2ac177089f80>, 'Z3Exception': <type at remote 0x201a120>, 'ContextObj': <_ctypes...(truncated), locals={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py') at remote 0x2ac176ec1180>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x2ac16fb34900>, '__file__': '/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py', '__cached__': None, 'z3types': <module at remote 0x2ac1771f9f80>, 'z3consts': <module at remote 0x2ac177218400>, 'z3core': <module at remote 0x2ac177065b70>, 'z3printer': <module at remote 0x2ac1770f7c40>, 'z3': <module at remote 0x2ac176fc4360>, 'atexit': <module at remote 0x2ac177089850>, 'sys': <module at remote 0x2ac16fb1e390>, 'os': <module at remote 0x2ac176ee4540>, 'contextlib': <module at remote 0x2ac176f3a4d0>, 'ctypes': <module at remote 0x2ac177089800>, 'importlib_resources': <module at remote 0x2ac177089f80>, 'Z3Exception': <type at remote 0x201a120>, 'ContextObj': <_ctypes...(truncated), flags=<optimized out>, arena=<optimized out>) at /usr/local/src/conda/python-3.10.13/Python/pythonrun.c:1312
#70 0x000000000045956b in pyrun_file (fp=<optimized out>, filename=<optimized out>, start=<optimized out>, globals=<optimized out>, locals=<optimized out>, closeit=<optimized out>, flags=0x7ffc420bee68) at /usr/local/src/conda/python-3.10.13/Python/pythonrun.c:1208
#71 0x00000000005b805f in _PyRun_SimpleFileObject (fp=0x1ebf900, filename='/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py', closeit=1, flags=0x7ffc420bee68) at /usr/local/src/conda/python-3.10.13/Python/pythonrun.c:456
#72 0x00000000005b7dc3 in _PyRun_AnyFileObject (fp=0x1ebf900, filename='/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py', closeit=1, flags=0x7ffc420bee68) at /usr/local/src/conda/python-3.10.13/Python/pythonrun.c:90
#73 0x00000000005b4b7d in pymain_run_file_obj (skip_source_first_line=0, filename='/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing.py', program_name='python') at /usr/local/src/conda/python-3.10.13/Modules/main.c:357
#74 pymain_run_file (config=0x1e18bb0) at /usr/local/src/conda/python-3.10.13/Modules/main.c:376
#75 pymain_run_python (exitcode=0x7ffc420bee60) at /usr/local/src/conda/python-3.10.13/Modules/main.c:591
#76 Py_RunMain () at /usr/local/src/conda/python-3.10.13/Modules/main.c:670
#77 0x0000000000584e49 in Py_BytesMain (argc=<optimized out>, argv=<optimized out>) at /usr/local/src/conda/python-3.10.13/Modules/main.c:1090
#78 0x00002ac1705b1555 in __libc_start_main () from /lib64/libc.so.6
#79 0x0000000000584cfe in _start ()

I am sure that this is not the memory issue. Is it a known problem when the number of variables are too high? I can share a minimal code reproducing the problem if needed.

Edited: In addition, these are the logs I got by adding faulthandler.enable() to python code

Fatal Python error: Segmentation fault

Current thread 0x00007ff7a4a63740 (most recent call first):
  File "/home/jmayank/anaconda3/envs/ethernet_py_311/lib/python3.11/site-packages/z3/z3core.py", line 4235 in Z3_solver_check_assumptions
  File "/home/jmayank/anaconda3/envs/ethernet_py_311/lib/python3.11/site-packages/z3/z3.py", line 7174 in check
  File "/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing_v2.py", line 243 in solve
  File "/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing_v2.py", line 407 in main
  File "/home/jmayank/Ram/Ethernet/hybridCode/smt_pattern_heu_routing/smt_pattern_heu_routing_v2.py", line 427 in <module>
Segmentation fault (core dumped)

Thank you
NikolajBjorner added a commit that referenced this issue Feb 14, 2024
@NikolajBjorner
#7117
2b14793 
probably overflow of unsigned for large capacity
NikolajBjorner added a commit that referenced this issue Feb 21, 2024
@NikolajBjorner
#7117
98d1554 
probably overflow of unsigned for large capacity
@NikolajBjorner
Copy link
Contributor

does it repro?

@rammohan02
Copy link
Author

rammohan02 commented Feb 23, 2024 •
edited
Loading

Should i use the same version of z3-solver "4.12.5.0" to test?

@rammohan02
Copy link
Author

Issue is resolved with later z3-solver version (i.e., 4.12.6.0)

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
@NikolajBjorner @rammohan02