Hi, On 8 January 2016 at 10:18, xiaoqixue_1 <xiaoqixu...@163.com> wrote: > > > 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 :
The crash is due to Ult not being supported by the STPBuilder. In KLEE a Ult expression shouldn't ever occur due to expression canonicalisation rules used internally inside KLEE. The assertion failure you hit is Query 0: kleaver: /home/dan/dev/klee/src/lib/Solver/STPBuilder.cpp:903: klee::ExprHandle klee::STPBuilder::constructActual(klee::ref<klee::Expr>, int*): Assertion `0 && "unhandled Expr type"' failed. Take a look at ``include/klee/Expr.h`` to get an explanation of why these rules exists. If you pass `` --builder=simplify`` to kleaver the expression builder should try to canonicalise the expressions for you and avoid the crash. Hope that helps. Dan. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev