blob: 6284b058004162c466e4299e2e67d8cc13371586 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
|
(set-logic QF_AUFNRA)
(set-info :status sat)
(declare-fun r2 () Real)
(declare-fun r9 () Real)
(declare-fun r13 () Real)
(declare-fun ufrb5 (Real Real Real Real Real) Bool)
(declare-fun v3 () Bool)
(declare-fun v4 () Bool)
(declare-fun arr0 () (Array Bool Real))
(declare-fun arr1 () (Array Bool (Array Bool Real)))
(declare-fun v5 () Bool)
(declare-fun v7 () Bool)
(declare-fun v8 () Bool)
(declare-fun v71 () Bool)
(declare-fun v81 () Bool)
(declare-fun v161 () Bool)
(assert (or v161 (and v3 (not v7))))
(assert (or v8 (distinct v7 (and v7 v81) (ufrb5 0.0 1.0 0.0 1.0 (/ r13 r9)))))
(assert (or v161 (distinct v71 v8 (= v4 v81))))
(assert (or v81 (= arr0 (store (select (store arr1 (xor v81 (and (= r2 1.0) (= r13 1))) arr0) v7) v81 (select (store arr0 v5 1.0) false)))))
(check-sat)
|
