SMT2 translations naming conventions

[kooshanabedian]

Hi,
well, this one is not really an issue.
I intend to conduct a points-to analysis on C programs. I'm well aware of --pointer-check option of CBMC and I use it to deliver required assertions. The key point here is that I don't really rely on CBMC to verify some subjected property or refute some assertions and generating just one counterexample. Rather, I take in the translated SMT2 file to parse it manually, restore and correlate some of extra structural and relational information about those same variables through different SSA frames, unwinding loops, and/or thread indices. This is all carried out through some manual processes using an SMT solver API. The final goal is to generate multiple or all counterexamples instead of just one, if it does serve as any justification to our approach.

Yet the problem is that, unlike to other SMT transformations performed by CBMC, I can't really wrap my head around the inner-workings of the relation between an SMT2 statement corresponding to an object and the SMT2 statements corresponding to its pointer counter-part.

For instance, here we have a pointer c which points to a two byte-width object, denoted here by __CPROVER_memory macros. The memory associates store some values and it moves on to the end of the file, but there is no connection or back-reference to the actual pointer statement as far as I can see.
How should I introduce such a connection to my external solver API, so that it preserves such correspondence?

(declare-fun |ss2n::c!0@1#1| () (_ BitVec 64))
(assert (= |ss2n::c!0@1#1| ((_ sign_extend 32) (_ bv8 32))))


(declare-fun |__CPROVER_memory#2| () (Array (_ BitVec 64) (_ BitVec 8)))
(assert (= |__CPROVER_memory#2| (store |__CPROVER_memory#1| (_ bv8 64) (_ bv0 8))))


(declare-fun |__CPROVER_memory#3| () (Array (_ BitVec 64) (_ BitVec 8)))
(assert (= |__CPROVER_memory#3| (store |__CPROVER_memory#2| (_ bv9 64) (_ bv18 8))))

I wonder if there is any documented instructions about the naming conventions of SMT2 conversion module of CBMC, so that I could conveniently make a correspondence between pointers and their associated objects.

[thomasspriggs]

The documentation for our SMT support is unfortunately somewhat limited. We also aren't currently planning changes to the SMT output to support consumption of the output by any tool other than an SMT solver. I would be concerned that introducing such features would make it more difficult to debug and otherwise improve the support for SMT solvers without breaking compatibility with your tool. I hope you did manage to achieve what you wanted to with cbmc and my regrets that it took 4 years before anyone took the time to reply to you.