blob: e9478da6c8c26b96f46124e469bd347faeca507d (
plain) (
blame)
1
2
3
4
5
6
7
|
;SMTLIBv2 Query 0
(set-logic QF_AUFBV )
(declare-fun shift () (Array (_ BitVec 32) (_ BitVec 8) ) )
(declare-fun value () (Array (_ BitVec 32) (_ BitVec 8) ) )
(assert (and (= false (= (_ bv0 8) (ite (bvuge (select shift (_ bv0 32) ) (_ bv8 8) ) (_ bv0 8) (bvashr (select value (_ bv0 32) ) (select shift (_ bv0 32) ) ) ) ) ) (bvule (_ bv8 8) (select shift (_ bv0 32) ) ) ) )
(check-sat)
(exit)
|
