Soundness issue with sequences

[LeventErkok]

The following benchmark is unsat; but latest z3 gives a bogus model for it. Good news is that it knows the model it generated is invalid:

$ z3 bad.smt2 model_validate=true
sat
(error "line 182 column 10: an invalid model was generated")

I've a version of z3 compiled on October 29 2019 from github, which successfully says unsat on this benchmark. So, the issue must've crept in sometime in the last 3 months.

Here's the benchmark: (It tries to perform BMC on a mutual-exclusion protocol.)

(set-option :produce-models true)
(set-logic ALL)
(declare-datatypes ((State 0)) (((Idle) (Ready) (Critical))))
(define-fun State_constrIndex ((x State)) Int
   (ite (= x Idle) 0 (ite (= x Ready) 1 2))
)
(define-fun s4 () Int 3)
(define-fun s6 () State Idle)
(define-fun s7 () Int 0)
(define-fun s10 () State Ready)
(define-fun s13 () Int 1)
(define-fun s26 () State Critical)
(define-fun s69 () Int 2)
(define-fun s126 () (Seq Bool) (as seq.empty (Seq Bool)))
(declare-fun s0 () (Seq State))
(declare-fun s1 () (Seq State))
(declare-fun s2 () (Seq Int))
(define-fun s3 () Int (seq.len s0))
(define-fun s5 () Bool (= s3 s4))
(define-fun s8 () State (seq.nth s0 s7))
(define-fun s9 () Bool (= s6 s8))
(define-fun s11 () Bool (= s8 s10))
(define-fun s12 () Bool (or s9 s11))
(define-fun s14 () Int (- s3 s13))
(define-fun s15 () (Seq State) (seq.extract s0 s13 s14))
(define-fun s16 () State (seq.nth s15 s7))
(define-fun s17 () Bool (= s6 s16))
(define-fun s18 () Bool (= s10 s16))
(define-fun s19 () Bool (or s17 s18))
(define-fun s20 () Int (seq.len s2))
(define-fun s21 () Int (- s20 s13))
(define-fun s22 () (Seq Int) (seq.extract s2 s13 s21))
(define-fun s23 () Int (seq.nth s22 s7))
(define-fun s24 () Bool (= s13 s23))
(define-fun s25 () Bool (and s11 s24))
(define-fun s27 () Bool (= s16 s26))
(define-fun s28 () Bool (= s8 s26))
(define-fun s29 () Bool (or s17 s27))
(define-fun s30 () Bool (= s8 s16))
(define-fun s31 () Bool (ite s28 s29 s30))
(define-fun s32 () Bool (ite s25 s27 s31))
(define-fun s33 () Bool (ite s9 s19 s32))
(define-fun s34 () Int (seq.len s15))
(define-fun s35 () Int (- s34 s13))
(define-fun s36 () (Seq State) (seq.extract s15 s13 s35))
(define-fun s37 () State (seq.nth s36 s7))
(define-fun s38 () Bool (= s6 s37))
(define-fun s39 () Bool (= s10 s37))
(define-fun s40 () Bool (or s38 s39))
(define-fun s41 () Int (seq.len s22))
(define-fun s42 () Int (- s41 s13))
(define-fun s43 () (Seq Int) (seq.extract s22 s13 s42))
(define-fun s44 () Int (seq.nth s43 s7))
(define-fun s45 () Bool (= s13 s44))
(define-fun s46 () Bool (and s18 s45))
(define-fun s47 () Bool (= s26 s37))
(define-fun s48 () Bool (or s38 s47))
(define-fun s49 () Bool (= s16 s37))
(define-fun s50 () Bool (ite s27 s48 s49))
(define-fun s51 () Bool (ite s46 s47 s50))
(define-fun s52 () Bool (ite s17 s40 s51))
(define-fun s53 () Bool (and s33 s52))
(define-fun s54 () Bool (and s12 s53))
(define-fun s55 () Bool (and s9 s54))
(define-fun s56 () Bool (and s5 s55))
(define-fun s57 () Int (seq.len s1))
(define-fun s58 () Bool (= s4 s57))
(define-fun s59 () State (seq.nth s1 s7))
(define-fun s60 () Bool (= s6 s59))
(define-fun s61 () Bool (= s10 s59))
(define-fun s62 () Bool (or s60 s61))
(define-fun s63 () Int (- s57 s13))
(define-fun s64 () (Seq State) (seq.extract s1 s13 s63))
(define-fun s65 () State (seq.nth s64 s7))
(define-fun s66 () Bool (= s6 s65))
(define-fun s67 () Bool (= s10 s65))
(define-fun s68 () Bool (or s66 s67))
(define-fun s70 () Bool (= s23 s69))
(define-fun s71 () Bool (and s61 s70))
(define-fun s72 () Bool (= s26 s65))
(define-fun s73 () Bool (= s26 s59))
(define-fun s74 () Bool (or s66 s72))
(define-fun s75 () Bool (= s59 s65))
(define-fun s76 () Bool (ite s73 s74 s75))
(define-fun s77 () Bool (ite s71 s72 s76))
(define-fun s78 () Bool (ite s60 s68 s77))
(define-fun s79 () Int (seq.len s64))
(define-fun s80 () Int (- s79 s13))
(define-fun s81 () (Seq State) (seq.extract s64 s13 s80))
(define-fun s82 () State (seq.nth s81 s7))
(define-fun s83 () Bool (= s6 s82))
(define-fun s84 () Bool (= s10 s82))
(define-fun s85 () Bool (or s83 s84))
(define-fun s86 () Bool (= s44 s69))
(define-fun s87 () Bool (and s67 s86))
(define-fun s88 () Bool (= s26 s82))
(define-fun s89 () Bool (or s83 s88))
(define-fun s90 () Bool (= s65 s82))
(define-fun s91 () Bool (ite s72 s89 s90))
(define-fun s92 () Bool (ite s87 s88 s91))
(define-fun s93 () Bool (ite s66 s85 s92))
(define-fun s94 () Bool (and s78 s93))
(define-fun s95 () Bool (and s62 s94))
(define-fun s96 () Bool (and s60 s95))
(define-fun s97 () Bool (and s58 s96))
(define-fun s98 () Bool (= s4 s20))
(define-fun s99 () Int (seq.nth s2 s7))
(define-fun s100 () Bool (= s13 s99))
(define-fun s101 () Bool (= s69 s99))
(define-fun s102 () Bool (or s100 s101))
(define-fun s103 () Bool (or s28 s73))
(define-fun s104 () Bool (not s103))
(define-fun s105 () Bool (or s100 s104))
(define-fun s106 () Bool (or s24 s70))
(define-fun s107 () Bool (or s27 s72))
(define-fun s108 () Bool (not s107))
(define-fun s109 () Bool (= s23 s99))
(define-fun s110 () Bool (or s108 s109))
(define-fun s111 () Bool (or s45 s86))
(define-fun s112 () Bool (or s47 s88))
(define-fun s113 () Bool (not s112))
(define-fun s114 () Bool (= s23 s44))
(define-fun s115 () Bool (or s113 s114))
(define-fun s116 () Bool (and s111 s115))
(define-fun s117 () Bool (and s110 s116))
(define-fun s118 () Bool (and s106 s117))
(define-fun s119 () Bool (and s105 s118))
(define-fun s120 () Bool (and s102 s119))
(define-fun s121 () Bool (and s100 s120))
(define-fun s122 () Bool (and s98 s121))
(define-fun s123 () Bool (= s3 s7))
(define-fun s124 () Bool (= s7 s57))
(define-fun s125 () Bool (or s123 s124))
(define-fun s127 () Bool (distinct s8 s26))
(define-fun s128 () Bool (distinct s26 s59))
(define-fun s129 () Bool (or s127 s128))
(define-fun s130 () (Seq Bool) (seq.unit s129))
(define-fun s131 () Bool (= s7 s34))
(define-fun s132 () Bool (= s7 s79))
(define-fun s133 () Bool (or s131 s132))
(define-fun s134 () Bool (distinct s16 s26))
(define-fun s135 () Bool (distinct s26 s65))
(define-fun s136 () Bool (or s134 s135))
(define-fun s137 () (Seq Bool) (seq.unit s136))
(define-fun s138 () Int (seq.len s36))
(define-fun s139 () Bool (= s7 s138))
(define-fun s140 () Int (seq.len s81))
(define-fun s141 () Bool (= s7 s140))
(define-fun s142 () Bool (or s139 s141))
(define-fun s143 () Bool (distinct s26 s37))
(define-fun s144 () Bool (distinct s26 s82))
(define-fun s145 () Bool (or s143 s144))
(define-fun s146 () (Seq Bool) (seq.unit s145))
(define-fun s147 () (Seq Bool) (ite s142 s126 s146))
(define-fun s148 () (Seq Bool) (seq.++ s137 s147))
(define-fun s149 () (Seq Bool) (ite s133 s126 s148))
(define-fun s150 () (Seq Bool) (seq.++ s130 s149))
(define-fun s151 () (Seq Bool) (ite s125 s126 s150))
(define-fun s152 () Int (seq.len s151))
(define-fun s153 () Bool (= s7 s152))
(define-fun s154 () Bool (seq.nth s151 s7))
(define-fun s155 () Int (- s152 s13))
(define-fun s156 () (Seq Bool) (seq.extract s151 s13 s155))
(define-fun s157 () Int (seq.len s156))
(define-fun s158 () Bool (= s7 s157))
(define-fun s159 () Bool (seq.nth s156 s7))
(define-fun s160 () Int (- s157 s13))
(define-fun s161 () (Seq Bool) (seq.extract s156 s13 s160))
(define-fun s162 () Int (seq.len s161))
(define-fun s163 () Bool (= s7 s162))
(define-fun s164 () Bool (seq.nth s161 s7))
(define-fun s165 () Bool (or s163 s164))
(define-fun s166 () Bool (and s159 s165))
(define-fun s167 () Bool (or s158 s166))
(define-fun s168 () Bool (and s154 s167))
(define-fun s169 () Bool (or s153 s168))
(define-fun s170 () Bool (not s169))
(assert s56)
(assert s97)
(assert s122)
(assert s170)
(check-sat)

[zhendongsu]

Below is a much simpler reduced formula that should trigger the same issue; hope it is of use:

[515] % z3 small.smt2
sat
[516] % z3 model_validate=true small.smt2
sat
(error "line 16 column 10: an invalid model was generated")
[517] % 
[517] % cat small.smt2
(declare-datatypes ((a 0)) (((b))))
(define-fun v () (Seq Bool) (as seq.empty (Seq Bool)))
(declare-fun e () (Seq a))
(define-fun w () Int (seq.len e))
(define-fun x () (Seq a) (seq.extract e 1 (- w 1)))
(define-fun i () (Seq a) (seq.extract x 1 (- (seq.len x) 1)))
(define-fun y () (Seq Bool) (ite (= 0 (seq.len i)) v (seq.unit true)))
(define-fun m () (Seq Bool) (seq.++ (seq.unit false) y))
(define-fun n () (Seq Bool) (ite (= 0 (seq.len x)) v m))
(define-fun o () (Seq Bool) (seq.++ (seq.unit false) n))
(define-fun p () (Seq Bool) (ite (= 0 w) v o))
(define-fun s () (Seq Bool) (seq.extract p 1 (- (seq.len p) 1)))
(define-fun u () (Seq Bool) (seq.extract s 1 (- (seq.len s) 1)))
(assert (distinct 0 (seq.len u)))
(assert (not (seq.nth u 0)))
(check-sat)
[518] % 

[NikolajBjorner]

The much shorter examples help tremendously. There is significant context switching and then investigation involved in debugging these and it is sometimes very time consuming to identify the root cause of a single bug.

[NikolajBjorner]

this now produces unsat. It was very likely fixed when addressing unsound handling of "at".

[LeventErkok]

I can confirm that this works now. But I'm getting a bunch of other failures elsewhere. I'll take a look at the new ones.

Thanks!