Hi Burak, Thanks for your hints. You are right. My case just hit the "unhandled Expr type" assertion. It looks like Kleaver does not directly handle the "Ugt" expression. The problem is solved by converting Ugt to the equivalent Ult expressions.
Regards, -Jeff On Wed, Jul 11, 2012 at 8:15 PM, Burak Emir <[email protected]> wrote: > Hey, > > This is just a hunch, could it be that 1) you built it without asserts, > and 2) you are running into the "assert(0 && "unhandled Expr type");" > case? > > See bottom of STPBuilder, > https://code.comsys.rwth-aachen.de/redmine/embedded/kleenet-public/STPBuilder_8cpp_source.html > > -- Burak > > > On Thu, Jun 28, 2012 at 6:29 PM, Jeff Huang <[email protected]> wrote: > >> 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 >> >> >
_______________________________________________ klee-dev mailing list [email protected] http://keeda.Stanford.EDU/mailman/listinfo/klee-dev
