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

[Dan Liew]

>> 3. We need to control Z3's memory management for Z3_ast and Z3_sort
>> nodes manually. IIRC the C++ API doesn't let you do this.
>
>
> I could not understand the 3rd point. Can you please explain it a little
> more. It would help me understand the working of KLEE better.

The Z3Builder caches declared Arrays and Updates to be across multiple
solver queries. Therefore we can't use Z3's automatic memory
management because that clears expressions when they are popped from
the solver assertion stack.

See

Z3Builder::getInitialArray(..)

and

Z3Builder::getArrayForUpdate(..)

So instead we do our own memory management by using
``Z3_mk_context_rc(..)`` and using the Z3ASTHandle and Z3SortHandle
helper classes to automate most of the increment/decrement of
references.