blob: d29311109c489209e30f4c52e1b3fb73d0b16e98 (
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
|
; COMMAND-LINE: --ackermann --no-check-models --no-check-proofs --no-check-unsat-cores
; EXPECT: sat
(set-logic QF_UFBV)
(declare-sort S 0)
(declare-sort T 0)
(declare-fun s1 () S)
(declare-fun s2 () S)
(declare-fun t1 () T)
(declare-fun t2 () T)
(declare-fun a () (_ BitVec 4))
(declare-fun b () (_ BitVec 4))
(declare-fun f (S) (_ BitVec 4))
(declare-fun g (S) S)
(declare-fun h (T) S)
(declare-fun i (T) T)
(assert (= (f s1) (bvand a b)))
(assert (= (f s2) (bvand a b)))
(assert (= (f (g s1)) (f (h (i t1)))))
(assert (= (f (g (h (i t2)))) (f (h (i t2)))))
(assert (= t1 t2))
(assert (= s1 (h (i t2))))
(check-sat)
(exit)
|