{"action":"closed","issue":{"url":"https://api.github.com/repos/CVC4/CVC4/issues/1853","repository_url":"https://api.github.com/repos/CVC4/CVC4","labels_url":"https://api.github.com/repos/CVC4/CVC4/issues/1853/labels{/name}","comments_url":"https://api.github.com/repos/CVC4/CVC4/issues/1853/comments","events_url":"https://api.github.com/repos/CVC4/CVC4/issues/1853/events","html_url":"https://github.com/CVC4/CVC4/issues/1853","id":319748827,"number":1853,"title":"CVC4 uses SMT2 syntax for dump with option --output-lang=smt1 ","user":{"login":"4tXJ7f","id":1926228,"avatar_url":"https://avatars3.githubusercontent.com/u/1926228?v=4","gravatar_id":"","url":"https://api.github.com/users/4tXJ7f","html_url":"https://github.com/4tXJ7f","followers_url":"https://api.github.com/users/4tXJ7f/followers","following_url":"https://api.github.com/users/4tXJ7f/following{/other_user}","gists_url":"https://api.github.com/users/4tXJ7f/gists{/gist_id}","starred_url":"https://api.github.com/users/4tXJ7f/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/4tXJ7f/subscriptions","organizations_url":"https://api.github.com/users/4tXJ7f/orgs","repos_url":"https://api.github.com/users/4tXJ7f/repos","events_url":"https://api.github.com/users/4tXJ7f/events{/privacy}","received_events_url":"https://api.github.com/users/4tXJ7f/received_events","type":"User","site_admin":false},"labels":[{"id":21411286,"url":"https://api.github.com/repos/CVC4/CVC4/labels/bug","name":"bug","color":"b60205","default":true},{"id":671892488,"url":"https://api.github.com/repos/CVC4/CVC4/labels/minor","name":"minor","color":"fef2c0","default":false}],"state":"closed","locked":false,"assignee":{"login":"4tXJ7f","id":1926228,"avatar_url":"https://avatars3.githubusercontent.com/u/1926228?v=4","gravatar_id":"","url":"https://api.github.com/users/4tXJ7f","html_url":"https://github.com/4tXJ7f","followers_url":"https://api.github.com/users/4tXJ7f/followers","following_url":"https://api.github.com/users/4tXJ7f/following{/other_user}","gists_url":"https://api.github.com/users/4tXJ7f/gists{/gist_id}","starred_url":"https://api.github.com/users/4tXJ7f/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/4tXJ7f/subscriptions","organizations_url":"https://api.github.com/users/4tXJ7f/orgs","repos_url":"https://api.github.com/users/4tXJ7f/repos","events_url":"https://api.github.com/users/4tXJ7f/events{/privacy}","received_events_url":"https://api.github.com/users/4tXJ7f/received_events","type":"User","site_admin":false},"assignees":[{"login":"4tXJ7f","id":1926228,"avatar_url":"https://avatars3.githubusercontent.com/u/1926228?v=4","gravatar_id":"","url":"https://api.github.com/users/4tXJ7f","html_url":"https://github.com/4tXJ7f","followers_url":"https://api.github.com/users/4tXJ7f/followers","following_url":"https://api.github.com/users/4tXJ7f/following{/other_user}","gists_url":"https://api.github.com/users/4tXJ7f/gists{/gist_id}","starred_url":"https://api.github.com/users/4tXJ7f/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/4tXJ7f/subscriptions","organizations_url":"https://api.github.com/users/4tXJ7f/orgs","repos_url":"https://api.github.com/users/4tXJ7f/repos","events_url":"https://api.github.com/users/4tXJ7f/events{/privacy}","received_events_url":"https://api.github.com/users/4tXJ7f/received_events","type":"User","site_admin":false}],"milestone":null,"comments":2,"created_at":"2018-05-02T23:48:58Z","updated_at":"2018-05-03T03:08:01Z","closed_at":"2018-05-03T03:08:01Z","author_association":"OWNER","body":"```\r\n$ builds/bin/cvc4 --preprocess-only --lang=smt1 --output-lang=smt1 --dump raw-benchmark test/regress/regress0/arith/miplibtrick.smt\r\n(set-option :incremental false)\r\n(meta-info :status sat)\r\n(set-logic QF_LRA)\r\n(declare-fun tmp1 () Real)\r\n(declare-fun x177 () Bool)\r\n(check-sat-assuming ( (and (=> (and (not x177) true) (= tmp1 0.0)) (=> (and x177 true) (= tmp1 (to_real (- 350))))) ))\r\nunknown (REQUIRES_FULL_CHECK)\r\n```"}}
{"actor":{"display_login":"ajreynol"}}