blob: 8eae3d0734f7eee27a2cb8a46763691f64d6a9b8 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
|
; COMMAND-LINE: --uf-ho
; EXPECT: sat
(set-logic ALL)
(declare-fun g (Int) Real)
(declare-fun h (Int) Real)
(assert (not (= g h)))
; g will be given a model value of lambda x. 0.0, which is interpreted as
; a function Int -> Int; however since function types T -> U are subtypes of
; T -> U' where U is a subtype of U', this example works.
(assert (= (g 0) 0.0))
(assert (= (h 0) 0.5))
(check-sat)
|