(error "context exception") on a QF_IDL problem

[dddejan]

The problem

(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)
(assert (let ((e2 61895))
(let ((e3 329848102180743))
(let ((e4 764349))
(let ((e5 23463))
(let ((e6 2))
(let ((e7 6))
(let ((e8 (< v0 v1)))
(let ((e9 (distinct (- v0 v0) e3)))
(let ((e10 (= (- v1 v1) e7)))
(let ((e11 (= v0 v0)))
(let ((e12 (>= (- v0 v1) e6)))
(let ((e13 (>= (- v0 v1) e7)))
(let ((e14 (<= v0 v0)))
(let ((e15 (> (- v0 v0) (- e2))))
(let ((e16 (>= v0 v0)))
(let ((e17 (<= v0 v0)))
(let ((e18 (= (- v1 v1) (- e2))))
(let ((e19 (distinct (- v1 v0) e3)))
(let ((e20 (> (- v1 v1) e4)))
(let ((e21 (> v1 v1)))
(let ((e22 (<= (- v1 v0) (- e4))))
(let ((e23 (< (- v1 v0) (- e6))))
(let ((e24 (<= (- v0 v1) (- e4))))
(let ((e25 (>= (- v1 v0) (- e4))))
(let ((e26 (< v0 v1)))
(let ((e27 (> (- v0 v1) (- e3))))
(let ((e28 (distinct v1 v1)))
(let ((e29 (distinct (- v0 v0) (- e3))))
(let ((e30 (< v0 v0)))
(let ((e31 (< (- v1 v0) (- e7))))
(let ((e32 (>= v0 v0)))
(let ((e33 (< (- v1 v1) e4)))
(let ((e34 (<= (- v1 v0) (- e4))))
(let ((e35 (= (- v1 v0) (- e5))))
(let ((e36 (> v0 v0)))
(let ((e37 (> v0 v0)))
(let ((e38 (< v1 v1)))
(let ((e39 (>= (- v1 v1) (- e4))))
(let ((e40 (= v0 v1)))
(let ((e41 (distinct v1 v0)))
(let ((e42 (< v0 v0)))
(let ((e43 (< v1 v1)))
(let ((e44 (< (- v0 v1) (- e4))))
(let ((e45 (= (- v0 v0) e2)))
(let ((e46 (<= (- v1 v0) (- e5))))
(let ((e47 (distinct (- v0 v1) e2)))
(let ((e48 (>= (- v0 v0) e4)))
(let ((e49 (< v1 v0)))
(let ((e50 (> v0 v1)))
(let ((e51 (> v0 v1)))
(let ((e52 (distinct (- v1 v1) e5)))
(let ((e53 (distinct (- v1 v1) (- e2))))
(let ((e54 (<= (- v1 v1) (- e4))))
(let ((e55 (< (- v0 v1) e4)))
(let ((e56 (= (- v0 v0) e5)))
(let ((e57 (= v0 v0)))
(let ((e58 (= (- v1 v0) (- e4))))
(let ((e59 (> v1 v1)))
(let ((e60 (distinct v1 v0)))
(let ((e61 (distinct (- v0 v0) (- e7))))
(let ((e62 (ite e25 e46 e56)))
(let ((e63 (and e51 e53)))
(let ((e64 (=> e47 e10)))
(let ((e65 (= e43 e52)))
(let ((e66 (=> e31 e65)))
(let ((e67 (= e24 e13)))
(let ((e68 (= e28 e38)))
(let ((e69 (or e39 e30)))
(let ((e70 (and e64 e55)))
(let ((e71 (=> e11 e29)))
(let ((e72 (or e69 e21)))
(let ((e73 (= e22 e49)))
(let ((e74 (or e33 e18)))
(let ((e75 (not e67)))
(let ((e76 (xor e15 e74)))
(let ((e77 (xor e14 e71)))
(let ((e78 (= e36 e23)))
(let ((e79 (= e34 e58)))
(let ((e80 (and e68 e62)))
(let ((e81 (=> e50 e63)))
(let ((e82 (not e42)))
(let ((e83 (not e77)))
(let ((e84 (ite e45 e16 e60)))
(let ((e85 (= e76 e82)))
(let ((e86 (= e84 e80)))
(let ((e87 (or e85 e12)))
(let ((e88 (xor e83 e70)))
(let ((e89 (ite e66 e17 e48)))
(let ((e90 (ite e79 e27 e86)))
(let ((e91 (and e73 e44)))
(let ((e92 (ite e81 e87 e87)))
(let ((e93 (ite e32 e72 e78)))
(let ((e94 (ite e90 e40 e59)))
(let ((e95 (xor e19 e75)))
(let ((e96 (ite e95 e94 e94)))
(let ((e97 (=> e35 e93)))
(let ((e98 (and e26 e61)))
(let ((e99 (xor e8 e37)))
(let ((e100 (and e20 e92)))
(let ((e101 (= e41 e88)))
(let ((e102 (xor e54 e57)))
(let ((e103 (or e91 e9)))
(let ((e104 (and e89 e101)))
(let ((e105 (=> e100 e103)))
(let ((e106 (not e97)))
(let ((e107 (and e106 e105)))
(let ((e108 (= e107 e102)))
(let ((e109 (=> e98 e98)))
(let ((e110 (xor e104 e104)))
(let ((e111 (ite e99 e108 e109)))
(let ((e112 (and e111 e96)))
(let ((e113 (or e112 e110)))
e113
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)

[dddejan]

Another IDL problem with the same issue

(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)
(declare-fun v3 () Int)
(declare-fun v4 () Int)
(declare-fun v5 () Int)
(assert (let ((e6 3044))
(let ((e7 717307937888699))
(let ((e8 1))
(let ((e9 532995695784405))
(let ((e10 139358193))
(let ((e11 77363600))
(let ((e12 (< (- v1 v4) e11)))
(let ((e13 (>= v4 v0)))
(let ((e14 (< v0 v0)))
(let ((e15 (= (- v1 v5) (- e6))))
(let ((e16 (< (- v0 v1) e6)))
(let ((e17 (<= (- v3 v1) e6)))
(let ((e18 (<= (- v1 v3) (- e6))))
(let ((e19 (= v1 v2)))
(let ((e20 (> (- v4 v4) (- e9))))
(let ((e21 (= v0 v1)))
(let ((e22 (> (- v1 v1) (- e7))))
(let ((e23 (<= (- v2 v0) (- e7))))
(let ((e24 (<= (- v1 v5) (- e7))))
(let ((e25 (<= v1 v2)))
(let ((e26 (> (- v1 v2) (- e7))))
(let ((e27 (< v3 v1)))
(let ((e28 (> (- v1 v3) e11)))
(let ((e29 (< (- v0 v3) e9)))
(let ((e30 (<= v2 v3)))
(let ((e31 (>= (- v4 v1) e11)))
(let ((e32 (= (- v3 v1) e11)))
(let ((e33 (distinct v2 v4)))
(let ((e34 (distinct v4 v2)))
(let ((e35 (distinct v4 v4)))
(let ((e36 (>= v3 v2)))
(let ((e37 (> v5 v5)))
(let ((e38 (> v2 v3)))
(let ((e39 (> v5 v5)))
(let ((e40 (= (- v4 v1) (- e9))))
(let ((e41 (< (- v1 v5) e10)))
(let ((e42 (= (- v0 v4) e8)))
(let ((e43 (<= (- v5 v3) e7)))
(let ((e44 (distinct v2 v4)))
(let ((e45 (= v1 v1)))
(let ((e46 (= (- v3 v4) e6)))
(let ((e47 (>= v0 v0)))
(let ((e48 (distinct v1 v2)))
(let ((e49 (< v3 v2)))
(let ((e50 (> v2 v4)))
(let ((e51 (distinct (- v1 v0) e6)))
(let ((e52 (<= v0 v1)))
(let ((e53 (distinct v2 v5)))
(let ((e54 (distinct (- v4 v1) e7)))
(let ((e55 (< v2 v4)))
(let ((e56 (>= v2 v2)))
(let ((e57 (distinct (- v0 v4) e7)))
(let ((e58 (= v0 v1)))
(let ((e59 (>= v4 v3)))
(let ((e60 (distinct (- v2 v2) (- e9))))
(let ((e61 (> v5 v1)))
(let ((e62 (distinct (- v2 v2) (- e8))))
(let ((e63 (distinct (- v1 v1) e6)))
(let ((e64 (= (- v4 v0) e6)))
(let ((e65 (distinct (- v1 v0) (- e7))))
(let ((e66 (= (- v0 v3) (- e6))))
(let ((e67 (distinct (- v2 v5) (- e11))))
(let ((e68 (<= (- v4 v2) (- e11))))
(let ((e69 (>= (- v3 v5) (- e7))))
(let ((e70 (< (- v5 v2) (- e9))))
(let ((e71 (= (- v1 v1) e10)))
(let ((e72 (distinct (- v1 v1) e9)))
(let ((e73 (< v4 v4)))
(let ((e74 (< v0 v0)))
(let ((e75 (ite e24 e56 e67)))
(let ((e76 (not e48)))
(let ((e77 (=> e18 e49)))
(let ((e78 (= e12 e64)))
(let ((e79 (ite e75 e63 e14)))
(let ((e80 (ite e57 e55 e72)))
(let ((e81 (ite e36 e60 e59)))
(let ((e82 (and e20 e69)))
(let ((e83 (xor e73 e41)))
(let ((e84 (xor e13 e68)))
(let ((e85 (= e61 e35)))
(let ((e86 (ite e82 e46 e53)))
(let ((e87 (ite e44 e83 e38)))
(let ((e88 (xor e40 e26)))
(let ((e89 (ite e47 e27 e54)))
(let ((e90 (= e51 e58)))
(let ((e91 (= e85 e77)))
(let ((e92 (not e30)))
(let ((e93 (ite e42 e79 e79)))
(let ((e94 (xor e50 e45)))
(let ((e95 (and e25 e16)))
(let ((e96 (xor e29 e17)))
(let ((e97 (= e71 e80)))
(let ((e98 (xor e32 e65)))
(let ((e99 (ite e96 e70 e34)))
(let ((e100 (xor e39 e28)))
(let ((e101 (and e100 e86)))
(let ((e102 (not e97)))
(let ((e103 (xor e93 e43)))
(let ((e104 (ite e90 e19 e84)))
(let ((e105 (or e92 e23)))
(let ((e106 (= e103 e94)))
(let ((e107 (= e105 e99)))
(let ((e108 (not e37)))
(let ((e109 (=> e102 e104)))
(let ((e110 (or e31 e76)))
(let ((e111 (or e110 e101)))
(let ((e112 (= e52 e88)))
(let ((e113 (or e108 e107)))
(let ((e114 (=> e98 e78)))
(let ((e115 (=> e113 e106)))
(let ((e116 (=> e111 e66)))
(let ((e117 (= e95 e112)))
(let ((e118 (not e117)))
(let ((e119 (xor e33 e89)))
(let ((e120 (=> e74 e116)))
(let ((e121 (not e119)))
(let ((e122 (or e114 e87)))
(let ((e123 (and e122 e21)))
(let ((e124 (and e120 e22)))
(let ((e125 (and e62 e124)))
(let ((e126 (xor e81 e81)))
(let ((e127 (=> e91 e121)))
(let ((e128 (= e118 e115)))
(let ((e129 (and e127 e109)))
(let ((e130 (= e128 e128)))
(let ((e131 (or e130 e126)))
(let ((e132 (and e15 e125)))
(let ((e133 (and e123 e131)))
(let ((e134 (and e133 e132)))
(let ((e135 (=> e129 e129)))
(let ((e136 (or e134 e134)))
(let ((e137 (and e135 e136)))
e137
)))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))))

(check-sat)