{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/619","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/619/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/619/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/619/events","html_url":"https://github.com/Z3Prover/z3/issues/619","id":156603348,"number":619,"title":"Unexpected large table warning, occurring sporadically","user":{"login":"jcreedcmu","id":1500822,"avatar_url":"https://avatars.githubusercontent.com/u/1500822?v=3","gravatar_id":"","url":"https://api.github.com/users/jcreedcmu","html_url":"https://github.com/jcreedcmu","followers_url":"https://api.github.com/users/jcreedcmu/followers","following_url":"https://api.github.com/users/jcreedcmu/following{/other_user}","gists_url":"https://api.github.com/users/jcreedcmu/gists{/gist_id}","starred_url":"https://api.github.com/users/jcreedcmu/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/jcreedcmu/subscriptions","organizations_url":"https://api.github.com/users/jcreedcmu/orgs","repos_url":"https://api.github.com/users/jcreedcmu/repos","events_url":"https://api.github.com/users/jcreedcmu/events{/privacy}","received_events_url":"https://api.github.com/users/jcreedcmu/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":{"login":"NikolajBjorner","id":3085284,"avatar_url":"https://avatars.githubusercontent.com/u/3085284?v=3","gravatar_id":"","url":"https://api.github.com/users/NikolajBjorner","html_url":"https://github.com/NikolajBjorner","followers_url":"https://api.github.com/users/NikolajBjorner/followers","following_url":"https://api.github.com/users/NikolajBjorner/following{/other_user}","gists_url":"https://api.github.com/users/NikolajBjorner/gists{/gist_id}","starred_url":"https://api.github.com/users/NikolajBjorner/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/NikolajBjorner/subscriptions","organizations_url":"https://api.github.com/users/NikolajBjorner/orgs","repos_url":"https://api.github.com/users/NikolajBjorner/repos","events_url":"https://api.github.com/users/NikolajBjorner/events{/privacy}","received_events_url":"https://api.github.com/users/NikolajBjorner/received_events","type":"User","site_admin":false},"milestone":null,"comments":5,"created_at":"2016-05-24T20:38:04Z","updated_at":"2016-05-27T03:55:52Z","closed_at":null,"body":"When I put \r\nhttps://gist.github.com/anonymous/bacabff86b15923bf482feb22c54456a\r\nin `/tmp/test.smt2`\r\nand run\r\n`z3 /tmp/test.smt2`\r\nI reliably get the warning\r\n`WARNING: creating large table of size 4294967296 for relation acl-rule-must-match-tcp-udp`\r\nwhich I don't expect. Moreover, when I change every occurrence of `acl-rule-must-match-tcp-udp` to `bar`, the warning usually goes away --- but still occurs about 1% of the time, when I run a bash loop repeatedly doing `z3 /tmp/test.smt2`.\r\n\r\nMost of my attempts at making this counterexample smaller also make the warning go away ~100% of the time, up to the limits of my patience while testing."},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/222054498","html_url":"https://github.com/Z3Prover/z3/issues/619#issuecomment-222054498","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/619","id":222054498,"user":{"login":"NikolajBjorner","id":3085284,"avatar_url":"https://avatars.githubusercontent.com/u/3085284?v=3","gravatar_id":"","url":"https://api.github.com/users/NikolajBjorner","html_url":"https://github.com/NikolajBjorner","followers_url":"https://api.github.com/users/NikolajBjorner/followers","following_url":"https://api.github.com/users/NikolajBjorner/following{/other_user}","gists_url":"https://api.github.com/users/NikolajBjorner/gists{/gist_id}","starred_url":"https://api.github.com/users/NikolajBjorner/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/NikolajBjorner/subscriptions","organizations_url":"https://api.github.com/users/NikolajBjorner/orgs","repos_url":"https://api.github.com/users/NikolajBjorner/repos","events_url":"https://api.github.com/users/NikolajBjorner/events{/privacy}","received_events_url":"https://api.github.com/users/NikolajBjorner/received_events","type":"User","site_admin":false},"created_at":"2016-05-27T03:55:52Z","updated_at":"2016-05-27T03:55:52Z","body":"yes, sure I am wondering too, but don't yet have an answer on that. non-determinism is a bug."}}
{"actor":{"display_login":"NikolajBjorner"}}