{"action":"closed","issue":{"url":"https://api.github.com/repos/stp/stp/issues/106","repository_url":"https://api.github.com/repos/stp/stp","labels_url":"https://api.github.com/repos/stp/stp/issues/106/labels{/name}","comments_url":"https://api.github.com/repos/stp/stp/issues/106/comments","events_url":"https://api.github.com/repos/stp/stp/issues/106/events","html_url":"https://github.com/stp/stp/issues/106","id":33732952,"number":106,"title":"Crash when \"thinking about\" divide by zero","user":{"login":"smcc","id":2005910,"avatar_url":"https://avatars.githubusercontent.com/u/2005910?v=3","gravatar_id":"","url":"https://api.github.com/users/smcc","html_url":"https://github.com/smcc","followers_url":"https://api.github.com/users/smcc/followers","following_url":"https://api.github.com/users/smcc/following{/other_user}","gists_url":"https://api.github.com/users/smcc/gists{/gist_id}","starred_url":"https://api.github.com/users/smcc/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/smcc/subscriptions","organizations_url":"https://api.github.com/users/smcc/orgs","repos_url":"https://api.github.com/users/smcc/repos","events_url":"https://api.github.com/users/smcc/events{/privacy}","received_events_url":"https://api.github.com/users/smcc/received_events","type":"User","site_admin":false},"labels":[],"state":"closed","locked":false,"assignee":null,"milestone":null,"comments":4,"created_at":"2014-05-17T15:42:32Z","updated_at":"2016-06-09T04:28:29Z","closed_at":"2016-06-09T04:28:29Z","body":"STP has some long-running issues related to division by zero, which I recently noticed can still bite FuzzBALL in the right (wrong) situation. I think it's not clear exactly what semantics we want for the result, which may be part of the problem. Situations where you write an explicit division by zero in the input file can usually be avoided. But it appears you can also create a formula that involves division of values that are not constrained to be zero, and STP will choose to try values that lead to a division by zero and then crash. For instance in the following example, it appears from a quick look that STP reaches the point of running SAT and getting a satisfying CNF assignment, and then crashes when substituting it back in to check the assignment.\r\n\r\n```\r\ny : BV(8);\r\nt4 : BV(8) = BVPLUS(8, y, BVUMINUS(y), 0h01);\r\nQUERY(BVDIV(16, (0h00 @ t4),(0h00 @ y))[0:0] = 0b0);\r\n```\r\n(Also gist: https://gist.github.com/smcc/901e471273743fac922f)\r\n\r\nIt should certainly be possible to not crash, but I'm not sure what the right behavior should be, since having undefined behavior breaks the assumption that you will always get a consistent output when you plug in a given input. IIRC the SMTLIB2 spec says that division by zero is undefined. If we consider that that gives us license to say, pretend it always returns 1 (I think this was the behavior of early versions and is still present in the code), that would be a nice deterministic choice, but some users might feel it it's weird behavior to show up with no error message."}}
{"actor":{"display_login":"TrevorHansen"}}