blob: abafdeddf47bd9c77bec6e08765235bde8bf13ca (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(set-logic QF_SLIA)
(set-info :status unsat)
(declare-fun x () (Seq (Seq Int)))
(declare-fun xp () (Seq (Seq Int)))
(declare-fun y () (Seq (Seq Int)))
(declare-fun yp () (Seq (Seq Int)))
(declare-fun z () (Seq Int))
(declare-fun w () (Seq Int))
(declare-fun i () Int)
(declare-fun j () Int)
(declare-fun n () Int)
(assert (> i j))
(assert (= (seq.extract z n 1) (seq.unit i)))
(assert (= (seq.extract w n 1) (seq.unit j)))
(assert (= x (seq.++ (seq.unit z) xp)))
(assert (= y (seq.++ (seq.unit w) yp)))
(assert (= x y))
(check-sat)
|
