blob: a253cf12f301a33984d0332a69bc2fb5dea0eccc (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(set-logic QF_ALL_SUPPORTED)
(declare-fun _substvar_245_ () Bool)
(declare-fun _substvar_246_ () Bool)
(declare-fun _substvar_247_ () Bool)
(declare-fun group_size_x () (_ BitVec 32))
(declare-fun group_id_x$2 () (_ BitVec 32))
(declare-fun local_id_x$2 () (_ BitVec 32))
(assert (= _substvar_245_ _substvar_246_))
(assert
(and (bvsge group_id_x$2 #x00000000) (bvsge local_id_x$2 #x00000000) (bvslt local_id_x$2 group_size_x)
(or (not (bvsgt group_size_x #x00000000)) (not (and (=> _substvar_247_ (bvsge group_id_x$2 #x00000000)) (= _substvar_245_ _substvar_246_))))
)
)
(check-sat)
|