From 2d49119d2ab112f43b94b5f561771bed4ca126c6 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Wed, 21 Jun 2017 18:55:35 -0700 Subject: [PATCH] add note to Context documentation about scoped uses of contexts #1077 --- src/api/java/Context.java | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/src/api/java/Context.java b/src/api/java/Context.java index db7a08711..2609dbb29 100644 --- a/src/api/java/Context.java +++ b/src/api/java/Context.java @@ -25,6 +25,12 @@ import java.util.Map; /** * The main interaction with Z3 happens via the Context. + * For applications that spawn an unbounded number of contexts, + * the proper use is within a try-with-resources + * scope so that the Context object gets garbage collected in + * a predictable way. Contexts maintain all data-structures + * related to terms and formulas that are created relative + * to them. **/ public class Context implements AutoCloseable { private final long m_ctx;