Hristina, I tried your suggestion today and added a
make_division_total(vc); call to the STPSolverImpl constructor in
lib/Solver/Solver.cpp (line 557).
I already did 3 (the 4th is running) 30 min runs on the ginstall tool
and, as expected, I haven't seen the div zero error so far. I want to do
further tests, because they are not deterministic in this regard. I also
want to test if this has any effect on the other error I encountered.
What side-effects does this workaround have on KLEE (if any)?
Thank you!
Best regards,
Emil
On 10/8/2014 8:39 PM, Hristina Palikareva wrote:
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 <[email protected]> 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
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
.
_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
