blob: 8989acdc406e54a94b2b5e7c9f7ba42f82630c19 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
|
(set-logic HO_ALL)
(set-info :status sat)
(declare-fun a ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
(declare-fun b () (_ BitVec 32))
(declare-fun c () (_ BitVec 1))
(declare-fun d () (_ BitVec 32))
(declare-fun e () (_ BitVec 32))
(declare-fun f () (_ BitVec 32))
(declare-fun g ((_ BitVec 32) (_ BitVec 32)) (_ BitVec 32))
(declare-fun h () (_ BitVec 32))
(declare-fun i () (_ BitVec 32))
(declare-fun j () (_ BitVec 1))
(declare-fun k () (_ BitVec 32))
(assert (= b (a d e)))
(assert (= f (g h i)))
(assert (distinct j (ite (= i k) (_ bv1 1) (_ bv0 1))))
(assert (= (ite (= i b) (_ bv1 1) (_ bv0 1)) j (ite (= c (_ bv0 1)) (_ bv1 1) (_ bv0 1))))
(check-sat)
|
