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