blob: 4fe2a85a9b48e84eefe1a15b96a57b22e26c5071 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
|
; COMMAND-LINE: --strings-exp -q
;EXPECT: unsat
(set-logic ALL)
(declare-fun s () (Seq Int))
(declare-fun n () Int)
(assert (=> (and (<= 0 n ) (< n (seq.len s))) (= (seq.nth s n) 6)))
(assert (=> (>= 0 n) (= (seq.nth s n) 7)))
(assert (=> (>= n (seq.len s)) (= (seq.nth s n) 8)))
(assert (distinct (seq.unit 6) (seq.extract s n 1)))
(assert (distinct (seq.unit 7) (seq.extract s n 1)))
(assert (distinct (seq.unit 8) (seq.extract s n 1)))
(assert (> n 0))
(assert (< n (seq.len s)))
(assert (> (seq.len s) 0))
(check-sat)
|
