blob: 8f31750b2e61080fc986395295fd7c430bcaed16 (
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
26
27
28
29
30
31
32
33
34
35
36
37
|
(set-logic ALL)
(set-info :status unsat)
(declare-sort U 0)
(declare-datatypes ((D 0) (T@t 0)) (((err)) ((t (|v#t| U) (|l#t| Int)))))
(declare-sort V 0)
(declare-datatypes ((T 0) (TArray 0)) (((E) (b (B Bool)) (A (add Int)) (Vec (vec TArray))) ((Var (R V) (|l#Var| Int)))))
(declare-sort B 0)
(declare-datatypes ((M 0)) (((Mem (cm B)))))
(declare-fun mc (D) U)
(declare-fun eq (T T) Bool)
(declare-fun s (V Int) T)
(declare-fun sto (V Int T) V)
(declare-fun sel (B T@t Int) T)
(declare-fun c () T)
(declare-fun in () M)
(declare-fun rdv () T)
(declare-fun ivp () T)
(declare-fun ex () T)
(declare-fun cdv () T)
(assert (forall ((z T) (y T)) (! (or (= z y) (not (eq z y))) :qid Q1)))
(assert (forall ((?x0 V) (?x1 Int) (?x2 T)) (! (= ?x2 (s (sto ?x0 ?x1 ?x2) ?x1)) :qid Q2)))
(declare-fun k1 () Bool)
(declare-fun k2 () Bool)
(assert (and
(is-Vec ex)
(not
(and
(not (= ex E))
(or
(not (= rdv (b false)))
(not (= ivp (Vec (Var (sto (R (vec cdv)) (|l#Var| (vec cdv)) c) 0))))
(not (= rdv (b k1)))
(not (B (b k2))))))))
(assert (= k1 (not (forall ((j Int)) (! (not (eq c (s (R (vec ivp)) j))) :qid Q3)))))
(assert (= k2 (not (forall (($i_0 Int)) (! (not (B (b (eq c (s (R (vec (s (R (vec (s (R (vec (sel (cm in) (t (mc err) 1) (add (A 0))))) 0))) 0))) $i_0))))) :qid Q4)))))
(check-sat)
|
