Dear sir, As suggested, I checked the ExprSMTLIBPrinter.cpp and SpecialFunctionHandler.cpp. Now I am able to print the constraints in SMTLIB2 format along with symbolic expression in the klee_print_expr by adding the following lines.
ExprSMTLIBPrinter printer; printer.setOutput(llvm::errs()); Query query(state.constraints, ConstantExpr::alloc(0, Expr::Bool)); printer.setQuery(query); printer.generateOutput(); However, I am not able to find out a way to print the symbolic expression of a given variable in SMTLIB2 format. May I get some more suggestions regarding this? Thanking You, Ramanuj Choukey, Research Scholar, CSE, IIT Guwahati, India. On Fri, Jul 26, 2019 at 3:04 AM Cadar, Cristian <[email protected]> wrote: > > No, but you should be able to accomplish this easily, by changing the > code in handlePrintExpr() to use the code for printing expressions in > the SMT-LIBv2 format (ExprSMTLIBPrinter). > > Best, > Cristian > > On 25/07/2019 12:43, Ramanuj Chouksey wrote: > > Hi, > > How do I convert the symbolic expression printed by klee_print_expr > > into SMTLIB2 format? Is it possible using kleaver? > > > > Thanking you, > > Ramanuj, > > Research Scholar, > > CSE, IIT Guwahati, > > India. > > > > _______________________________________________ > > klee-dev mailing list > > [email protected] > > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev > > > _______________________________________________ > klee-dev mailing list > [email protected] > https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
