search

ultimate-pa / smtinterpol

SMTInterpol interpolating SMT solver
GNU Lesser General Public License v3.0
60 stars 17 forks source link

NullPointerException on QF_ALIA formula (produce-interpolants, interpolant-check-mode) #87

Closed rainoftime closed 4 years ago

rainoftime commented 4 years ago

Hi, for the following formula,

SMTInterpol (commit 8719a86) throws a NPD

rainoftime commented 4 years ago 
(set-option :produce-interpolants true)
(set-option :interpolant-check-mode true)
(set-logic QF_ALIA)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v10 Bool)
(declare-const i0 Int)
(declare-const i3 Int)
(declare-const i4 Int)
(declare-const v11 Bool)
(declare-const v12 Bool)
(declare-const i8 Int)
(declare-const v13 Bool)
(declare-const v14 Bool)
(declare-const arr--3920153197951843945_5243811257660301665-0 (Array Int Bool))
(declare-const arr-2821965189590592473_-3920153197951843945-0 (Array (Array Int Bool) Int))
(declare-const v15 Bool)
(declare-const arr-2821965189590592473_5243811257660301665-0 (Array (Array Int Bool) Bool))
(declare-const arr--3920153197951843945_5243811257660301665-2 (Array Int Bool))
(declare-const arr--3920153197951843945_2821965189590592473-0 (Array Int (Array Int Bool)))
(declare-const v16 Bool)
(declare-const arr--89796910704405183_-6818947020679966917-0 (Array (Array Int (Array Int Bool)) (Array (Array Int Bool) Bool)))
(declare-const v18 Bool)
(declare-const arr--89796910704405183_7863748300854297453-0 (Array (Array Int (Array Int Bool)) (Array (Array Int (Array Int Bool)) (Array (Array Int Bool) Bool))))
(declare-const i9 Int)
(declare-const arr--89796910704405183_2821965189590592473-0 (Array (Array Int (Array Int Bool)) (Array Int Bool)))
(declare-const arr--89796910704405183_-8219425927650061733-0 (Array (Array Int (Array Int Bool)) (Array (Array Int (Array Int Bool)) (Array Int Bool))))
(declare-const v19 Bool)
(declare-const arr-6063138686794276301_-89796910704405183-0 (Array (Array (Array Int (Array Int Bool)) (Array (Array Int (Array Int Bool)) (Array Int Bool))) (Array Int (Array Int Bool))))
(declare-const arr-2821965189590592473_-7866087040585767423-0 (Array (Array Int Bool) (Array (Array Int Bool) Int)))
(declare-const v23 Bool)
(declare-const arr--9002618208544496305_-6818947020679966917-0 (Array (Array (Array (Array Int (Array Int Bool)) (Array (Array Int (Array Int Bool)) (Array Int Bool))) (Array Int (Array Int Bool))) (Array (Array Int Bool) Bool)))
(declare-const v24 Bool)
(declare-const arr--3920153197951843945_-7866087040585767423-0 (Array Int (Array (Array Int Bool) Int)))
(declare-const arr--4115666975680612581_-9002618208544496305-0 (Array (Array (Array Int Bool) (Array (Array Int Bool) Int)) (Array (Array (Array Int (Array Int Bool)) (Array (Array Int (Array Int Bool)) (Array Int Bool))) (Array Int (Array Int Bool)))))
(declare-const v25 Bool)
(declare-const arr--7928200959372586193_-6818947020679966917-0 (Array (Array (Array Int (Array Int Bool)) (Array (Array Int (Array Int Bool)) (Array (Array Int Bool) Bool))) (Array (Array Int Bool) Bool)))
(declare-const v26 Bool)
(declare-const i10 Int)
(declare-const arr--9002618208544496305_-7928200959372586193-0 (Array (Array (Array (Array Int (Array Int Bool)) (Array (Array Int (Array Int Bool)) (Array Int Bool))) (Array Int (Array Int Bool))) (Array (Array Int (Array Int Bool)) (Array (Array Int (Array Int Bool)) (Array (Array Int Bool) Bool)))))
(declare-const v27 Bool)
(declare-const arr-7863748300854297453_-3988332692865450567-0 (Array (Array (Array Int (Array Int Bool)) (Array (Array Int Bool) Bool)) (Array Int (Array (Array Int Bool) Int))))
(declare-const arr-1616920169858119687_-7866087040585767423-0 (Array (Array (Array (Array Int Bool) (Array (Array Int Bool) Int)) (Array (Array (Array Int (Array Int Bool)) (Array (Array Int (Array Int Bool)) (Array Int Bool))) (Array Int (Array Int Bool)))) (Array (Array Int Bool) Int)))
(declare-const i11 Int)
(declare-const arr--4120804103381795383_-9002618208544496305-0 (Array (Array (Array (Array (Array Int Bool) (Array (Array Int Bool) Int)) (Array (Array (Array Int (Array Int Bool)) (Array (Array Int (Array Int Bool)) (Array Int Bool))) (Array Int (Array Int Bool)))) (Array (Array Int Bool) Int)) (Array (Array (Array Int (Array Int Bool)) (Array (Array Int (Array Int Bool)) (Array Int Bool))) (Array Int (Array Int Bool)))))
(assert (! (or (select (store arr--3920153197951843945_5243811257660301665-0 89 v8) 256) (< 256 (div 33 114)) false) :named IP_1))
(assert (! (or (xor (select (store arr--3920153197951843945_5243811257660301665-0 89 v8) 256) v10 (= 541 (- 941)) (= v5 v11 v12 v13 v2) v15 (= v14 v0 v2 v11) (>= i11 (div (mod (- 29 (div 33 114) i8) 29) 707) (- 941) (abs 89) (- 29 (div 33 114) i8)) (>= (* 972 (div 33 114) 29) 895) (or v23 (distinct 88 (div 147 114)) (= 114 89 147))) (xor (select (store arr--3920153197951843945_5243811257660301665-0 89 v8) 256) v10 (= 541 (- 941)) (= v5 v11 v12 v13 v2) v15 (= v14 v0 v2 v11) (>= i11 (div (mod (- 29 (div 33 114) i8) 29) 707) (- 941) (abs 89) (- 29 (div 33 114) i8)) (>= (* 972 (div 33 114) 29) 895) (or v23 (distinct 88 (div 147 114)) (= 114 89 147))) v6 v25 (not (distinct (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731) (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731) (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731))) v6 (= (and v11 v6 v4 v8 v6 v10 v3 v8 v6 v1 v10) (= (= arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0) v19 v2) v19 v4 (=> v6 v3) v12 (xor (distinct 33 i0 972 i0) (<= 610 33) (distinct 147 i0) v18 v2 v10 v1 (= arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0) (= v2 (not v4) (= v14 v0 v2 v11) v14 v16) v16 v16)) (> i9 731) (=> v6 v3) false) :named IP_2))
(assert (! (or v6 (select (store arr--3920153197951843945_5243811257660301665-0 89 v8) 256) (not (distinct (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731) (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731) (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731))) v25 v6 (< i4 610) (> i9 731) false) :named IP_11))
(assert (! (or (= (and v11 v6 v4 v8 v6 v10 v3 v8 v6 v1 v10) (= (= arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0) v19 v2) v19 v4 (=> v6 v3) v12 (xor (distinct 33 i0 972 i0) (<= 610 33) (distinct 147 i0) v18 v2 v10 v1 (= arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0) (= v2 (not v4) (= v14 v0 v2 v11) v14 v16) v16 v16)) v25 (< 256 (div 33 114)) false) :named IP_12))
(assert (! (or (xor (select (store arr--3920153197951843945_5243811257660301665-0 89 v8) 256) v10 (= 541 (- 941)) (= v5 v11 v12 v13 v2) v15 (= v14 v0 v2 v11) (>= i11 (div (mod (- 29 (div 33 114) i8) 29) 707) (- 941) (abs 89) (- 29 (div 33 114) i8)) (>= (* 972 (div 33 114) 29) 895) (or v23 (distinct 88 (div 147 114)) (= 114 89 147))) (< i4 610) false) :named IP_23))
(assert (! (or (xor (select (store arr--3920153197951843945_5243811257660301665-0 89 v8) 256) v10 (= 541 (- 941)) (= v5 v11 v12 v13 v2) v15 (= v14 v0 v2 v11) (>= i11 (div (mod (- 29 (div 33 114) i8) 29) 707) (- 941) (abs 89) (- 29 (div 33 114) i8)) (>= (* 972 (div 33 114) 29) 895) (or v23 (distinct 88 (div 147 114)) (= 114 89 147))) false) :named IP_24))
(assert (! (or (not (distinct (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731) (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731) (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731))) false) :named IP_25))
(assert (! (or (> i9 731) v25 (< 256 (div 33 114)) false) :named IP_26))
(assert (! (or (> i9 731) false) :named IP_27))
(assert (! (or v6 false) :named IP_28))
(assert (! (or v25 (> i9 731) (= (and v11 v6 v4 v8 v6 v10 v3 v8 v6 v1 v10) (= (= arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0) v19 v2) v19 v4 (=> v6 v3) v12 (xor (distinct 33 i0 972 i0) (<= 610 33) (distinct 147 i0) v18 v2 v10 v1 (= arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0) (= v2 (not v4) (= v14 v0 v2 v11) v14 v16) v16 v16)) (= (and v11 v6 v4 v8 v6 v10 v3 v8 v6 v1 v10) (= (= arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0) v19 v2) v19 v4 (=> v6 v3) v12 (xor (distinct 33 i0 972 i0) (<= 610 33) (distinct 147 i0) v18 v2 v10 v1 (= arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0) (= v2 (not v4) (= v14 v0 v2 v11) v14 v16) v16 v16)) false) :named IP_29))
(assert (! (or (= (and v11 v6 v4 v8 v6 v10 v3 v8 v6 v1 v10) (= (= arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0) v19 v2) v19 v4 (=> v6 v3) v12 (xor (distinct 33 i0 972 i0) (<= 610 33) (distinct 147 i0) v18 v2 v10 v1 (= arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0) (= v2 (not v4) (= v14 v0 v2 v11) v14 v16) v16 v16)) v6 v6 (=> v6 v3) v27 (> i9 731) false) :named IP_30))
(assert (! (or (not (distinct (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731) (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731) (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731))) (< i4 610) (> i9 731) v25 (= (and v11 v6 v4 v8 v6 v10 v3 v8 v6 v1 v10) (= (= arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0) v19 v2) v19 v4 (=> v6 v3) v12 (xor (distinct 33 i0 972 i0) (<= 610 33) (distinct 147 i0) v18 v2 v10 v1 (= arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0) (= v2 (not v4) (= v14 v0 v2 v11) v14 v16) v16 v16)) false) :named IP_31))
(assert (! (or (< i4 610) (=> v6 v3) false) :named IP_32))
(assert (! (or (not (distinct (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731) (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731) (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731))) v6 (= (and v11 v6 v4 v8 v6 v10 v3 v8 v6 v1 v10) (= (= arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0) v19 v2) v19 v4 (=> v6 v3) v12 (xor (distinct 33 i0 972 i0) (<= 610 33) (distinct 147 i0) v18 v2 v10 v1 (= arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0 arr--3920153197951843945_2821965189590592473-0) (= v2 (not v4) (= v14 v0 v2 v11) v14 v16) v16 v16)) false) :named IP_33))
(assert (! (or v25 false) :named IP_34))
(assert (! (or (not (distinct (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731) (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731) (store arr-2821965189590592473_-3920153197951843945-0 arr--3920153197951843945_5243811257660301665-0 731))) (select (store arr--3920153197951843945_5243811257660301665-0 89 v8) 256) v6 false) :named IP_35))
(assert (! (or (< 256 (div 33 114)) false) :named IP_36))
(assert (! (or (> i9 731) v27 (xor (select (store arr--3920153197951843945_5243811257660301665-0 89 v8) 256) v10 (= 541 (- 941)) (= v5 v11 v12 v13 v2) v15 (= v14 v0 v2 v11) (>= i11 (div (mod (- 29 (div 33 114) i8) 29) 707) (- 941) (abs 89) (- 29 (div 33 114) i8)) (>= (* 972 (div 33 114) 29) 895) (or v23 (distinct 88 (div 147 114)) (= 114 89 147))) false) :named IP_38))
(check-sat)
(get-interpolants IP_2 (and IP_12 IP_2))
rainoftime commented 4 years ago

I cannot use ddSMT to reduce the tests. Perhaps I can try the delta debugger provided by SMTInterpol