Hi, Currently, only queries can be printed. Extend your code to create an empty constraint set and use the expression (arguments[0]) as an argument:
``` std::vector<ref<Expr>> emptyCS; ConstraintManager emptyCM(emptyCS); Query query(emptyCM, arguments[0]); ``` Hope that helps. Cheers, Martin On 27. Jul 2019, at 13:19, Ramanuj Chouksey <[email protected]<mailto:[email protected]>> wrote: 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]<mailto:[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]<mailto:[email protected]> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected]<mailto:[email protected]> https://mailman.ic.ac.uk/mailman/listinfo/klee-dev _______________________________________________ klee-dev mailing list [email protected]<mailto:[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
