Segmentation fault with satisfy_one function call on a large boolean expression

[azewiusz]

I do not have much to show as expression is in size of several GB but found out this GDB / Python trace that I would like to understand: It fails teh same on Windows 10 machine and on Linux one (Ubuntu) _Linux dev 6.8.0-35-generic #35-Ubuntu SMP PREEMPT_DYNAMIC Mon May 20 15:51:52 UTC 2024 x86_64 x86_64 x8664 GNU/Linux

Thread 1 "python3.11" received signal SIGSEGV, Segmentation fault.
Downloading source file /build/python3.11-khintT/python3.11-3.11.9/build-static/../Objects/obmalloc.c
0x000000000051cd33 in pymalloc_alloc (ctx=<optimized out>, nbytes=32)           
    at ../Objects/obmalloc.c:1979
warning: 1979   ../Objects/obmalloc.c: No such file or directory
(gdb) bt
#0  0x000000000051cd33 in pymalloc_alloc (ctx=<optimized out>, nbytes=32)
    at ../Objects/obmalloc.c:1979
#1  _PyObject_Malloc (nbytes=32, ctx=<optimized out>)
    at ../Objects/obmalloc.c:1998
#2  PyMem_Malloc (size=32) at ../Objects/obmalloc.c:623
#3  0x00007ffff7bd8357 in new (ps=ps@entry=0x2cdab00, size=size@entry=32)
    at thirdparty/picosat/picosat.c:949
#4  0x00007ffff7bdb6d6 in new_clause (learned=1, size=1, ps=<optimized out>)
    at thirdparty/picosat/picosat.c:1292
#5  add_simplified_clause (ps=ps@entry=0x2cdab00, learned=learned@entry=1)
    at thirdparty/picosat/picosat.c:2345
#6  0x00007ffff7bda09b in resolve_top_level_unit (reason=0x2cdab70, 
    lit=0x1a1327820, ps=<optimized out>) at thirdparty/picosat/picosat.c:1890
#7  assign_forced (ps=ps@entry=0x2cdab00, lit=0x1a1327820, reason=0x2cdab70)
    at thirdparty/picosat/picosat.c:1975
#8  0x00007ffff7bdbc0d in prop2 (this=0x1a1327825, ps=0x2cdab00)
    at thirdparty/picosat/picosat.c:3895
#9  bcp (ps=ps@entry=0x2cdab00) at thirdparty/picosat/picosat.c:4299
#10 0x00007ffff7be21b7 in bcp (ps=0x2cdab00)
    at thirdparty/picosat/picosat.c:4291
#11 sat (l=-1, ps=0x2cdab00) at thirdparty/picosat/picosat.c:5868
#12 picosat_sat (ps=ps@entry=0x2cdab00, l=-1)
    at thirdparty/picosat/picosat.c:7109
--Type <RET> for more, q to quit, c to continue without paging--
#13 0x00007ffff7bd7dfb in _satisfy_one (self=<optimized out>, 
    args=<optimized out>, kwargs=<optimized out>)
    at pyeda/boolalg/picosatmodule.c:383
#14 0x000000000055394b in cfunction_call (
    func=<built-in method satisfy_one of module object at remote 0x7ffff73938d0>, args=<optimized out>, kwargs=<optimized out>)
    at ../Objects/methodobject.c:542
#15 0x000000000052e6d3 in _PyObject_MakeTpCall (
    tstate=0xa53198 <_PyRuntime+166328>, 
    callable=<built-in method satisfy_one of module object at remote 0x7ffff73938d0>, args=<optimized out>, nargs=<optimized out>, keywords=0x0)
    at ../Objects/call.c:214
#16 0x000000000053bf0d in _PyEval_EvalFrameDefault (tstate=<optimized out>, 
    frame=<optimized out>, throwflag=<optimized out>) at ../Python/ceval.c:4769
#17 0x000000000060eb9d in _PyEval_EvalFrame (throwflag=0, 
    frame=0x7ffff7fb2020, tstate=0xa53198 <_PyRuntime+166328>)
    at ../Include/internal/pycore_ceval.h:73
#18 _PyEval_Vector (tstate=tstate@entry=0xa53198 <_PyRuntime+166328>, 
    func=func@entry=0x7ffff7415ee0, 
    locals=locals@entry={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__fi--Type <RET> for more, q to quit, c to continue without paging--
le__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``, a singleton that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated), args=args@entry=0x0, argcount=argcount@entry=0, 
    kwnames=kwnames@entry=0x0) at ../Python/ceval.c:6434
#19 0x000000000060e348 in PyEval_EvalCode (co=<code at remote 0xe16480>, 
    globals=<optimized out>, 
    locals={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__file__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``, a singleton--Type <RET> for more, q to quit, c to continue without paging--
 that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated)) at ../Python/ceval.c:1148
#20 0x000000000062d9cc in run_eval_code_obj (
    tstate=0xa53198 <_PyRuntime+166328>, co=0xe16480, 
    globals={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__file__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``, a singleton that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated), 
    locals={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotatio--Type <RET> for more, q to quit, c to continue without paging--
ns__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__file__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``, a singleton that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated)) at ../Python/pythonrun.c:1741
#21 0x0000000000629c66 in run_mod (mod=<optimized out>, 
    filename=<optimized out>, 
    globals={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__file__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``, a singleto--Type <RET> for more, q to quit, c to continue without paging--
n that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated), 
    locals={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__file__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``, a singleton that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated), flags=<optimized out>, arena=<optimized out>)
    at ../Python/pythonrun.c:1762
#22 0x000000000063e687 in pyrun_file (fp=fp@entry=0xabf860, 
    filename=filename@entry='/home/dev/Desktop/number_games/sha256/sharun_tse.py', start=start@entry=257, 
    globals=globals@entry={'__name__': '__main__', '__doc__': None, '__package__--Type <RET> for more, q to quit, c to continue without paging--
': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__file__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``, a singleton that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated), 
    locals=locals@entry={'__name__': '__main__', '__doc__': None, '__package__': None, '__loader__': <SourceFileLoader(name='__main__', path='/home/dev/Desktop/number_games/sha256/sharun_tse.py') at remote 0x7ffff75fc2d0>, '__spec__': None, '__annotations__': {}, '__builtins__': <module at remote 0x7ffff7588ae0>, '__file__': '/home/dev/Desktop/number_games/sha256/sharun_tse.py', '__cached__': None, 'annotations': <_Feature(optional=(3, 7, 0, 'beta', 1), mandatory=None, compiler_flag=16777216) at remote 0x7ffff74fb7d0>, 'dpll': <module at remote 0x7ffff74bcbd0>, 'sha256': <module at remote 0x7ffff5ef56c0>, 'math': <module at remote 0x7ffff74bcf90>, 'pyeda': <module at remote 0x7ffff74bebb0>, 'BooleanTrue': <Singleton(__module__='sympy.logic.boolalg', __doc__='\n    SymPy version of ``True``--Type <RET> for more, q to quit, c to continue without paging--
, a singleton that can be accessed via ``S.true``.\n\n    This is the SymPy version of ``True``, for use in the logic module. The\n    primary advantage of using ``true`` instead of ``True`` is that shorthand Boolean\n    operations like ``~`` and ...(truncated), closeit=closeit@entry=1, flags=0x7fffffffdb08)
    at ../Python/pythonrun.c:1657
#23 0x000000000063dd49 in _PyRun_SimpleFileObject (fp=fp@entry=0xabf860, 
    filename=filename@entry='/home/dev/Desktop/number_games/sha256/sharun_tse.py', closeit=closeit@entry=1, flags=flags@entry=0x7fffffffdb08)
    at ../Python/pythonrun.c:440
#24 0x000000000063dabf in _PyRun_AnyFileObject (fp=0xabf860, 
    filename='/home/dev/Desktop/number_games/sha256/sharun_tse.py', closeit=1, 
    flags=0x7fffffffdb08) at ../Python/pythonrun.c:79
#25 0x00000000006385c7 in pymain_run_file_obj (skip_source_first_line=0, 
    filename='/home/dev/Desktop/number_games/sha256/sharun_tse.py', 
    program_name='/home/dev/Desktop/number_games/venv/bin/python3.11')
    at ../Modules/main.c:360
#26 pymain_run_file (config=0xa391e0 <_PyRuntime+59904>)
    at ../Modules/main.c:379
#27 pymain_run_python (exitcode=0x7fffffffdb04) at ../Modules/main.c:601
#28 Py_RunMain () at ../Modules/main.c:680
#29 0x00000000005ff63d in Py_BytesMain (argc=<optimized out>, 
    argv=<optimized out>) at ../Modules/main.c:734
#30 0x00007ffff7c2a1ca in __libc_start_call_main (
--Type <RET> for more, q to quit, c to continue without paging--
    main=main@entry=0x5ff590 <main>, argc=argc@entry=2, 
    argv=argv@entry=0x7fffffffdd48)
    at ../sysdeps/nptl/libc_start_call_main.h:58
#31 0x00007ffff7c2a28b in __libc_start_main_impl (main=0x5ff590 <main>, 
    argc=2, argv=0x7fffffffdd48, init=<optimized out>, fini=<optimized out>, 
    rtld_fini=<optimized out>, stack_end=0x7fffffffdd38)
    at ../csu/libc-start.c:360
#32 0x00000000005ff4c5 in _start ()
(gdb) py-bt
Traceback (most recent call first):
  <built-in method satisfy_one of module object at remote 0x7ffff73938d0>
  File "/home/dev/Desktop/number_games/venv/lib/python3.11/site-packages/pyeda/boolalg/expr.py", line 1385, in satisfy_one
    return picosat.satisfy_one(self.nvars, self.clauses, assumptions,
  File "/home/dev/Desktop/number_games/venv/lib/python3.11/site-packages/pyeda/boolalg/expr.py", line 738, in satisfy_one
    soln = cnf.satisfy_one(assumptions)
  File "/home/dev/Desktop/number_games/sha256/sharun_tse.py", line ?, in <module>
    (failed to get frame line number)

[azewiusz]

Just to mention it fails for sure on pyeda 0.29.0