{"action":"closed","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/676","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/676/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/676/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/676/events","html_url":"https://github.com/Z3Prover/z3/issues/676","id":164672069,"number":676,"title":"Segmentation fault in python3","user":{"login":"DanielWaterworth","id":663767,"avatar_url":"https://avatars.githubusercontent.com/u/663767?v=3","gravatar_id":"","url":"https://api.github.com/users/DanielWaterworth","html_url":"https://github.com/DanielWaterworth","followers_url":"https://api.github.com/users/DanielWaterworth/followers","following_url":"https://api.github.com/users/DanielWaterworth/following{/other_user}","gists_url":"https://api.github.com/users/DanielWaterworth/gists{/gist_id}","starred_url":"https://api.github.com/users/DanielWaterworth/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/DanielWaterworth/subscriptions","organizations_url":"https://api.github.com/users/DanielWaterworth/orgs","repos_url":"https://api.github.com/users/DanielWaterworth/repos","events_url":"https://api.github.com/users/DanielWaterworth/events{/privacy}","received_events_url":"https://api.github.com/users/DanielWaterworth/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":3,"created_at":"2016-07-09T15:40:57Z","updated_at":"2016-07-17T23:17:45Z","closed_at":"2016-07-17T23:17:45Z","body":"test.py:\r\n\r\n```python\r\nimport z3\r\n\r\nData = z3.DeclareSort('Data')\r\n\r\nOperation = z3.Datatype('Operation')\r\nOperation.declare('set', ('key1', Data), ('value', Data))\r\nOperation.declare('delete', ('key2', Data))\r\nOperation.declare('get', ('key3', Data))\r\nOperation = Operation.create()\r\n\r\n# This is necessary for some reason\r\nclass Foo:\r\n    def __init__(self):\r\n        pass\r\n```\r\n\r\nGDB backtrace:\r\n\r\n    #0  0x00007ffff78261c7 in __GI_raise (sig=sig@entry=6) at ../sysdeps/unix/sysv/linux/raise.c:55\r\n    #1  0x00007ffff7827e2a in __GI_abort () at abort.c:89\r\n    #2  0x00007ffff7869ba3 in __libc_message (do_abort=do_abort@entry=1, fmt=fmt@entry=0x7ffff79820f8 \"*** Error in `%s': %s: 0x%s ***\\n\") at ../sysdeps/posix/libc_fatal.c:175\r\n    #3  0x00007ffff78703b8 in malloc_printerr (ptr=<optimised out>, str=0x7ffff797e285 \"corrupted double-linked list\", action=1) at malloc.c:4965\r\n    #4  malloc_consolidate (av=av@entry=0x7ffff7bb5c00 <main_arena>) at malloc.c:4150\r\n    #5  0x00007ffff7871e68 in _int_free (av=0x7ffff7bb5c00 <main_arena>, p=<optimised out>, have_lock=0) at malloc.c:4042\r\n    #6  0x00007ffff78757ec in __GI___libc_free (mem=<optimised out>) at malloc.c:2950\r\n    #7  0x000000000056e4b9 in dict_tp_clear.lto_priv.287 (op=<optimised out>) at ../Objects/dictobject.c:2495\r\n    #8  0x00000000005204fe in delete_garbage (old=<optimised out>, collectable=<optimised out>) at ../Modules/gcmodule.c:866\r\n    #9  collect.lto_priv () at ../Modules/gcmodule.c:1032\r\n    #10 0x00000000005f3597 in _PyGC_CollectNoFail () at ../Modules/gcmodule.c:1638\r\n    #11 0x0000000000500340 in PyImport_Cleanup () at ../Python/import.c:487\r\n    #12 0x00000000005f8836 in Py_Finalize () at ../Python/pythonrun.c:616\r\n    #13 0x0000000000619043 in Py_Main () at ../Modules/main.c:771\r\n    #14 0x00000000004c27df in main () at ../Modules/python.c:69\r\n    #15 0x00007ffff7811ac0 in __libc_start_main (main=0x4c2700 <main>, argc=2, argv=0x7fffffffdd48, init=<optimised out>, fini=<optimised out>, rtld_fini=<optimised out>, stack_end=0x7fffffffdd38) at libc-start.c:289\r\n    #16 0x00000000005bdf09 in _start ()\r\n\r\nInstalled versions:\r\n\r\n    $ z3 --version\r\n    Z3 version 4.4.2\r\n    # The sha of the checkout was 0d0d504d62735616bf38c8b2671ea91d68fb5fd2\r\n\r\n    $ python3 --version\r\n    Python 3.4.3+\r\n    # The plus is because I installed a version with debugging symbols."}}
{"actor":{"display_login":"NikolajBjorner"}}