[klee-dev] a question about kleaver

[Dan Liew]

Hi,

On 8 January 2016 at 10:18, xiaoqixue_1 <xiaoqixue_1 at 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.