blob: 5fbddf13d15f56134877919ee3a40d59262b7a9f (
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 QF_UFNRA)
(set-option :nl-ext-purify true)
(set-option :sygus-inference true)
(set-info :status unsat)
(declare-const v0 Bool)
(declare-const v1 Bool)
(declare-const v2 Bool)
(declare-const v3 Bool)
(declare-const v4 Bool)
(declare-const v5 Bool)
(declare-const v6 Bool)
(declare-const v7 Bool)
(declare-const v8 Bool)
(declare-const v9 Bool)
(declare-const r3 Real)
(declare-const r5 Real)
(assert v8)
(declare-const v10 Bool)
(assert (= 169 r5))
(declare-const v11 Bool)
(assert v5)
(declare-const v12 Bool)
(declare-const r7 Real)
(assert (not v1))
(assert v10)
(declare-const v13 Bool)
(declare-const r8 Real)
(assert (not (distinct r7 (- (/ 0.816577 (+ r5 569703))) 0.0 r3)))
(assert v4)
(assert (and (distinct v3 v4 (= 169 r5) (= (+ r5 569703) (/ 0.816577 (+ r5 569703)) 0.816577 0.26205) v11 v7 (= 169 r5)) (> 0.816577 169 569703 0.26205) (distinct r7 (- (/ 0.816577 (+ r5 569703))) 0.0 r3) v3 (= (+ r5 569703) (/ 0.816577 (+ r5 569703)) 0.816577 0.26205) v5 v10))
(declare-const v14 Bool)
(assert (or (= (+ r5 569703) (/ 0.816577 (+ r5 569703)) 0.816577 0.26205) v6 (or (<= 0.26205 r7 353 569703) v7 v8 v13 v3) v5 v6 (distinct r7 (- (/ 0.816577 (+ r5 569703))) 0.0 r3)))
(declare-const v15 Bool)
(assert (xor v3 v11 v9 v3))
(declare-const v16 Bool)
(assert (xor v2 v8))
(check-sat)
|
