about summary refs log tree commit diff homepage
path: root/test/Solver/FastCexSolver.kquery
blob: b3ec63e3c8c5952e57b2e261d13f4e983e60edf0 (plain) (blame)
1
2
3
4
5
6
7
8
9
10
# RUN: %kleaver --use-fast-cex-solver --solver-backend=dummy %s > %t
# RUN: not grep FAIL %t

array arr1[4] : w32 -> w8 = symbolic
(query [] (Not (Eq 4096 (ReadLSB w32 0 arr1))))

array A-data[2] : w32 -> w8 = symbolic
(query [(Ule (Add w8 208 N0:(Read w8 0 A-data))
             9)]
       (Eq 52 N0))