Sequence models are still self referential

[LeventErkok]

This is a follow-up to #2019

That benchmark is now producing unsat; but I'm still seeing the self-referential models coming out from z3 that I built just now: Here's an example benchmark:

(set-option :produce-models true)
(set-logic ALL)
(define-fun s4 () Int 1)
(define-fun s15 () Int 0)
(define-fun s2 () (Seq Int) (as seq.empty (Seq Int)))
(declare-fun s0 () Int) ; tracks user variable "x"
(declare-fun s1 () (Seq Int)) ; tracks user variable "xs"
(declare-fun s13 () Int) ; tracks user variable "__internal_sbv_s13"
(declare-fun s23 () Int) ; tracks user variable "__internal_sbv_s23"
(declare-fun s41 () Int) ; tracks user variable "__internal_sbv_s41"
(declare-fun s50 () Int) ; tracks user variable "__internal_sbv_s50"
(declare-fun s72 () Int) ; tracks user variable "__internal_sbv_s72"
(declare-fun s81 () Int) ; tracks user variable "__internal_sbv_s81"
(declare-fun s99 () Int) ; tracks user variable "__internal_sbv_s99"
(declare-fun s108 () Int) ; tracks user variable "__internal_sbv_s108"
(declare-fun rev ((Seq Int)) (Seq Int))
(define-fun s3 () Bool (= s1 s2))
(define-fun s5 () Int (seq.len s1))
(define-fun s6 () Int (- s5 s4))
(define-fun s7 () (Seq Int) (seq.extract s1 s4 s6))
(define-fun s8 () Bool (= s2 s7))
(define-fun s9 () Int (seq.len s7))
(define-fun s10 () Int (- s9 s4))
(define-fun s11 () (Seq Int) (seq.extract s7 s4 s10))
(define-fun s12 () (Seq Int) (rev s11))
(define-fun s14 () (Seq Int) (seq.unit s13))
(define-fun s16 () Bool (> s9 s15))
(define-fun s17 () Bool (not s16))
(define-fun s18 () (Seq Int) (seq.extract s7 s15 s4))
(define-fun s19 () Bool (= s14 s18))
(define-fun s20 () Bool (or s17 s19))
(define-fun s21 () (Seq Int) (seq.++ s12 s14))
(define-fun s22 () (Seq Int) (ite s8 s2 s21))
(define-fun s24 () (Seq Int) (seq.unit s23))
(define-fun s25 () Bool (> s5 s15))
(define-fun s26 () Bool (not s25))
(define-fun s27 () (Seq Int) (seq.extract s1 s15 s4))
(define-fun s28 () Bool (= s24 s27))
(define-fun s29 () Bool (or s26 s28))
(define-fun s30 () (Seq Int) (seq.++ s22 s24))
(define-fun s31 () (Seq Int) (ite s3 s2 s30))
(define-fun s32 () Bool (= s2 s31))
(define-fun s33 () Int (seq.len s31))
(define-fun s34 () Int (- s33 s4))
(define-fun s35 () (Seq Int) (seq.extract s31 s4 s34))
(define-fun s36 () Bool (= s2 s35))
(define-fun s37 () Int (seq.len s35))
(define-fun s38 () Int (- s37 s4))
(define-fun s39 () (Seq Int) (seq.extract s35 s4 s38))
(define-fun s40 () (Seq Int) (rev s39))
(define-fun s42 () (Seq Int) (seq.unit s41))
(define-fun s43 () Bool (> s37 s15))
(define-fun s44 () Bool (not s43))
(define-fun s45 () (Seq Int) (seq.extract s35 s15 s4))
(define-fun s46 () Bool (= s42 s45))
(define-fun s47 () Bool (or s44 s46))
(define-fun s48 () (Seq Int) (seq.++ s40 s42))
(define-fun s49 () (Seq Int) (ite s36 s2 s48))
(define-fun s51 () (Seq Int) (seq.unit s50))
(define-fun s52 () Bool (> s33 s15))
(define-fun s53 () Bool (not s52))
(define-fun s54 () (Seq Int) (seq.extract s31 s15 s4))
(define-fun s55 () Bool (= s51 s54))
(define-fun s56 () Bool (or s53 s55))
(define-fun s57 () (Seq Int) (seq.++ s49 s51))
(define-fun s58 () (Seq Int) (ite s32 s2 s57))
(define-fun s59 () Bool (= s1 s58))
(define-fun s60 () Bool (not s59))
(define-fun s61 () (Seq Int) (seq.unit s0))
(define-fun s62 () (Seq Int) (seq.++ s61 s1))
(define-fun s63 () Bool (= s2 s62))
(define-fun s64 () Int (seq.len s62))
(define-fun s65 () Int (- s64 s4))
(define-fun s66 () (Seq Int) (seq.extract s62 s4 s65))
(define-fun s67 () Bool (= s2 s66))
(define-fun s68 () Int (seq.len s66))
(define-fun s69 () Int (- s68 s4))
(define-fun s70 () (Seq Int) (seq.extract s66 s4 s69))
(define-fun s71 () (Seq Int) (rev s70))
(define-fun s73 () (Seq Int) (seq.unit s72))
(define-fun s74 () Bool (> s68 s15))
(define-fun s75 () Bool (not s74))
(define-fun s76 () (Seq Int) (seq.extract s66 s15 s4))
(define-fun s77 () Bool (= s73 s76))
(define-fun s78 () Bool (or s75 s77))
(define-fun s79 () (Seq Int) (seq.++ s71 s73))
(define-fun s80 () (Seq Int) (ite s67 s2 s79))
(define-fun s82 () (Seq Int) (seq.unit s81))
(define-fun s83 () Bool (> s64 s15))
(define-fun s84 () Bool (not s83))
(define-fun s85 () (Seq Int) (seq.extract s62 s15 s4))
(define-fun s86 () Bool (= s82 s85))
(define-fun s87 () Bool (or s84 s86))
(define-fun s88 () (Seq Int) (seq.++ s80 s82))
(define-fun s89 () (Seq Int) (ite s63 s2 s88))
(define-fun s90 () Bool (= s2 s89))
(define-fun s91 () Int (seq.len s89))
(define-fun s92 () Int (- s91 s4))
(define-fun s93 () (Seq Int) (seq.extract s89 s4 s92))
(define-fun s94 () Bool (= s2 s93))
(define-fun s95 () Int (seq.len s93))
(define-fun s96 () Int (- s95 s4))
(define-fun s97 () (Seq Int) (seq.extract s93 s4 s96))
(define-fun s98 () (Seq Int) (rev s97))
(define-fun s100 () (Seq Int) (seq.unit s99))
(define-fun s101 () Bool (> s95 s15))
(define-fun s102 () Bool (not s101))
(define-fun s103 () (Seq Int) (seq.extract s93 s15 s4))
(define-fun s104 () Bool (= s100 s103))
(define-fun s105 () Bool (or s102 s104))
(define-fun s106 () (Seq Int) (seq.++ s98 s100))
(define-fun s107 () (Seq Int) (ite s94 s2 s106))
(define-fun s109 () (Seq Int) (seq.unit s108))
(define-fun s110 () Bool (> s91 s15))
(define-fun s111 () Bool (not s110))
(define-fun s112 () (Seq Int) (seq.extract s89 s15 s4))
(define-fun s113 () Bool (= s109 s112))
(define-fun s114 () Bool (or s111 s113))
(define-fun s115 () (Seq Int) (seq.++ s107 s109))
(define-fun s116 () (Seq Int) (ite s90 s2 s115))
(define-fun s117 () Bool (= s62 s116))
(define-fun s118 () Bool (or s60 s117))
(assert s20)
(assert s29)
(assert s47)
(assert s56)
(assert s78)
(assert s87)
(assert s105)
(assert s114)
(assert (not s118))
(check-sat)
(get-value (s1))

[NikolajBjorner]

at least this model now looks sane.

[LeventErkok]

Looks good to me; did some extra testing and didn't see anything funky. Thanks!