Open
Description
Again, about a month ago version old of z3 was able to answer this benchmark unsat pretty quickly. Right now it seems to be taking forever:
(set-logic ALL)
(define-fun s3 () Int 0)
(define-fun s6 () Int 1)
(declare-fun s0 () (Seq Int))
(declare-fun s1 () Int)
(declare-fun s2 () Int)
(define-fun s4 () Bool (>= s1 s3))
(define-fun s5 () Int (seq.len s0))
(define-fun s7 () Int (- s5 s6))
(define-fun s8 () Bool (<= s1 s7))
(define-fun s9 () Bool (and s4 s8))
(define-fun s10 () Int (seq.nth s0 s1))
(define-fun s11 () Bool (= s2 s10))
(define-fun s12 () Bool (and s9 s11))
(define-fun s13 () Bool (not s12))
(define-fun s14 () (Seq Int) (seq.unit s2))
(define-fun s15 () Int (seq.indexof s0 s14 s3))
(define-fun s16 () Bool (<= s15 s1))
(define-fun s17 () Bool (or s13 s16))
(assert (not s17))
(check-sat)