>> 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. _______________________________________________ klee-dev mailing list klee-dev@imperial.ac.uk https://mailman.ic.ac.uk/mailman/listinfo/klee-dev
