blob: 92c4dabba0c33ddd0a49c24d0c46861e5d3dd763 (
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
38
39
40
|
; COMMAND-LINE: -q
; EXPECT: sat
; EXPECT: sat
; EXPECT: unsat
; EXPECT: sat
; EXPECT: unsat
(set-option :incremental true)
(set-logic ALL)
(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)
(push)
(assert (= (sqrt 1.0) 1.0))
(check-sat)
(pop)
(push)
(assert (= (sqrt 1.0) (- 1.0)))
(check-sat)
(pop)
(push)
(assert (= x 1.0))
(assert (not (= (sqrt 1.0) (sqrt x))))
(check-sat)
(pop)
(push)
(assert (< x 0))
(assert (= (sqrt 1.0) (sqrt x)))
(check-sat)
(pop)
(push)
(assert (= (sqrt y) z))
(assert (= (sqrt x) (sqrt y)))
(assert (not (= (sqrt x) z)))
(check-sat)
(pop)
|
