blob: b245228be06f14f3679812c68b5a8e5e0341173c (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(set-logic QF_AUFBV)
(declare-sort U 0)
(declare-sort Index 0)
(declare-sort Element 0)
(declare-fun memory_0 () (Array (_ BitVec 32) (_ BitVec 8)))
(set-info :status sat)
(set-info :notes "RewriteRule <ExtractBitwise>; expect unsat")
(assert (not (= ((_ extract 7 0) (bvor (_ bv65536 32) (concat (_ bv0 25) ((_ extract 7 1) (select memory_0 (_ bv1 32)))) (concat (_ bv0 24) (select memory_0 (_ bv1 32))))) (bvor ((_ extract 7 0) (_ bv65536 32)) ((_ extract 7 0) (concat (_ bv0 25) ((_ extract 7 1) (select memory_0 (_ bv1 32)))))))))
(check-sat)
(exit)
|
