[klee-dev] Named Annotations in SMT-LIB2 expressions

[Srijan R Shetty]

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.
-------------- next part --------------
HTML attachment scrubbed and removed