{"action":"created","issue":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/447","repository_url":"https://api.github.com/repos/Z3Prover/z3","labels_url":"https://api.github.com/repos/Z3Prover/z3/issues/447/labels{/name}","comments_url":"https://api.github.com/repos/Z3Prover/z3/issues/447/comments","events_url":"https://api.github.com/repos/Z3Prover/z3/issues/447/events","html_url":"https://github.com/Z3Prover/z3/issues/447","id":132928185,"number":447,"title":"Problem understanding z3 behaviour with floats ","user":{"login":"cfumex","id":17174706,"avatar_url":"https://avatars.githubusercontent.com/u/17174706?v=3","gravatar_id":"","url":"https://api.github.com/users/cfumex","html_url":"https://github.com/cfumex","followers_url":"https://api.github.com/users/cfumex/followers","following_url":"https://api.github.com/users/cfumex/following{/other_user}","gists_url":"https://api.github.com/users/cfumex/gists{/gist_id}","starred_url":"https://api.github.com/users/cfumex/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cfumex/subscriptions","organizations_url":"https://api.github.com/users/cfumex/orgs","repos_url":"https://api.github.com/users/cfumex/repos","events_url":"https://api.github.com/users/cfumex/events{/privacy}","received_events_url":"https://api.github.com/users/cfumex/received_events","type":"User","site_admin":false},"labels":[{"url":"https://api.github.com/repos/Z3Prover/z3/labels/question","name":"question","color":"cc317c"}],"state":"open","locked":false,"assignee":null,"milestone":null,"comments":2,"created_at":"2016-02-11T09:44:20Z","updated_at":"2016-02-11T10:25:09Z","closed_at":null,"body":"Hello,\r\n\r\nI am experimenting with z3 float support. Currently z3 is behaving\r\nerratically, proving some hard VCs and not proving simpler ones. I\r\nhave isolated a representative problem to try to understand it with\r\nyou.\r\n\r\nOn this example pasted below, I had to kill z3 (git version) after\r\n~550s. However if I remove the (apparently unrelated) first assertion,\r\nline 9, on \"to_bv\", z3 returns unsat in less than 2 seconds. Now if I \r\nadd the assertion commented out, line 16, z3 returns unsat in ~90s.\r\n\r\nIs this expected ?\r\nIs there any way to anticipate / prevent this behaviour (are the\r\nassertions stated in a bad way, or maybe the trigger's patterns are ...) ?\r\n\r\nThank you,\r\nClément Fumex\r\n___________________________________________________________\r\n\r\n(set-info :source |VC generated by SPARK 2014|)\r\n(set-info :smt-lib-version 2.0)\r\n(set-info :category industrial)\r\n(set-info :status unknown)\r\n\r\n(declare-fun to_bv (Float32) (_ BitVec 32))\r\n\r\n;; \\/ x1 : bv32. is_finite (of_bv x1) -> to_bv (of_bv x1) = x1\r\n(assert\r\n (forall ((x1 (_ BitVec 32)))\r\n (! (=>\r\n     (not (or (fp.isInfinite ((_ to_fp 8 24) x1)) (fp.isNaN ((_ to_fp 8 24) x1))))\r\n     (= (to_bv ((_ to_fp 8 24) x1)) x1))\r\n    :pattern ((to_bv ((_ to_fp 8 24) x1))) )))\r\n\r\n;; (assert\r\n;;   (forall ((x1 Float32))\r\n;;   (! (=> (not (or (fp.isInfinite x1) (fp.isNaN x1)))\r\n;;          (= ((_ to_fp 8 24) (to_bv x1)) x1)) :pattern (((_ to_fp 8 24) (to_bv x1))) )))\r\n\r\n(define-fun l2 () Float32 ((_ to_fp 8 24) #x3F800000)) ; 1.0\r\n(define-fun l3 () Float32 ((_ to_fp 8 24) #x3E800000)) ; 0.25\r\n(define-fun l4 () Float32 ((_ to_fp 8 24) #x454CCCCD)) ; 2 ** 16 / 20 ~= 3276.8\r\n(define-fun l5 () Float32 ((_ to_fp 8 24) #x41200000)) ; 10.0\r\n(define-fun l6 () Float32 ((_ to_fp 8 24) #x41A00000)) ; 20.0\r\n\r\n(declare-fun x () (_ BitVec 16))\r\n(declare-fun y () Float32)\r\n(declare-fun res4 () Float32)\r\n(declare-fun res5 () Float32)\r\n\r\n(assert (and (fp.leq l3 y) (fp.leq y l2)))                        ; 0.25 <= y <= 1.0\r\n(assert (= res4 (fp.div RNE ((_ to_fp_unsigned 8 24) RNE x) l4))) ; res4 = (float)x / l4\r\n(assert (=> (fp.geq res4 l5) (= res5 (fp.sub RNE res4 l6))))      ; res4 >= 10.0 -> res5 = res4 - 20.0\r\n(assert (=> (not (fp.geq res4 l5)) (= res5 res4)))                ; res4 <  10.0 -> res5 = res4\r\n\r\n(assert                                                           ; res5 / y is not finite\r\n (or (fp.isInfinite (fp.div RNE res5 y))\r\n     (fp.isNaN (fp.div RNE res5 y))))\r\n(check-sat)"},"comment":{"url":"https://api.github.com/repos/Z3Prover/z3/issues/comments/182794331","html_url":"https://github.com/Z3Prover/z3/issues/447#issuecomment-182794331","issue_url":"https://api.github.com/repos/Z3Prover/z3/issues/447","id":182794331,"user":{"login":"cfumex","id":17174706,"avatar_url":"https://avatars.githubusercontent.com/u/17174706?v=3","gravatar_id":"","url":"https://api.github.com/users/cfumex","html_url":"https://github.com/cfumex","followers_url":"https://api.github.com/users/cfumex/followers","following_url":"https://api.github.com/users/cfumex/following{/other_user}","gists_url":"https://api.github.com/users/cfumex/gists{/gist_id}","starred_url":"https://api.github.com/users/cfumex/starred{/owner}{/repo}","subscriptions_url":"https://api.github.com/users/cfumex/subscriptions","organizations_url":"https://api.github.com/users/cfumex/orgs","repos_url":"https://api.github.com/users/cfumex/repos","events_url":"https://api.github.com/users/cfumex/events{/privacy}","received_events_url":"https://api.github.com/users/cfumex/received_events","type":"User","site_admin":false},"created_at":"2016-02-11T10:25:09Z","updated_at":"2016-02-11T10:25:09Z","body":"Thanks for the very quick answer ! \r\nThis definitely explains things. \r\n\r\nTo go a little further: this example was reduced from several VCs where we have a lot of assertions with quantifier in the context which don't seem to be directly related to the current goal (defining functions that are not used etc ...). We tried to remove some of them expecting something like the less of those axioms in the context the quicker z3 would be. However we found out that, while removing /adding such axioms has a lot of impact, we are not able to anticipate this impact at all. This is somewhat illustrated in the VC pasted above where if I uncomment the second assertion with a quantifier z3 returns unsat in 80s instead of nothing in 550s with just the first assertion. \r\nIs there anything to do about that ? (besides getting rid of all of the axioms with quantifier)"}}