test/regress/regress1/quantifiers/seq-solved-enum.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17

; COMMAND-LINE: --strings-exp --full-saturate-quant
; EXPECT: unsat
(set-logic ALL)

(declare-fun s () (Seq Int))

(declare-fun x () Int)

(declare-fun y () Int)

(assert (and (<= 0 x) (<= x y) (< y (seq.len s))))

(assert (forall ((i Int) (j Int)) (=> (and (<= 0 i) (<= i j) (< j (seq.len s))) (<= (seq.nth s i) (seq.nth s j)))))

(assert (not (<= (seq.nth s x) (seq.nth s y))))

(check-sat)