[Z3] In `getConstraintLog()` use a separate builder from that of the

solver. This is to avoid tampering with the cache of the builder the
solver is using.

1 files changed, 18 insertions, 3 deletions

diff --git a/lib/Solver/Z3Solver.cpp b/lib/Solver/Z3Solver.cpp
index 2b2e63b8..f32860f7 100644
--- a/lib/Solver/Z3Solver.cpp
+++ b/lib/Solver/Z3Solver.cpp
@@ -132,10 +132,18 @@ void Z3Solver::setCoreSolverTimeout(double timeout) {
 
 char *Z3SolverImpl::getConstraintLog(const Query &query) {
   std::vector<Z3ASTHandle> assumptions;
+  // We use a different builder here because we don't want to interfere
+  // with the solver's builder because it may change the solver builder's
+  // cache.
+  // NOTE: The builder does not set `z3LogInteractionFile` to avoid conflicting
+  // with whatever the solver's builder is set to do.
+  Z3Builder temp_builder(/*autoClearConstructCache=*/false,
+                         /*z3LogInteractionFile=*/NULL);
+
   for (std::vector<ref<Expr> >::const_iterator it = query.constraints.begin(),
                                                ie = query.constraints.end();
        it != ie; ++it) {
-    assumptions.push_back(builder->construct(*it));
+    assumptions.push_back(temp_builder.construct(*it));
   }
   ::Z3_ast *assumptionsArray = NULL;
   int numAssumptions = query.constraints.size();
@@ -152,10 +160,11 @@ char *Z3SolverImpl::getConstraintLog(const Query &query) {
   // the negation of the equivalent i.e.
   // ∃ X Constraints(X) ∧ ¬ query(X)
   Z3ASTHandle formula = Z3ASTHandle(
-      Z3_mk_not(builder->ctx, builder->construct(query.expr)), builder->ctx);
+      Z3_mk_not(temp_builder.ctx, temp_builder.construct(query.expr)),
+      temp_builder.ctx);
 
   ::Z3_string result = Z3_benchmark_to_smtlib_string(
-      builder->ctx,
+      temp_builder.ctx,
       /*name=*/"Emited by klee::Z3SolverImpl::getConstraintLog()",
       /*logic=*/"",
       /*status=*/"unknown",
@@ -166,6 +175,12 @@ char *Z3SolverImpl::getConstraintLog(const Query &query) {
 
   if (numAssumptions)
     free(assumptionsArray);
+
+  // We need to trigger a dereference before the `temp_builder` gets destroyed.
+  // We do this indirectly by emptying `assumptions` and assigning to
+  // `formula`.
+  assumptions.clear();
+  formula = Z3ASTHandle(NULL, temp_builder.ctx);
   // Client is responsible for freeing the returned C-string
   return strdup(result);
 }