Hi Bowen,

The way to do that is the following:
- at the beginning of the file you will find a list of arrays
- from the list, you choose the name of the array that you are interested in
- .pc file probably ends with "false)" 
        - the way to get the value of the selected array is to modify "false)" 
into "false [] [array_name])"
        (where you put the name of the selected array in square brackets); so 
you have two pairs of 
        square brackets - the first pair is empty and in the second one you put 
the name of the array.

Hope that helps,
Best regards,
Tomek


On 11 Oct 2013, at 04:00, Bowen Zhou <[email protected]> wrote:

> Hello,
> 
> I tried to use Kleaver to solve a .pc file generated by Klee with option 
> '-write-pcs'. The command I used is 'kleaver input.pc'. Kleaver always gives 
> 'Query 0:        INVALID' as its output.
> 
> How can I get Kleaver to output a test input that satisfy the constraints in 
> the input .pc file? Is it possible?
> 
> Cheers,
> Bowen
> 
> _______________________________________________
> klee-dev mailing list
> [email protected]
> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

<<attachment: winmail.dat>>

_______________________________________________
klee-dev mailing list
[email protected]
https://mailman.ic.ac.uk/mailman/listinfo/klee-dev

Reply via email to