Hi, On 28 April 2016 at 20:57, Sumit Kumar <[email protected]> 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. _______________________________________________ klee-dev mailing list [email protected] https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
