1# RUN: %kleaver %s > %t
2# RUN: not grep INVALID %t
3
4array shift[4] : w32 -> w8 = symbolic
5# ∀ x. x >= 32 → ( ( ( (signed int)2 ) >> x) = 0 )
6# Check we arithmetic right overshift to zero when shifting a constant ALWAYS!
7
8(query [ (Ule  (w32 32) (ReadLSB w32 (w32 0) shift)) ]
9    (Eq
10        (AShr w32 (w32 2)
11            (ReadLSB w32 (w32 0) shift)
12        )
13        (w32 0)
14    ) [ ] [shift] )
15
16# 64-bit version
17# ∀ x. x >= 64 → ( (((signed int) 2) >> x) = 0 )
18array shift64[8] : w32 -> w8 = symbolic
19
20(query [ (Ule  (w64 64) (ReadLSB w64 (w32 0) shift64)) ]
21    (Eq
22        (AShr w64 (w64 2)
23            (ReadLSB w64 (w32 0) shift64)
24        )
25        (w64 0)
26    ) [ ] [shift64] )
27