[klee-dev] how to add label to assert statements

[Dan Liew]

Hi,

On 28 April 2016 at 20:57, Sumit Kumar <sumit686215 at gmail.com> wrote:
> Hi,
> I forgot to add this earlier and I think that this is important in this
> context: I am running klee with following setting: -solver-backend=z3. I
> apologize for missing this information.

Yes your previous e-mails were misleading because you said
"getConstraintLog method in Executor.cpp is called with
logFormat=STP". It's cool that you're using the Z3 support I recently
introduced but I am very bemused by how you are using it.

* If your aim is to get to constraints in the SMT-LIBv2 format then
why are you using ``getConstraintLog()`` which will use the core
solver's natural constraint language (for Z3 this happens to be
SMT-LIBv2 but you don't have fine the grained control you need)?
Instead you should do what Thuan is suggesting and modify the
ExprSMTLIBPrinter to add labels if that is your goal.

* If you are already using Z3 as the solver backend why don't you use
its C API to get the unsat core?

Dan.