{"action":"opened","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/1491","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/1491/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/1491/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/1491/events","html_url":"https://github.com/Z3Prover/z3/issues/1491","id":297457155,"number":1491,"title":"lexicographic assert-soft bug (?)","user":{"login":"PatrickTrentin88","id":6245704,"avatar_url":"https://avatars3.githubusercontent.com/u/6245704?v=4","gravatar_id":"","url":"https://api.github.com/users/PatrickTrentin88","html_url":"https://github.com/PatrickTrentin88","followers_url":"https://api.github.com/users/PatrickTrentin88/followers","following_url":"https://api.github.com/users/PatrickTrentin88/following{/other_user}","gists_url":"https://api.github.com/users/PatrickTrentin88/gists{/gist_id}","starred_url":"https://api.github.com/users/PatrickTrentin88/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/PatrickTrentin88/subscriptions","organizations_url":"https://api.github.com/users/PatrickTrentin88/orgs","repos_url":"https://api.github.com/users/PatrickTrentin88/repos","events_url":"https://api.github.com/users/PatrickTrentin88/events{/privacy}","received_events_url":"https://api.github.com/users/PatrickTrentin88/received_events","type":"User","site_admin":false},"labels":[],"state":"open","locked":false,"assignee":null,"assignees":[],"milestone":null,"comments":0,"created_at":"2018-02-15T14:05:04Z","updated_at":"2018-02-15T14:05:04Z","closed_at":null,"author_association":"NONE","body":"**toy.smt2**:\r\n```\r\n(set-option :produce-models true)\r\n(set-option :opt.priority lex)\r\n\r\n(declare-fun A () Bool)\r\n(declare-fun B () Bool)\r\n(declare-fun x () Int)\r\n\r\n(assert (or (not A) (not B)))\r\n\r\n(assert (or (not A) (<= x 50)))\r\n(assert (or (not B) (<= x 99)))\r\n\r\n(assert (<= x 200))\r\n\r\n(assert-soft A :weight 1 :id goal)\r\n(assert-soft B :weight 1 :id goal)\r\n\r\n;(minimize goal)\r\n(maximize x)\r\n\r\n(check-sat)\r\n(get-objectives)\r\n(get-model)\r\n```\r\n\r\n**output**:\r\n\r\n```\r\nsat\r\n(objectives\r\n (goal 1)\r\n (x 200)\r\n)\r\n(model \r\n  (define-fun A () Bool\r\n    false)\r\n  (define-fun B () Bool\r\n    false)\r\n  (define-fun x () Int\r\n    200)\r\n)\r\n```\r\n\r\nObjective `x` should not evaluate `200`, because `goal` equals to `1` means that either `A` or `B` is true, which means that there should be an additional upper-bound over `x` equal to `50` or `99`.\r\n"}}
{"actor":{"display_login":"PatrickTrentin88"}}