# RUN: not %kleaver %s 2> %t.log



# RUN: grep "TypeChecking.kquery:7:9: error: type widths do not match in binary expression" %t.log
array arr1[8] : w32 -> w8 = symbolic
(query [(Eq (ReadLSB w32 0 arr1) true)]
       false)

# RUN: grep "TypeChecking.kquery:14:25: error: invalid write index (doesn't match array domain)" %t.log
# RUN: grep "TypeChecking.kquery:14:35: error: invalid write value (doesn't match array range)" %t.log
# FIXME: Add array declarations
array arr2[8] : w32 -> w8 = symbolic
(query [(Eq (Read w8 0 [ (w17 0) = (w9 0) ] @ arr2) 0)] false)

# RUN: grep "TypeChecking.kquery: parse failure: 3 errors." %t.log