test/Solver/FastCexSolver.pc


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))