blob: 846339f5244b2b9d5762760f0466a015f09f9ca4 (
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: unsat
(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 (not (= (f (g (h (i t2)))) (f (h (i t2))))))
(assert (= t1 t2))
(assert (= s1 (h (i t2))))
(check-sat)
(exit)
|
