Hi, I'm an undergraduate student at the Indian Institute of Technology Kanpur, India. I'm currently working on a project which requires the output of the path constraint generated by klee in SMT-LIBv2 format with named annotations (We want to use a different SMT solver).
While '--smtlib-abbreviation-mode=named' had the desired effect, I also wanted the mapping of expressions to emitted annotations which I believe can be obtained from BindingMap in lib/Expr/ExprSMTLIBPrinter.cpp. Could someone shed more light on the same/ correct me if I'm wrong and give me a few pointers about how the bindings work. I'll be obliged by any help in this regard. Sincerely, Srijan R. Shetty.
_______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
