blob: 354b0489d590e6afacc74d6eb540c2806062442b (
plain) (
blame)
1
2
3
4
5
6
7
8
9
10
11
12
13
|
# RUN: %kleaver -evaluate %s > %t.log
# RUN: grep "Query 0: INVALID" %t.log
# Query 0
(query [] (Not (Ult (ReadLSB w32 0 arr65)
16)))
# RUN: grep "Query 1: VALID" %t.log
# Query 1
(query [(Eq N0:(ReadLSB w32 0 arr1) 10)
(Eq N1:(ReadLSB w32 4 arr1) 20)]
(Eq (Add w32 N0 N1)
30))
|