Skip to content

Instantly share code, notes, and snippets.

@dddejan
Created April 19, 2015 15:30
Show Gist options
  • Save dddejan/80537e542611c0f7cfea to your computer and use it in GitHub Desktop.
Save dddejan/80537e542611c0f7cfea to your computer and use it in GitHub Desktop.
z3 segfault idl
(set-info :source |fuzzsmt|)
(set-info :smt-lib-version 2.0)
(set-info :category "random")
(set-info :status unknown)
(set-logic QF_IDL)
(declare-fun v0 () Int)
(declare-fun v1 () Int)
(declare-fun v2 () Int)
(assert (let ((e3 198588528432604))
(let ((e4 1829885882))
(let ((e5 26020438394164209))
(let ((e6 51808564085))
(let ((e7 7896))
(let ((e8 105069))
(let ((e9 (> v2 v0)))
(let ((e10 (> v0 v2)))
(let ((e11 (>= (- v2 v1) (- e3))))
(let ((e12 (<= (- v1 v0) e4)))
(let ((e13 (<= v0 v0)))
(let ((e14 (> (- v2 v2) e4)))
(let ((e15 (<= (- v0 v2) (- e3))))
(let ((e16 (<= (- v0 v0) (- e8))))
(let ((e17 (< v1 v0)))
(let ((e18 (>= (- v2 v1) (- e5))))
(let ((e19 (distinct (- v1 v0) e3)))
(let ((e20 (< (- v0 v2) (- e5))))
(let ((e21 (> (- v1 v1) e6)))
(let ((e22 (= (- v1 v0) e3)))
(let ((e23 (distinct (- v2 v0) (- e3))))
(let ((e24 (<= v2 v0)))
(let ((e25 (>= v0 v2)))
(let ((e26 (< v0 v2)))
(let ((e27 (= (- v1 v1) e8)))
(let ((e28 (>= v1 v1)))
(let ((e29 (<= v2 v0)))
(let ((e30 (distinct v0 v1)))
(let ((e31 (> v2 v1)))
(let ((e32 (<= v2 v2)))
(let ((e33 (distinct v2 v1)))
(let ((e34 (distinct (- v1 v0) (- e8))))
(let ((e35 (distinct (- v0 v0) (- e4))))
(let ((e36 (<= (- v1 v2) e5)))
(let ((e37 (< (- v1 v2) (- e5))))
(let ((e38 (> v1 v1)))
(let ((e39 (< (- v2 v0) (- e3))))
(let ((e40 (distinct (- v2 v1) (- e3))))
(let ((e41 (> (- v1 v2) e7)))
(let ((e42 (<= (- v1 v1) e4)))
(let ((e43 (<= v1 v0)))
(let ((e44 (= (- v0 v0) (- e5))))
(let ((e45 (< (- v2 v1) e3)))
(let ((e46 (distinct (- v1 v0) e5)))
(let ((e47 (<= (- v2 v2) (- e7))))
(let ((e48 (> v2 v1)))
(let ((e49 (< (- v1 v1) e4)))
(let ((e50 (= v1 v0)))
(let ((e51 (<= v0 v0)))
(let ((e52 (distinct v1 v0)))
(let ((e53 (not e24)))
(let ((e54 (or e42 e30)))
(let ((e55 (= e9 e53)))
(let ((e56 (and e19 e49)))
(let ((e57 (and e35 e32)))
(let ((e58 (and e25 e47)))
(let ((e59 (ite e15 e16 e50)))
(let ((e60 (xor e56 e55)))
(let ((e61 (ite e21 e27 e45)))
(let ((e62 (=> e34 e38)))
(let ((e63 (or e46 e52)))
(let ((e64 (= e59 e14)))
(let ((e65 (xor e58 e48)))
(let ((e66 (ite e10 e33 e54)))
(let ((e67 (not e40)))
(let ((e68 (= e41 e13)))
(let ((e69 (=> e37 e31)))
(let ((e70 (or e39 e26)))
(let ((e71 (=> e12 e20)))
(let ((e72 (ite e68 e17 e28)))
(let ((e73 (xor e44 e67)))
(let ((e74 (not e72)))
(let ((e75 (=> e71 e23)))
(let ((e76 (=> e73 e22)))
(let ((e77 (=> e29 e64)))
(let ((e78 (= e11 e70)))
(let ((e79 (or e60 e63)))
(let ((e80 (ite e79 e79 e51)))
(let ((e81 (xor e43 e62)))
(let ((e82 (not e65)))
(let ((e83 (ite e61 e81 e80)))
(let ((e84 (not e74)))
(let ((e85 (and e84 e78)))
(let ((e86 (ite e83 e85 e69)))
(let ((e87 (or e77 e82)))
(let ((e88 (and e87 e76)))
(let ((e89 (= e75 e75)))
(let ((e90 (=> e86 e88)))
(let ((e91 (=> e90 e57)))
(let ((e92 (= e91 e89)))
(let ((e93 (not e66)))
(let ((e94 (or e18 e18)))
(let ((e95 (not e94)))
(let ((e96 (xor e36 e92)))
(let ((e97 (xor e96 e95)))
(let ((e98 (and e93 e97)))
e98
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))
(check-sat)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment