[klee-dev] Coreutils: STP division by zero errors and computeValue assertion failures

[Hristina Palikareva]

Hi all,

There is functionality in STP to make division by 0 total and I have
used it to avoid crashes. The code is in make_division_total() -- it
defines x / 0 = 1 and x % 0 = x.

Best regards,
Hristina



> On 8 October 2014 11:02, Cadar, Cristian <c.cadar at imperial.ac.uk> wrote:
>> Hi Emil,
>>
>> What version of STP did you use for these experiments?
>> If r940, I would try a more recent version of STP.  In fact, we would
>> like to start recommending a more recent version, but we'd like to have
>> more experience with this first.
>>
>> The usual cause of this problem is the stack size, but you say you've
>> already double-checked that.  To debug this further, I would suggest to
>> log the STP queries, reproduce the problem outside KLEE and then report
>> it to the STP developers.
> 
> Just to note there is a known issue with division by zero in STP
> 
> https://github.com/stp/stp/issues/106
> 
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>