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

[Thuan Pham]

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