[klee-dev] Timed-out solver queries

Hooman homyhost at gmail.com
Tue Apr 14 15:18:59 BST 2020


*******************
This email originates from outside Imperial. Do not click on links and attachments unless you recognise the sender. 
If you trust the sender, add them to your safe senders list https://spam.ic.ac.uk/SpamConsole/Senders.aspx to disable email stamping for this address.
*******************
Dear Professor Cadar,

As you rightfully mentioned I am not sure that any of the queries 
time-out. However, I am also not sure if I should use all 
-use-query-log=solver:smt2 -min-query-time-to-log=20 
--max-solver-time=20 options or klee will report timed-out queries 
itself by default. (as -log-timed-out-queries option is true by 
default). I also appreciate to have a response for my second question.


Kind regards,

Hooman

On 2020-04-14 15:12, Cristian Cadar wrote:
> Hi Hooman,
>
> How do you know it is not working?  Are you sure there are queries 
> that time out?
>
> Best,
> Cristian
>
> On 14/04/2020 08:39, Hooman wrote:
>> Dear all,
>>
>> I have two questions and I will appreciate any help.
>>
>> 1- I am wondering how is it possible to find out the percentage of 
>> timed-out queries out of all queries sent to solver? I am aware of 
>> the -log-timed-out-queries option. but apparently it is not working. 
>> because it is by default enabled but in a long klee execution (2 
>> days) I don't see any logged timed-out queries. I also don't know 
>> where to look for it :) Moreover, I tried to combine 
>> -use-query-log=solver:smt2 -min-query-time-to-log=20 
>> --max-solver-time=20 options together to kind of trying to log 
>> queries which took more than 20 seconds but solver-queries.smt2 file 
>> is empty after a long run.
>>
>>
>> 2- How is it possible to associate a timed-out query with certain 
>> part of the code. So to understand what parts klee was not able to 
>> cover.
>>
>>
>> Thank you very much.
>>
>> Kind regards,
>>
>> Hooman
>>
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>
> _______________________________________________
> klee-dev mailing list
> klee-dev at imperial.ac.uk
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev



More information about the klee-dev mailing list