blob: 2f86a2764bec024ed868fd47f84d16aeac72a8a5 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
|
(set-logic ALL)
(set-info :status unsat)
(declare-sort S 0)
(declare-datatypes ((Y 0) (St 0)) (((err)) ((t (|v#t| S) (|l#t| Int)))))
(declare-sort Q 0)
(declare-datatypes ((T 0) (TArray 0)) (((b (B Bool)) (D (add Int)) (Vec (vec TArray))) ((zValueArray (R Q)))))
(declare-sort U 0)
(declare-datatypes ((Sm 0)) (((m (cm U)))))
(declare-fun O (Y) S)
(declare-fun s (T T) Bool)
(declare-fun j (Q Int) T)
(declare-fun K (S Int Y) S)
(declare-fun r () Int)
(declare-fun c () Int)
(declare-fun h (U St Int) T)
(declare-fun a () Sm)
(declare-fun e () T)
(declare-fun l () T)
(declare-fun n () Y)
(assert (forall ((v T) (v2 T)) (! (or (= v v2) (not (s v v2))) :qid Q1)))
(assert (B (b (s l (j (R (vec (h (cm a) (t (K (O err) 0 n) 1) (add (D 1))))) r)))))
(assert (forall ((i Int)) (! (not (s e (j (R (vec (j (R (vec l)) c))) i))) :qid Q2)))
(assert (exists ((z Int)) (! (B (b (s e (j (R (vec (j (R (vec (j (R (vec (h (cm a) (t (K (O err) 0 n) 1) (add (D 1))))) r))) c))) z)))) :qid Q3)))
(check-sat)
|
