Hi everyone, I am doing a small experiment with kleaver and got a problem. Basically I want to use Kleaver to solve the following simple constraints over two variables:
0<x1<3 0<x2<3 x1<x2 and x1,x2 are numbers Following is the KQuery input: array x[2] : w32 -> w8 = symbolic (query [ (Ugt N0:(ReadLSB w8 0 x) 0) (Ult N0 3) (Ugt N1:(ReadLSB w8 1 x) 0) (Ult N1 3) (Ult N0 N1) ] false [] [ x ]) The expected result should be x[1,2], but Kleaver returns x[0, 1]. Any hint on where I'm doing wrong? I am working with klee trunk and llvm 2.9. Jeff
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
