about summary refs log tree commit diff homepage
path: root/lib/Solver/Solver.cpp
diff options
context:
space:
mode:
Diffstat (limited to 'lib/Solver/Solver.cpp')
-rw-r--r--lib/Solver/Solver.cpp9
1 files changed, 9 insertions, 0 deletions
diff --git a/lib/Solver/Solver.cpp b/lib/Solver/Solver.cpp
index 1d13a11d..4059a82b 100644
--- a/lib/Solver/Solver.cpp
+++ b/lib/Solver/Solver.cpp
@@ -453,6 +453,15 @@ STPSolverImpl::STPSolverImpl(STPSolver *_solver, bool _useForkedSTP, bool _optim
   assert(vc && "unable to create validity checker");
   assert(builder && "unable to create STPBuilder");
 
+#ifdef HAVE_EXT_STP
+  // In newer versions of STP, a memory management mechanism has been
+  // introduced that automatically invalidates certain C interface
+  // pointers at vc_Destroy time.  This caused double-free errors
+  // due to the ExprHandle destructor also attempting to invalidate
+  // the pointers using vc_DeleteExpr.  By setting EXPRDELETE to 0
+  // we restore the old behaviour.
+  vc_setInterfaceFlags(vc, EXPRDELETE, 0);
+#endif
   vc_registerErrorHandler(::stp_error_handler);
 
   if (useForkedSTP) {