Hi,
When a use kleaver to solve a query, I found that "Ult" and "Ugt" can not be
used at the same time.
the logic is simple:
if( sn > 5) {
if( sn < 8 ) {
if (sn==0) printf("hello");
}
}
the query is as follows:
====================
array sn[4] : w32 -> w8 = symbolic
(query [(Ult 5
N0:(ReadLSB w8 0 sn))
(Ugt N0 8) ]
(Eq N0 0) [] [ sn ] )
====================
it crashes the kleaver, but when I change the file to :
====================
array sn[4] : w32 -> w8 = symbolic
(query [(Ult 5
N0:(ReadLSB w8 0 sn))
(Ult N0 8) ]
(Eq N0 0) [] [ sn ] )
=========================
it works normal.
could you tell me why ?
What is different between "Ugt" and "Ult", or I have made some mistake when
using kleaver?
Thanks.
Good Luck!
_______________________________________________
klee-dev mailing list
klee-dev@imperial.ac.uk
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
