heap-use-after-free on QF_LIA formula

[rainoftime]

Hi, for the following formula,
z3 40159a3

(set-logic QF_LIA)
(set-option :smt.arith.bounded_expansion true)
(declare-fun v3 () Bool)
(declare-fun i1 () Int)
(declare-fun i4 () Int)
(declare-fun i6 () Int)
(declare-fun v4 () Bool)
(declare-fun v5 () Bool)
(declare-fun v17 () Bool)
(assert (< (+ 0 981 95 (mod i6 421) i6) 19))
(assert-soft (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4)))
(assert-soft (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4)))
(assert-soft (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4)))
(assert-soft (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4)))
(assert-soft (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)))
(assert-soft (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)))
(assert-soft (and (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (or true (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) true) (or true true true) (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4))))
(assert-soft (and (or (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4)) (or true true (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19))) (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) true) (or true (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) true) (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4)) (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (or (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4)) (or true true (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19))) (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) true (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4)) (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4)) (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19))))
(assert-soft (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4)))
(assert-soft (=> (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) true (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (and (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) true (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4)) (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) true (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (or true (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) true) (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (or true (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4)) (or true (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)))))
(assert-soft (and (=> (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4)) (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) true (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19))) (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (or true true (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (or (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (and (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4)) (and (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4)))) (or (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19)) (or true (xor v5 (= (= (> i1 i4 i6 i6 26) true) (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3)))) v17 (and (<= i4 i1) (> (- (- 26 95 (abs (mod i6 421)) (mod 95 18) (abs 95)) i4) 409) (xor v5 (not v3))) (>= (+ 981 95) (mod i6 421)) v4) (< (+ (+ (div (+ 19 73 i6 (abs 95) 19) 339) (+ 981 95)) 981 95 (abs (mod i6 421)) i6) 19))))
(check-sat)

=================================================================
==96425==ERROR: AddressSanitizer: heap-use-after-free on address 0x6070001e5a34 at pc 0x00000047c25b bp 0x7ffd6f363de0 sp 0x7ffd6f363dd0
READ of size 4 at 0x6070001e5a34 thread T0
    #0 0x47c25a in ast::hash() const ../src/ast/ast.h:501
    #1 0x5e918d in obj_map<expr, expr*>::key_data::hash() const ../src/util/obj_hashtable.h:77
    #2 0x5e8565 in obj_map<expr, expr*>::obj_map_entry::get_hash() const ../src/util/obj_hashtable.h:86
    #3 0x5e827b in core_hashtable<obj_map<expr, expr*>::obj_map_entry, obj_hash<obj_map<expr, expr*>::key_data>, default_eq<obj_map<expr, expr*>::key_data> >::find_core(obj_map<expr, expr*>::key_data const&) const ../src/util/hashtable.h:517
    #4 0x5e6958 in obj_map<expr, expr*>::find_core(expr*) const ../src/util/obj_hashtable.h:157
    #5 0x6a1342 in obj_map<expr, expr*>::find(expr*, expr*&) const ../src/util/obj_hashtable.h:161
    #6 0x11e3717 in smt::theory_lra::imp::should_research(ref_vector<expr, ast_manager>&) (/home/peisen/test/tofuzz/z3-debug/build/z3+0x11e3717)
    #7 0x11b1857 in smt::theory_lra::should_research(ref_vector<expr, ast_manager>&) ../src/smt/theory_lra.cpp:3952
    #8 0xfa85f2 in smt::context::should_research(lbool) ../src/smt/smt_context.cpp:3327
    #9 0xfaac06 in smt::context::check(unsigned int, expr* const*, bool) ../src/smt/smt_context.cpp:3563
    #10 0xd0fffc in smt::kernel::imp::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:116
    #11 0xd0de0d in smt::kernel::check(unsigned int, expr* const*) ../src/smt/smt_kernel.cpp:330
    #12 0x5dc2b2 in opt::opt_solver::check_sat_core2(unsigned int, expr* const*) ../src/opt/opt_solver.cpp:189
    #13 0x1b82221 in solver_na2as::check_sat_core(unsigned int, expr* const*) ../src/solver/solver_na2as.cpp:67
    #14 0x1b864be in solver::check_sat(unsigned int, expr* const*) ../src/solver/solver.cpp:332
    #15 0x5ec0ff in maxres::check_sat(unsigned int, expr* const*) ../src/opt/maxres.cpp:313
    #16 0x5ebf54 in maxres::check_sat_hill_climb(ref_vector<expr, ast_manager>&) ../src/opt/maxres.cpp:303
    #17 0x5eb28d in maxres::mus_solver() ../src/opt/maxres.cpp:209
    #18 0x5ec4eb in maxres::operator()() ../src/opt/maxres.cpp:344
    #19 0x5cf829 in opt::maxsmt::operator()() ../src/opt/maxsmt.cpp:264
    #20 0x5938c3 in opt::context::execute_maxsat(symbol const&, bool, bool) ../src/opt/opt_context.cpp:428
    #21 0x593c1d in opt::context::execute(opt::context::objective const&, bool, bool) ../src/opt/opt_context.cpp:442
    #22 0x5923d3 in opt::context::optimize(ref_vector<expr, ast_manager> const&) ../src/opt/opt_context.cpp:335
    #23 0x1b3f549 in cmd_context::check_sat(unsigned int, expr* const*) ../src/cmd_context/cmd_context.cpp:1541
    #24 0x1aeb4b1 in smt2::parser::parse_check_sat() ../src/parsers/smt2/smt2parser.cpp:2596
    #25 0x1aef40d in smt2::parser::parse_cmd() ../src/parsers/smt2/smt2parser.cpp:2938
    #26 0x1af0b05 in smt2::parser::operator()() ../src/parsers/smt2/smt2parser.cpp:3130
    #27 0x1acfb5b in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&, char const*) ../src/parsers/smt2/smt2parser.cpp:3179
    #28 0x43eb31 in read_smtlib2_commands(char const*) ../src/shell/smtlib_frontend.cpp:142
    #29 0x4696b6 in main ../src/shell/main.cpp:372
    #30 0x7fc64deb183f in __libc_start_main (/lib/x86_64-linux-gnu/libc.so.6+0x2083f)