{"action":"closed","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/961","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/961/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/961/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/961/events","html_url":"https://github.com/Z3Prover/z3/issues/961","id":218700164,"node_id":"MDU6SXNzdWUyMTg3MDAxNjQ=","number":961,"title":"Strange regression between 4.5.0 and current master (4.5.1)","user":{"login":"kostis","id":165033,"node_id":"MDQ6VXNlcjE2NTAzMw==","avatar_url":"https://avatars1.githubusercontent.com/u/165033?v=4","gravatar_id":"","url":"https://api.github.com/users/kostis","html_url":"https://github.com/kostis","followers_url":"https://api.github.com/users/kostis/followers","following_url":"https://api.github.com/users/kostis/following{/other_user}","gists_url":"https://api.github.com/users/kostis/gists{/gist_id}","starred_url":"https://api.github.com/users/kostis/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/kostis/subscriptions","organizations_url":"https://api.github.com/users/kostis/orgs","repos_url":"https://api.github.com/users/kostis/repos","events_url":"https://api.github.com/users/kostis/events{/privacy}","received_events_url":"https://api.github.com/users/kostis/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":6,"created_at":"2017-04-01T14:41:55Z","updated_at":"2018-11-12T12:15:19Z","closed_at":"2018-11-12T12:15:19Z","author_association":"NONE","body":"We are using z3 in a concolic testing tool, called [CutEr](https://github.com/aggelgian/cuter/) and are heavily relying on it -- thanks for all your excellent work, by the way!\r\n\r\nWe have noticed various regressions between v4.5.0, which we use on Travis, and the current `master` branch, which we use for local testing on our own machines (and so that we can notice problems before it is too late).\r\n\r\nOne of them, perhaps the simplest one, is shown below:\r\n```sh\r\n$ z3 -version\r\nZ3 version 4.5.0 - 64 bit\r\n$ z3 -smt2 -T:2 cuter1.smt2 \r\nsat\r\n$ z3 -smt2 -T:2 cuter2.smt2\r\nsat\r\n\r\n$  z3 -version\r\nZ3 version 4.5.1 - 64 bit\r\n$ z3 -smt2 -T:2 cuter1.smt2 \r\nunknown\r\n$ z3 -smt2 -T:2 cuter2.smt2\r\nsat\r\n```\r\n\r\nFiles can be [found here](https://gist.github.com/aggelgian/61d82ff30a6d3700dee060d85dc020c2).  Seems it's not possible to attach `.smt2` files on GitHub.\r\n\r\nThanks to @aggelgian for minimizing the examples.\r\n\r\nPS. There are various other regressions between v4.5.0 and master, but we'll leave these for after this one is fixed."}}
{"actor":{"display_login":"NikolajBjorner"}}