[klee-dev] how to add label to assert statements

[Sumit Kumar]

Hi,
I forgot to add this earlier and I think that this is important in this
context: I am running klee with following setting: -solver-backend=z3. I
apologize for missing this information.

--
Thanks and Regards,
Sumit

On 25 April 2016 at 19:39, Thuan Pham <thuanpv at comp.nus.edu.sg> wrote:

> Hi,
> You can update methods in ExprSMTLIBPrinter class like printConstraints
> and printQuery to modify "assert" statements and add "named" at the end of
> the assert. Following is the example code for printConstraints
> void ExprSMTLIBPrinter::printConstraints()
> {
> if(humanReadable)
> *o << "; Constraints" << endl;
>
> //Generate assert statements for each constraint
> for(ConstraintManager::const_iterator i= query->constraints.begin(); i !=
> query->constraints.end(); i++)
> {
> // modified by rubinovk
> *p << "(assert (!";
> //*p << "(assert ";
> p->pushIndent();
> printSeperator();
>
> //recurse into Expression
> printExpression(*i,SORT_BOOL);
>
> p->popIndent();
> printSeperator();
> //added by rubinovk
> *p << ":named a" << getAssertNum() << ")";
> *p << " )";
> //*p << ")";
> p->breakLineI();
> }
> }
>
> The function getAssertNum() gets the next identifier for the label. So
> using this function, you can generate query in which assert statements have
> labels like a0, a1, a2 and so on. By feeding such query into Z3, you will
> get your expected unsat core if the formula is unsatisfiable.
> Hope it helps,
> Thuan
>
> On Mon, Apr 25, 2016 at 9:44 PM, Sumit Kumar <sumit686215 at gmail.com>
> wrote:
>
>> Hi,
>>
>> Can anyone please tell me how to add label to each of the assert
>> statements in the smt2lib formula emitted by KLEE when getConstraintLog
>> method in Executor.cpp is called with logFormat=STP ?  Even if anyone has a
>> faint idea of how it can be done please tell.
>>
>> P.S:This will help me to get an unsat core when I feed the constraint log
>> to z3 solver.
>>
>> --
>> Thanks and Regards,
>> Sumit
>>
>> _______________________________________________
>> klee-dev mailing list
>> klee-dev at imperial.ac.uk
>> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
>>
>>
>
-------------- next part --------------
HTML attachment scrubbed and removed