(set-option :verbose true)
(declare-const x1 Real)
(declare-const x2 Real)
(assert (<= 3.0 x1))
(assert (<= x1 3.14))
(assert (<= -7.0 x2))
(assert (<= x2 5.0))
(assert (<= (+ (* 2.0 3.14159265)
               (* -2.0 x1 (arcsin (* (cos 0.797)
                                     (sin (* 3.14159265 (** x1 -1)))
                                  ))))
            (+ -0.591 (* -0.0331 x2) 0.506 1.0)))
(debug graph)
(check-sat)
(get-model)
-------------------------
0 ==> true
1 ==> false
2 ==> x1
3 ==> x2
4 ==> 3.0
5 ==> $4 <= $2
6 ==> assert $5
7 ==> 3.1
8 ==> $2 <= $7
9 ==> assert $8
10 ==> -7.0
11 ==> $10 <= $3
12 ==> assert $11
13 ==> 5.0
14 ==> $3 <= $13
15 ==> assert $14
16 ==> 0.8
17 ==> (cos $16)
18 ==> $2^-1 * 3.1
19 ==> (sin $18)
20 ==> $17 * $19
21 ==> (arcsin $20)
22 ==> $2 * $21
23 ==> $22*-2.0 + 6.3
24 ==> $3*-0.0 + 0.9
25 ==> $23 <= $24
26 ==> assert $25
unsat
2 iterations of propagation
0 decisions
  24 narrowing of a value interval
  29 narrowing of a constraint interval
No model