Hi Thuan, I thank you for your help. I am very grateful to you for your quick response. However, I am afraid that your solution may not work in my case. The getConstraintLog method uses Z3 C/C++ api (inside Z3Solver.cpp file) to get the smt file. I found that small changes (that you mentioned) had to be made in z3/src/ast/ast_smt_pp.cpp file (inside the method "display_smt2") to get the desired smt output.
-- Thanks and Regards, Sumit On 25 April 2016 at 19:39, Thuan Pham <thua...@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 <sumit686...@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@imperial.ac.uk >> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev >> >> >
_______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev