summaryrefslogtreecommitdiff
path: root/test/regress/regress0/seq/seq-ex5-dd.smt2
blob: d9ef5c8ba5829c0ede06cce7c602e1b4e0d82e79 (plain) 
1
2
3
4
5
6
7
8

(set-logic QF_SLIA)
(set-info :status sat)
(declare-fun z () (Seq Int))
(declare-fun i () Int)
(declare-fun n () Int)
(assert (> i 777))
(assert (= (seq.extract z n 1) (seq.unit i)))
(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback