{"action":"closed","issue":{"url":"https://api.github.com/repos/dreal/dreal3/issues/118","labels_url":"https://api.github.com/repos/dreal/dreal3/issues/118/labels{/name}","comments_url":"https://api.github.com/repos/dreal/dreal3/issues/118/comments","events_url":"https://api.github.com/repos/dreal/dreal3/issues/118/events","html_url":"https://github.com/dreal/dreal3/issues/118","id":75967399,"number":118,"title":"previously delta-sat now unsat (commit fef04c126ebd)","user":{"login":"pzuliani","id":7444350,"avatar_url":"https://avatars.githubusercontent.com/u/7444350?v=3","gravatar_id":"","url":"https://api.github.com/users/pzuliani","html_url":"https://github.com/pzuliani","followers_url":"https://api.github.com/users/pzuliani/followers","following_url":"https://api.github.com/users/pzuliani/following{/other_user}","gists_url":"https://api.github.com/users/pzuliani/gists{/gist_id}","starred_url":"https://api.github.com/users/pzuliani/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/pzuliani/subscriptions","organizations_url":"https://api.github.com/users/pzuliani/orgs","repos_url":"https://api.github.com/users/pzuliani/repos","events_url":"https://api.github.com/users/pzuliani/events{/privacy}","received_events_url":"https://api.github.com/users/pzuliani/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/dreal/dreal3/labels/bug","name":"bug","color":"fc2929"}],"state":"closed","locked":false,"assignee":{"login":"soonhokong","id":403281,"avatar_url":"https://avatars.githubusercontent.com/u/403281?v=3","gravatar_id":"","url":"https://api.github.com/users/soonhokong","html_url":"https://github.com/soonhokong","followers_url":"https://api.github.com/users/soonhokong/followers","following_url":"https://api.github.com/users/soonhokong/following{/other_user}","gists_url":"https://api.github.com/users/soonhokong/gists{/gist_id}","starred_url":"https://api.github.com/users/soonhokong/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/soonhokong/subscriptions","organizations_url":"https://api.github.com/users/soonhokong/orgs","repos_url":"https://api.github.com/users/soonhokong/repos","events_url":"https://api.github.com/users/soonhokong/events{/privacy}","received_events_url":"https://api.github.com/users/soonhokong/received_events","type":"User","site_admin":false},"milestone":null,"comments":2,"created_at":"2015-05-13T12:26:21Z","updated_at":"2015-05-13T16:31:37Z","closed_at":"2015-05-13T16:31:37Z","body":"```\r\n(set-logic QF_NRA_ODE)\r\n(declare-fun v () Real)\r\n(declare-fun v_0_0 () Real)\r\n(declare-fun v_0_t () Real)\r\n(declare-fun x () Real)\r\n(declare-fun x_0_0 () Real)\r\n(declare-fun x_0_t () Real)\r\n(declare-fun y () Real)\r\n(declare-fun y_0_0 () Real)\r\n(declare-fun y_0_t () Real)\r\n(declare-fun z () Real)\r\n(declare-fun z_0_0 () Real)\r\n(declare-fun z_0_t () Real)\r\n(declare-fun alphay () Real)\r\n(declare-fun alphay_0_0 () Real)\r\n(declare-fun alphay_0_t () Real)\r\n(declare-fun betax () Real)\r\n(declare-fun betax_0_0 () Real)\r\n(declare-fun betax_0_t () Real)\r\n(declare-fun t () Real)\r\n(declare-fun t_0_0 () Real)\r\n(declare-fun t_0_t () Real)\r\n(declare-fun time_0 () Real)\r\n(define-ode flow_1 ((= d/dt[alphay] 0.0)(= d/dt[betax] 0.0)(= d/dt[t] 1.0)(= d/dt[v] (+ (* (- (- (- (/ 0.0197 (+ 1.0 (exp (* (- 10.0 z) 1.0)))) (/ betax (+ 1.0 (exp (* (- z 10.0) 2.0))))) (* 5.0E-5 (- 1.0 (/ z 12.0)))) 0.01) x) (+ 0.02 (+ (* 5.0E-5 (* (- 1.0 (/ z 12.0)) x)) (* (- (* alphay (- 1.0 (* 1.0 (/ z 12.0)))) 0.0168) y)))))(= d/dt[x] (+ (* (- (- (- (/ 0.0197 (+ 1.0 (exp (* (- 10.0 z) 1.0)))) (/ betax (+ 1.0 (exp (* (- z 10.0) 2.0))))) (* 5.0E-5 (- 1.0 (/ z 12.0)))) 0.01) x) 0.02))(= d/dt[y] (+ (* 5.0E-5 (* (- 1.0 (/ z 12.0)) x)) (* (- (* alphay (- 1.0 (* 1.0 (/ z 12.0)))) 0.0168) y)))(= d/dt[z] (+ (* (- 0.0 z) 0.08) 0.03))))\r\n(assert (>= v_0_0 0))\r\n(assert (<= v_0_0 100))\r\n(assert (>= v_0_t 0))\r\n(assert (<= v_0_t 100))\r\n(assert (>= x_0_0 0))\r\n(assert (<= x_0_0 100))\r\n(assert (>= x_0_t 0))\r\n(assert (<= x_0_t 100))\r\n(assert (>= y_0_0 0))\r\n(assert (<= y_0_0 100))\r\n(assert (>= y_0_t 0))\r\n(assert (<= y_0_t 100))\r\n(assert (>= z_0_0 0))\r\n(assert (<= z_0_0 100))\r\n(assert (>= z_0_t 0))\r\n(assert (<= z_0_t 100))\r\n(assert (>= alphay_0_0 0))\r\n(assert (<= alphay_0_0 0.025))\r\n(assert (>= alphay_0_t 0))\r\n(assert (<= alphay_0_t 0.025))\r\n(assert (>= betax_0_0 0))\r\n(assert (<= betax_0_0 0.025))\r\n(assert (>= betax_0_t 0))\r\n(assert (<= betax_0_t 0.025))\r\n(assert (>= time_0 0))\r\n(assert (<= time_0 83))\r\n(assert (>= t_0_0 0))\r\n(assert (<= t_0_0 83))\r\n(assert (>= t_0_t 0))\r\n(assert (<= t_0_t 83))\r\n(assert\r\n(and\r\n(= [v_0_t x_0_t y_0_t z_0_t alphay_0_t betax_0_t t_0_t] (integral 0. time_0 [v_0_0 x_0_0 y_0_0 z_0_0 alphay_0_0 betax_0_0 t_0_0] flow_1))\r\n(= alphay_0_0 alphay_0_t)\r\n(= betax_0_0 betax_0_t)\r\n(= t_0_0 0)\r\n(>= v_0_0 19.0998)\r\n(<= v_0_0 19.1002)\r\n(>= x_0_0 18.9998)\r\n(<= x_0_0 19.0002)\r\n(>= y_0_0 0.099999)\r\n(<= y_0_0 0.100001)\r\n(>= z_0_0 12.4999)\r\n(<= z_0_0 12.5001)\r\n(= t_0_t 83)\r\n(>= v_0_t 1.1)\r\n(<= v_0_t 3.9)\r\n)\r\n)\r\n(check-sat)\r\n(exit)\r\n```\r\n"}}