Enable CI for Junit tests (#7436)

This PR enables CI for java tests by adding --java-bindings to ci.yml.
It also replaces the unreliable finalize method and instead uses AutoCloseable and explicit close method to clean up dynamic memory allocated by java native interface.
The PR fixes compile errors for SolverTest.java and runtime errors for Solver.defineFun.

57 files changed, 1268 insertions, 1189 deletions

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 1acc26c5a..fedcb9bb4 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -38,7 +38,7 @@ jobs:
 
           - name: ubuntu:production-dbg
             os: ubuntu-18.04
-            config: production --auto-download --assertions --tracing --unit-testing --editline
+            config: production --auto-download --assertions --tracing --unit-testing --java-bindings --editline
             cache-key: dbg
             check-units: true
             exclude_regress: 3-4
diff --git a/examples/api/java/BitVectors.java b/examples/api/java/BitVectors.java
index 6209cf9dd..4d1d9e169 100644
--- a/examples/api/java/BitVectors.java
+++ b/examples/api/java/BitVectors.java
@@ -22,104 +22,106 @@ public class BitVectors
 {
   public static void main(String args[]) throws CVC5ApiException
   {
-    Solver slv = new Solver();
-    slv.setLogic("QF_BV"); // Set the logic
-
-    // The following example has been adapted from the book A Hacker's Delight by
-    // Henry S. Warren.
-    //
-    // Given a variable x that can only have two values, a or b. We want to
-    // assign to x a value other than the current one. The straightforward code
-    // to do that is:
-    //
-    //(0) if (x == a ) x = b;
-    //    else x = a;
-    //
-    // Two more efficient yet equivalent methods are:
-    //
-    //(1) x = a ⊕ b ⊕ x;
-    //
-    //(2) x = a + b - x;
-    //
-    // We will use cvc5 to prove that the three pieces of code above are all
-    // equivalent by encoding the problem in the bit-vector theory.
-
-    // Creating a bit-vector type of width 32
-    Sort bitvector32 = slv.mkBitVectorSort(32);
-
-    // Variables
-    Term x = slv.mkConst(bitvector32, "x");
-    Term a = slv.mkConst(bitvector32, "a");
-    Term b = slv.mkConst(bitvector32, "b");
-
-    // First encode the assumption that x must be Kind.EQUAL to a or b
-    Term x_eq_a = slv.mkTerm(Kind.EQUAL, x, a);
-    Term x_eq_b = slv.mkTerm(Kind.EQUAL, x, b);
-    Term assumption = slv.mkTerm(Kind.OR, x_eq_a, x_eq_b);
-
-    // Assert the assumption
-    slv.assertFormula(assumption);
-
-    // Introduce a new variable for the new value of x after assignment.
-    Term new_x = slv.mkConst(bitvector32, "new_x"); // x after executing code (0)
-    Term new_x_ = slv.mkConst(bitvector32, "new_x_"); // x after executing code (1) or (2)
-
-    // Encoding code (0)
-    // new_x = x == a ? b : a;
-    Term ite = slv.mkTerm(Kind.ITE, x_eq_a, b, a);
-    Term assignment0 = slv.mkTerm(Kind.EQUAL, new_x, ite);
-
-    // Assert the encoding of code (0)
-    System.out.println("Asserting " + assignment0 + " to cvc5 ");
-    slv.assertFormula(assignment0);
-    System.out.println("Pushing a new context.");
-    slv.push();
-
-    // Encoding code (1)
-    // new_x_ = a xor b xor x
-    Term a_xor_b_xor_x = slv.mkTerm(Kind.BITVECTOR_XOR, a, b, x);
-    Term assignment1 = slv.mkTerm(Kind.EQUAL, new_x_, a_xor_b_xor_x);
-
-    // Assert encoding to cvc5 in current context;
-    System.out.println("Asserting " + assignment1 + " to cvc5 ");
-    slv.assertFormula(assignment1);
-    Term new_x_eq_new_x_ = slv.mkTerm(Kind.EQUAL, new_x, new_x_);
-
-    System.out.println(" Check entailment assuming: " + new_x_eq_new_x_);
-    System.out.println(" Expect ENTAILED. ");
-    System.out.println(" cvc5: " + slv.checkEntailed(new_x_eq_new_x_));
-    System.out.println(" Popping context. ");
-    slv.pop();
-
-    // Encoding code (2)
-    // new_x_ = a + b - x
-    Term a_plus_b = slv.mkTerm(Kind.BITVECTOR_ADD, a, b);
-    Term a_plus_b_minus_x = slv.mkTerm(Kind.BITVECTOR_SUB, a_plus_b, x);
-    Term assignment2 = slv.mkTerm(Kind.EQUAL, new_x_, a_plus_b_minus_x);
-
-    // Assert encoding to cvc5 in current context;
-    System.out.println("Asserting " + assignment2 + " to cvc5 ");
-    slv.assertFormula(assignment2);
-
-    System.out.println(" Check entailment assuming: " + new_x_eq_new_x_);
-    System.out.println(" Expect ENTAILED. ");
-    System.out.println(" cvc5: " + slv.checkEntailed(new_x_eq_new_x_));
-
-    Term x_neq_x = slv.mkTerm(Kind.EQUAL, x, x).notTerm();
-    Term[] v = new Term[] {new_x_eq_new_x_, x_neq_x};
-    System.out.println(" Check entailment assuming: " + v);
-    System.out.println(" Expect NOT_ENTAILED. ");
-    System.out.println(" cvc5: " + slv.checkEntailed(v));
-
-    // Assert that a is odd
-    Op extract_op = slv.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0);
-    Term lsb_of_a = slv.mkTerm(extract_op, a);
-    System.out.println("Sort of " + lsb_of_a + " is " + lsb_of_a.getSort());
-    Term a_odd = slv.mkTerm(Kind.EQUAL, lsb_of_a, slv.mkBitVector(1, 1));
-    System.out.println("Assert " + a_odd);
-    System.out.println("Check satisfiability.");
-    slv.assertFormula(a_odd);
-    System.out.println(" Expect sat. ");
-    System.out.println(" cvc5: " + slv.checkSat());
+    try (Solver slv = new Solver())
+    {
+      slv.setLogic("QF_BV"); // Set the logic
+
+      // The following example has been adapted from the book A Hacker's Delight by
+      // Henry S. Warren.
+      //
+      // Given a variable x that can only have two values, a or b. We want to
+      // assign to x a value other than the current one. The straightforward code
+      // to do that is:
+      //
+      //(0) if (x == a ) x = b;
+      //    else x = a;
+      //
+      // Two more efficient yet equivalent methods are:
+      //
+      //(1) x = a ⊕ b ⊕ x;
+      //
+      //(2) x = a + b - x;
+      //
+      // We will use cvc5 to prove that the three pieces of code above are all
+      // equivalent by encoding the problem in the bit-vector theory.
+
+      // Creating a bit-vector type of width 32
+      Sort bitvector32 = slv.mkBitVectorSort(32);
+
+      // Variables
+      Term x = slv.mkConst(bitvector32, "x");
+      Term a = slv.mkConst(bitvector32, "a");
+      Term b = slv.mkConst(bitvector32, "b");
+
+      // First encode the assumption that x must be Kind.EQUAL to a or b
+      Term x_eq_a = slv.mkTerm(Kind.EQUAL, x, a);
+      Term x_eq_b = slv.mkTerm(Kind.EQUAL, x, b);
+      Term assumption = slv.mkTerm(Kind.OR, x_eq_a, x_eq_b);
+
+      // Assert the assumption
+      slv.assertFormula(assumption);
+
+      // Introduce a new variable for the new value of x after assignment.
+      Term new_x = slv.mkConst(bitvector32, "new_x"); // x after executing code (0)
+      Term new_x_ = slv.mkConst(bitvector32, "new_x_"); // x after executing code (1) or (2)
+
+      // Encoding code (0)
+      // new_x = x == a ? b : a;
+      Term ite = slv.mkTerm(Kind.ITE, x_eq_a, b, a);
+      Term assignment0 = slv.mkTerm(Kind.EQUAL, new_x, ite);
+
+      // Assert the encoding of code (0)
+      System.out.println("Asserting " + assignment0 + " to cvc5 ");
+      slv.assertFormula(assignment0);
+      System.out.println("Pushing a new context.");
+      slv.push();
+
+      // Encoding code (1)
+      // new_x_ = a xor b xor x
+      Term a_xor_b_xor_x = slv.mkTerm(Kind.BITVECTOR_XOR, a, b, x);
+      Term assignment1 = slv.mkTerm(Kind.EQUAL, new_x_, a_xor_b_xor_x);
+
+      // Assert encoding to cvc5 in current context;
+      System.out.println("Asserting " + assignment1 + " to cvc5 ");
+      slv.assertFormula(assignment1);
+      Term new_x_eq_new_x_ = slv.mkTerm(Kind.EQUAL, new_x, new_x_);
+
+      System.out.println(" Check entailment assuming: " + new_x_eq_new_x_);
+      System.out.println(" Expect ENTAILED. ");
+      System.out.println(" cvc5: " + slv.checkEntailed(new_x_eq_new_x_));
+      System.out.println(" Popping context. ");
+      slv.pop();
+
+      // Encoding code (2)
+      // new_x_ = a + b - x
+      Term a_plus_b = slv.mkTerm(Kind.BITVECTOR_ADD, a, b);
+      Term a_plus_b_minus_x = slv.mkTerm(Kind.BITVECTOR_SUB, a_plus_b, x);
+      Term assignment2 = slv.mkTerm(Kind.EQUAL, new_x_, a_plus_b_minus_x);
+
+      // Assert encoding to cvc5 in current context;
+      System.out.println("Asserting " + assignment2 + " to cvc5 ");
+      slv.assertFormula(assignment2);
+
+      System.out.println(" Check entailment assuming: " + new_x_eq_new_x_);
+      System.out.println(" Expect ENTAILED. ");
+      System.out.println(" cvc5: " + slv.checkEntailed(new_x_eq_new_x_));
+
+      Term x_neq_x = slv.mkTerm(Kind.EQUAL, x, x).notTerm();
+      Term[] v = new Term[] {new_x_eq_new_x_, x_neq_x};
+      System.out.println(" Check entailment assuming: " + v);
+      System.out.println(" Expect NOT_ENTAILED. ");
+      System.out.println(" cvc5: " + slv.checkEntailed(v));
+
+      // Assert that a is odd
+      Op extract_op = slv.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0);
+      Term lsb_of_a = slv.mkTerm(extract_op, a);
+      System.out.println("Sort of " + lsb_of_a + " is " + lsb_of_a.getSort());
+      Term a_odd = slv.mkTerm(Kind.EQUAL, lsb_of_a, slv.mkBitVector(1, 1));
+      System.out.println("Assert " + a_odd);
+      System.out.println("Check satisfiability.");
+      slv.assertFormula(a_odd);
+      System.out.println(" Expect sat. ");
+      System.out.println(" cvc5: " + slv.checkSat());
+    }
   }
-}
\ No newline at end of file
+}
diff --git a/examples/api/java/BitVectorsAndArrays.java b/examples/api/java/BitVectorsAndArrays.java
index 07b9781d2..c72106082 100644
--- a/examples/api/java/BitVectorsAndArrays.java
+++ b/examples/api/java/BitVectorsAndArrays.java
@@ -27,73 +27,75 @@ public class BitVectorsAndArrays
 
   public static void main(String[] args) throws CVC5ApiException
   {
-    Solver slv = new Solver();
-    slv.setOption("produce-models", "true"); // Produce Models
-    slv.setOption("output-language", "smtlib"); // output-language
-    slv.setLogic("QF_AUFBV"); // Set the logic
+    try (Solver slv = new Solver())
+    {
+      slv.setOption("produce-models", "true"); // Produce Models
+      slv.setOption("output-language", "smtlib"); // output-language
+      slv.setLogic("QF_AUFBV"); // Set the logic
 
-    // Consider the following code (where size is some previously defined constant):
-    //
-    //
-    //   Assert (current_array[0] > 0);
-    //   for (unsigned i = 1; i < k; ++i) {
-    //     current_array[i] = 2 * current_array[i - 1];
-    //     Assert (current_array[i-1] < current_array[i]);
-    //     }
-    //
-    // We want to check whether the assertion in the body of the for loop holds
-    // throughout the loop.
+      // Consider the following code (where size is some previously defined constant):
+      //
+      //
+      //   Assert (current_array[0] > 0);
+      //   for (unsigned i = 1; i < k; ++i) {
+      //     current_array[i] = 2 * current_array[i - 1];
+      //     Assert (current_array[i-1] < current_array[i]);
+      //     }
+      //
+      // We want to check whether the assertion in the body of the for loop holds
+      // throughout the loop.
 
-    // Setting up the problem parameters
-    int k = 4; // number of unrollings (should be a power of 2)
-    int index_size = log2(k); // size of the index
+      // Setting up the problem parameters
+      int k = 4; // number of unrollings (should be a power of 2)
+      int index_size = log2(k); // size of the index
 
-    // Sorts
-    Sort elementSort = slv.mkBitVectorSort(32);
-    Sort indexSort = slv.mkBitVectorSort(index_size);
-    Sort arraySort = slv.mkArraySort(indexSort, elementSort);
+      // Sorts
+      Sort elementSort = slv.mkBitVectorSort(32);
+      Sort indexSort = slv.mkBitVectorSort(index_size);
+      Sort arraySort = slv.mkArraySort(indexSort, elementSort);
 
-    // Variables
-    Term current_array = slv.mkConst(arraySort, "current_array");
+      // Variables
+      Term current_array = slv.mkConst(arraySort, "current_array");
 
-    // Making a bit-vector constant
-    Term zero = slv.mkBitVector(index_size, 0);
+      // Making a bit-vector constant
+      Term zero = slv.mkBitVector(index_size, 0);
 
-    // Asserting that current_array[0] > 0
-    Term current_array0 = slv.mkTerm(Kind.SELECT, current_array, zero);
-    Term current_array0_gt_0 =
-        slv.mkTerm(Kind.BITVECTOR_SGT, current_array0, slv.mkBitVector(32, 0));
-    slv.assertFormula(current_array0_gt_0);
+      // Asserting that current_array[0] > 0
+      Term current_array0 = slv.mkTerm(Kind.SELECT, current_array, zero);
+      Term current_array0_gt_0 =
+          slv.mkTerm(Kind.BITVECTOR_SGT, current_array0, slv.mkBitVector(32, 0));
+      slv.assertFormula(current_array0_gt_0);
 
-    // Building the assertions in the loop unrolling
-    Term index = slv.mkBitVector(index_size, 0);
-    Term old_current = slv.mkTerm(Kind.SELECT, current_array, index);
-    Term two = slv.mkBitVector(32, 2);
+      // Building the assertions in the loop unrolling
+      Term index = slv.mkBitVector(index_size, 0);
+      Term old_current = slv.mkTerm(Kind.SELECT, current_array, index);
+      Term two = slv.mkBitVector(32, 2);
 
-    List<Term> assertions = new ArrayList<Term>();
-    for (int i = 1; i < k; ++i)
-    {
-      index = slv.mkBitVector(index_size, i);
-      Term new_current = slv.mkTerm(Kind.BITVECTOR_MULT, two, old_current);
-      // current[i] = 2 * current[i-1]
-      current_array = slv.mkTerm(Kind.STORE, current_array, index, new_current);
-      // current[i-1] < current [i]
-      Term current_slt_new_current = slv.mkTerm(Kind.BITVECTOR_SLT, old_current, new_current);
-      assertions.add(current_slt_new_current);
+      List<Term> assertions = new ArrayList<Term>();
+      for (int i = 1; i < k; ++i)
+      {
+        index = slv.mkBitVector(index_size, i);
+        Term new_current = slv.mkTerm(Kind.BITVECTOR_MULT, two, old_current);
+        // current[i] = 2 * current[i-1]
+        current_array = slv.mkTerm(Kind.STORE, current_array, index, new_current);
+        // current[i-1] < current [i]
+        Term current_slt_new_current = slv.mkTerm(Kind.BITVECTOR_SLT, old_current, new_current);
+        assertions.add(current_slt_new_current);
 
-      old_current = slv.mkTerm(Kind.SELECT, current_array, index);
-    }
+        old_current = slv.mkTerm(Kind.SELECT, current_array, index);
+      }
 
-    Term query = slv.mkTerm(Kind.NOT, slv.mkTerm(Kind.AND, assertions.toArray(new Term[0])));
+      Term query = slv.mkTerm(Kind.NOT, slv.mkTerm(Kind.AND, assertions.toArray(new Term[0])));
 
-    System.out.println("Asserting " + query + " to cvc5 ");
-    slv.assertFormula(query);
-    System.out.println("Expect sat. ");
-    System.out.println("cvc5: " + slv.checkSatAssuming(slv.mkTrue()));
+      System.out.println("Asserting " + query + " to cvc5 ");
+      slv.assertFormula(query);
+      System.out.println("Expect sat. ");
+      System.out.println("cvc5: " + slv.checkSatAssuming(slv.mkTrue()));
 
-    // Getting the model
-    System.out.println("The satisfying model is: ");
-    System.out.println("  current_array = " + slv.getValue(current_array));
-    System.out.println("  current_array[0] = " + slv.getValue(current_array0));
+      // Getting the model
+      System.out.println("The satisfying model is: ");
+      System.out.println("  current_array = " + slv.getValue(current_array));
+      System.out.println("  current_array[0] = " + slv.getValue(current_array0));
+    }
   }
 }
diff --git a/examples/api/java/Combination.java b/examples/api/java/Combination.java
index 66cd30b2b..03c43521a 100644
--- a/examples/api/java/Combination.java
+++ b/examples/api/java/Combination.java
@@ -39,89 +39,91 @@ public class Combination
 
   public static void main(String[] args) throws CVC5ApiException
   {
-    Solver slv = new Solver();
-    slv.setOption("produce-models", "true"); // Produce Models
-    slv.setOption("dag-thresh", "0"); // Disable dagifying the output
-    slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language
-    slv.setLogic("QF_UFLIRA");
-
-    // Sorts
-    Sort u = slv.mkUninterpretedSort("u");
-    Sort integer = slv.getIntegerSort();
-    Sort bool = slv.getBooleanSort();
-    Sort uToInt = slv.mkFunctionSort(u, integer);
-    Sort intPred = slv.mkFunctionSort(integer, bool);
-
-    // Variables
-    Term x = slv.mkConst(u, "x");
-    Term y = slv.mkConst(u, "y");
-
-    // Functions
-    Term f = slv.mkConst(uToInt, "f");
-    Term p = slv.mkConst(intPred, "p");
-
-    // Constants
-    Term zero = slv.mkInteger(0);
-    Term one = slv.mkInteger(1);
-
-    // Terms
-    Term f_x = slv.mkTerm(Kind.APPLY_UF, f, x);
-    Term f_y = slv.mkTerm(Kind.APPLY_UF, f, y);
-    Term sum = slv.mkTerm(Kind.PLUS, f_x, f_y);
-    Term p_0 = slv.mkTerm(Kind.APPLY_UF, p, zero);
-    Term p_f_y = slv.mkTerm(Kind.APPLY_UF, p, f_y);
-
-    // Construct the assertions
-    Term assertions = slv.mkTerm(Kind.AND,
-        new Term[] {
-            slv.mkTerm(Kind.LEQ, zero, f_x), // 0 <= f(x)
-            slv.mkTerm(Kind.LEQ, zero, f_y), // 0 <= f(y)
-            slv.mkTerm(Kind.LEQ, sum, one), // f(x) + f(y) <= 1
-            p_0.notTerm(), // not p(0)
-            p_f_y // p(f(y))
-        });
-    slv.assertFormula(assertions);
-
-    System.out.println("Given the following assertions:\n" + assertions + "\n");
-
-    System.out.println("Prove x /= y is entailed. \n"
-        + "cvc5: " + slv.checkEntailed(slv.mkTerm(Kind.DISTINCT, x, y)) + ".\n");
-
-    System.out.println("Call checkSat to show that the assertions are satisfiable. \n"
-        + "cvc5: " + slv.checkSat() + ".\n");
-
-    System.out.println("Call slv.getValue(...) on terms of interest.");
-    System.out.println("slv.getValue(" + f_x + "): " + slv.getValue(f_x));
-    System.out.println("slv.getValue(" + f_y + "): " + slv.getValue(f_y));
-    System.out.println("slv.getValue(" + sum + "): " + slv.getValue(sum));
-    System.out.println("slv.getValue(" + p_0 + "): " + slv.getValue(p_0));
-    System.out.println("slv.getValue(" + p_f_y + "): " + slv.getValue(p_f_y) + "\n");
-
-    System.out.println("Alternatively, iterate over assertions and call slv.getValue(...) "
-        + "on all terms.");
-    prefixPrintGetValue(slv, assertions);
-
-    System.out.println();
-    System.out.println("You can also use nested loops to iterate over terms.");
-    Iterator<Term> it1 = assertions.iterator();
-    while (it1.hasNext())
+    try (Solver slv = new Solver())
     {
-      Term t = it1.next();
-      System.out.println("term: " + t);
-      Iterator<Term> it2 = t.iterator();
-      while (it2.hasNext())
+      slv.setOption("produce-models", "true"); // Produce Models
+      slv.setOption("dag-thresh", "0"); // Disable dagifying the output
+      slv.setOption("output-language", "smt2"); // use smt-lib v2 as output language
+      slv.setLogic("QF_UFLIRA");
+
+      // Sorts
+      Sort u = slv.mkUninterpretedSort("u");
+      Sort integer = slv.getIntegerSort();
+      Sort bool = slv.getBooleanSort();
+      Sort uToInt = slv.mkFunctionSort(u, integer);
+      Sort intPred = slv.mkFunctionSort(integer, bool);
+
+      // Variables
+      Term x = slv.mkConst(u, "x");
+      Term y = slv.mkConst(u, "y");
+
+      // Functions
+      Term f = slv.mkConst(uToInt, "f");
+      Term p = slv.mkConst(intPred, "p");
+
+      // Constants
+      Term zero = slv.mkInteger(0);
+      Term one = slv.mkInteger(1);
+
+      // Terms
+      Term f_x = slv.mkTerm(Kind.APPLY_UF, f, x);
+      Term f_y = slv.mkTerm(Kind.APPLY_UF, f, y);
+      Term sum = slv.mkTerm(Kind.PLUS, f_x, f_y);
+      Term p_0 = slv.mkTerm(Kind.APPLY_UF, p, zero);
+      Term p_f_y = slv.mkTerm(Kind.APPLY_UF, p, f_y);
+
+      // Construct the assertions
+      Term assertions = slv.mkTerm(Kind.AND,
+          new Term[] {
+              slv.mkTerm(Kind.LEQ, zero, f_x), // 0 <= f(x)
+              slv.mkTerm(Kind.LEQ, zero, f_y), // 0 <= f(y)
+              slv.mkTerm(Kind.LEQ, sum, one), // f(x) + f(y) <= 1
+              p_0.notTerm(), // not p(0)
+              p_f_y // p(f(y))
+          });
+      slv.assertFormula(assertions);
+
+      System.out.println("Given the following assertions:\n" + assertions + "\n");
+
+      System.out.println("Prove x /= y is entailed. \n"
+          + "cvc5: " + slv.checkEntailed(slv.mkTerm(Kind.DISTINCT, x, y)) + ".\n");
+
+      System.out.println("Call checkSat to show that the assertions are satisfiable. \n"
+          + "cvc5: " + slv.checkSat() + ".\n");
+
+      System.out.println("Call slv.getValue(...) on terms of interest.");
+      System.out.println("slv.getValue(" + f_x + "): " + slv.getValue(f_x));
+      System.out.println("slv.getValue(" + f_y + "): " + slv.getValue(f_y));
+      System.out.println("slv.getValue(" + sum + "): " + slv.getValue(sum));
+      System.out.println("slv.getValue(" + p_0 + "): " + slv.getValue(p_0));
+      System.out.println("slv.getValue(" + p_f_y + "): " + slv.getValue(p_f_y) + "\n");
+
+      System.out.println("Alternatively, iterate over assertions and call slv.getValue(...) "
+          + "on all terms.");
+      prefixPrintGetValue(slv, assertions);
+
+      System.out.println();
+      System.out.println("You can also use nested loops to iterate over terms.");
+      Iterator<Term> it1 = assertions.iterator();
+      while (it1.hasNext())
       {
-        System.out.println(" + child: " + it2.next());
+        Term t = it1.next();
+        System.out.println("term: " + t);
+        Iterator<Term> it2 = t.iterator();
+        while (it2.hasNext())
+        {
+          System.out.println(" + child: " + it2.next());
+        }
       }
-    }
-    System.out.println();
-    System.out.println("Alternatively, you can also use for-each loops.");
-    for (Term t : assertions)
-    {
-      System.out.println("term: " + t);
-      for (Term c : t)
+      System.out.println();
+      System.out.println("Alternatively, you can also use for-each loops.");
+      for (Term t : assertions)
       {
-        System.out.println(" + child: " + c);
+        System.out.println("term: " + t);
+        for (Term c : t)
+        {
+          System.out.println(" + child: " + c);
+        }
       }
     }
   }
diff --git a/examples/api/java/Datatypes.java b/examples/api/java/Datatypes.java
index 85f878098..b29419165 100644
--- a/examples/api/java/Datatypes.java
+++ b/examples/api/java/Datatypes.java
@@ -123,46 +123,48 @@ public class Datatypes
 
   public static void main(String[] args) throws CVC5ApiException
   {
-    Solver slv = new Solver();
-    // This example builds a simple "cons list" of integers, with
-    // two constructors, "cons" and "nil."
-
-    // Building a datatype consists of two steps.
-    // First, the datatype is specified.
-    // Second, it is "resolved" to an actual sort, at which point function
-    // symbols are assigned to its constructors, selectors, and testers.
-
-    DatatypeDecl consListSpec = slv.mkDatatypeDecl("list"); // give the datatype a name
-    DatatypeConstructorDecl cons = slv.mkDatatypeConstructorDecl("cons");
-    cons.addSelector("head", slv.getIntegerSort());
-    cons.addSelectorSelf("tail");
-    consListSpec.addConstructor(cons);
-    DatatypeConstructorDecl nil = slv.mkDatatypeConstructorDecl("nil");
-    consListSpec.addConstructor(nil);
-
-    System.out.println("spec is:"
-        + "\n" + consListSpec);
-
-    // Keep in mind that "DatatypeDecl" is the specification class for
-    // datatypes---"DatatypeDecl" is not itself a cvc5 Sort.
-    // Now that our Datatype is fully specified, we can get a Sort for it.
-    // This step resolves the "SelfSort" reference and creates
-    // symbols for all the constructors, etc.
-
-    Sort consListSort = slv.mkDatatypeSort(consListSpec);
-
-    test(slv, consListSort);
-
-    System.out.println("\n"
-        + ">>> Alternatively, use declareDatatype");
-    System.out.println("\n");
-
-    DatatypeConstructorDecl cons2 = slv.mkDatatypeConstructorDecl("cons");
-    cons2.addSelector("head", slv.getIntegerSort());
-    cons2.addSelectorSelf("tail");
-    DatatypeConstructorDecl nil2 = slv.mkDatatypeConstructorDecl("nil");
-    DatatypeConstructorDecl[] ctors = new DatatypeConstructorDecl[] {cons2, nil2};
-    Sort consListSort2 = slv.declareDatatype("list2", ctors);
-    test(slv, consListSort2);
+    try (Solver slv = new Solver())
+    {
+      // This example builds a simple "cons list" of integers, with
+      // two constructors, "cons" and "nil."
+
+      // Building a datatype consists of two steps.
+      // First, the datatype is specified.
+      // Second, it is "resolved" to an actual sort, at which point function
+      // symbols are assigned to its constructors, selectors, and testers.
+
+      DatatypeDecl consListSpec = slv.mkDatatypeDecl("list"); // give the datatype a name
+      DatatypeConstructorDecl cons = slv.mkDatatypeConstructorDecl("cons");
+      cons.addSelector("head", slv.getIntegerSort());
+      cons.addSelectorSelf("tail");
+      consListSpec.addConstructor(cons);
+      DatatypeConstructorDecl nil = slv.mkDatatypeConstructorDecl("nil");
+      consListSpec.addConstructor(nil);
+
+      System.out.println("spec is:"
+          + "\n" + consListSpec);
+
+      // Keep in mind that "DatatypeDecl" is the specification class for
+      // datatypes---"DatatypeDecl" is not itself a cvc5 Sort.
+      // Now that our Datatype is fully specified, we can get a Sort for it.
+      // This step resolves the "SelfSort" reference and creates
+      // symbols for all the constructors, etc.
+
+      Sort consListSort = slv.mkDatatypeSort(consListSpec);
+
+      test(slv, consListSort);
+
+      System.out.println("\n"
+          + ">>> Alternatively, use declareDatatype");
+      System.out.println("\n");
+
+      DatatypeConstructorDecl cons2 = slv.mkDatatypeConstructorDecl("cons");
+      cons2.addSelector("head", slv.getIntegerSort());
+      cons2.addSelectorSelf("tail");
+      DatatypeConstructorDecl nil2 = slv.mkDatatypeConstructorDecl("nil");
+      DatatypeConstructorDecl[] ctors = new DatatypeConstructorDecl[] {cons2, nil2};
+      Sort consListSort2 = slv.declareDatatype("list2", ctors);
+      test(slv, consListSort2);
+    }
   }
 }
diff --git a/examples/api/java/Exceptions.java b/examples/api/java/Exceptions.java
index 2d62a7570..bc142571d 100644
--- a/examples/api/java/Exceptions.java
+++ b/examples/api/java/Exceptions.java
@@ -21,45 +21,46 @@ public class Exceptions
 {
   public static void main(String[] args)
   {
-    Solver solver = new Solver();
-
-    solver.setOption("produce-models", "true");
-
-    // Setting an invalid option
-    try
-    {
-      solver.setOption("non-existing", "true");
-      System.exit(1);
-    }
-    catch (Exception e)
+    try (Solver solver = new Solver())
     {
-      System.out.println(e.toString());
-    }
+      solver.setOption("produce-models", "true");
 
-    // Creating a term with an invalid type
-    try
-    {
-      Sort integer = solver.getIntegerSort();
-      Term x = solver.mkVar(integer, "x");
-      Term invalidTerm = solver.mkTerm(Kind.AND, x, x);
-      solver.checkSatAssuming(invalidTerm);
-      System.exit(1);
-    }
-    catch (Exception e)
-    {
-      System.out.println(e.toString());
-    }
+      // Setting an invalid option
+      try
+      {
+        solver.setOption("non-existing", "true");
+        System.exit(1);
+      }
+      catch (Exception e)
+      {
+        System.out.println(e.toString());
+      }
 
-    // Asking for a model after unsat result
-    try
-    {
-      solver.checkSatAssuming(solver.mkBoolean(false));
-      solver.getModel(new Sort[] {}, new Term[] {});
-      System.exit(1);
-    }
-    catch (Exception e)
-    {
-      System.out.println(e.toString());
+      // Creating a term with an invalid type
+      try
+      {
+        Sort integer = solver.getIntegerSort();
+        Term x = solver.mkVar(integer, "x");
+        Term invalidTerm = solver.mkTerm(Kind.AND, x, x);
+        solver.checkSatAssuming(invalidTerm);
+        System.exit(1);
+      }
+      catch (Exception e)
+      {
+        System.out.println(e.toString());
+      }
+
+      // Asking for a model after unsat result
+      try
+      {
+        solver.checkSatAssuming(solver.mkBoolean(false));
+        solver.getModel(new Sort[] {}, new Term[] {});
+        System.exit(1);
+      }
+      catch (Exception e)
+      {
+        System.out.println(e.toString());
+      }
     }
   }
 }
diff --git a/examples/api/java/Extract.java b/examples/api/java/Extract.java
index 0d8d6c2b2..4ec0c100f 100644
--- a/examples/api/java/Extract.java
+++ b/examples/api/java/Extract.java
@@ -21,32 +21,34 @@ public class Extract
 {
   public static void main(String args[]) throws CVC5ApiException
   {
-    Solver slv = new Solver();
-    slv.setLogic("QF_BV"); // Set the logic
+    try (Solver slv = new Solver())
+    {
+      slv.setLogic("QF_BV"); // Set the logic
 
-    Sort bitvector32 = slv.mkBitVectorSort(32);
+      Sort bitvector32 = slv.mkBitVectorSort(32);
 
-    Term x = slv.mkConst(bitvector32, "a");
+      Term x = slv.mkConst(bitvector32, "a");
 
-    Op ext_31_1 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1);
-    Term x_31_1 = slv.mkTerm(ext_31_1, x);
+      Op ext_31_1 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 31, 1);
+      Term x_31_1 = slv.mkTerm(ext_31_1, x);
 
-    Op ext_30_0 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 30, 0);
-    Term x_30_0 = slv.mkTerm(ext_30_0, x);
+      Op ext_30_0 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 30, 0);
+      Term x_30_0 = slv.mkTerm(ext_30_0, x);
 
-    Op ext_31_31 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 31, 31);
-    Term x_31_31 = slv.mkTerm(ext_31_31, x);
+      Op ext_31_31 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 31, 31);
+      Term x_31_31 = slv.mkTerm(ext_31_31, x);
 
-    Op ext_0_0 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0);
-    Term x_0_0 = slv.mkTerm(ext_0_0, x);
+      Op ext_0_0 = slv.mkOp(Kind.BITVECTOR_EXTRACT, 0, 0);
+      Term x_0_0 = slv.mkTerm(ext_0_0, x);
 
-    Term eq = slv.mkTerm(Kind.EQUAL, x_31_1, x_30_0);
-    System.out.println(" Asserting: " + eq);
-    slv.assertFormula(eq);
+      Term eq = slv.mkTerm(Kind.EQUAL, x_31_1, x_30_0);
+      System.out.println(" Asserting: " + eq);
+      slv.assertFormula(eq);
 
-    Term eq2 = slv.mkTerm(Kind.EQUAL, x_31_31, x_0_0);
-    System.out.println(" Check entailment assuming: " + eq2);
-    System.out.println(" Expect ENTAILED. ");
-    System.out.println(" cvc5: " + slv.checkEntailed(eq2));
+      Term eq2 = slv.mkTerm(Kind.EQUAL, x_31_31, x_0_0);
+      System.out.println(" Check entailment assuming: " + eq2);
+      System.out.println(" Expect ENTAILED. ");
+      System.out.println(" cvc5: " + slv.checkEntailed(eq2));
+    }
   }
-}
\ No newline at end of file
+}
diff --git a/examples/api/java/FloatingPointArith.java b/examples/api/java/FloatingPointArith.java
index 88e24cbab..d8ed384d0 100644
--- a/examples/api/java/FloatingPointArith.java
+++ b/examples/api/java/FloatingPointArith.java
@@ -26,76 +26,78 @@ public class FloatingPointArith
 {
   public static void main(String[] args) throws CVC5ApiException
   {
-    Solver solver = new Solver();
-    solver.setOption("produce-models", "true");
+    try (Solver solver = new Solver())
+    {
+      solver.setOption("produce-models", "true");
 
-    // Make single precision floating-point variables
-    Sort fpt32 = solver.mkFloatingPointSort(8, 24);
-    Term a = solver.mkConst(fpt32, "a");
-    Term b = solver.mkConst(fpt32, "b");
-    Term c = solver.mkConst(fpt32, "c");
-    Term d = solver.mkConst(fpt32, "d");
-    Term e = solver.mkConst(fpt32, "e");
+      // Make single precision floating-point variables
+      Sort fpt32 = solver.mkFloatingPointSort(8, 24);
+      Term a = solver.mkConst(fpt32, "a");
+      Term b = solver.mkConst(fpt32, "b");
+      Term c = solver.mkConst(fpt32, "c");
+      Term d = solver.mkConst(fpt32, "d");
+      Term e = solver.mkConst(fpt32, "e");
 
-    // Assert that floating-point addition is not associative:
-    // (a + (b + c)) != ((a + b) + c)
-    Term rm = solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN);
-    Term lhs = solver.mkTerm(
-        Kind.FLOATINGPOINT_ADD, rm, a, solver.mkTerm(Kind.FLOATINGPOINT_ADD, rm, b, c));
-    Term rhs = solver.mkTerm(
-        Kind.FLOATINGPOINT_ADD, rm, solver.mkTerm(Kind.FLOATINGPOINT_ADD, rm, a, b), c);
-    solver.assertFormula(solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, a, b)));
+      // Assert that floating-point addition is not associative:
+      // (a + (b + c)) != ((a + b) + c)
+      Term rm = solver.mkRoundingMode(RoundingMode.ROUND_NEAREST_TIES_TO_EVEN);
+      Term lhs = solver.mkTerm(
+          Kind.FLOATINGPOINT_ADD, rm, a, solver.mkTerm(Kind.FLOATINGPOINT_ADD, rm, b, c));
+      Term rhs = solver.mkTerm(
+          Kind.FLOATINGPOINT_ADD, rm, solver.mkTerm(Kind.FLOATINGPOINT_ADD, rm, a, b), c);
+      solver.assertFormula(solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, a, b)));
 
-    Result r = solver.checkSat(); // result is sat
-    assert r.isSat();
+      Result r = solver.checkSat(); // result is sat
+      assert r.isSat();
 
-    System.out.println("a = " + solver.getValue(a));
-    System.out.println("b = " + solver.getValue(b));
-    System.out.println("c = " + solver.getValue(c));
+      System.out.println("a = " + solver.getValue(a));
+      System.out.println("b = " + solver.getValue(b));
+      System.out.println("c = " + solver.getValue(c));
 
-    // Now, let's restrict `a` to be either NaN or positive infinity
-    Term nan = solver.mkNaN(8, 24);
-    Term inf = solver.mkPosInf(8, 24);
-    solver.assertFormula(solver.mkTerm(
-        Kind.OR, solver.mkTerm(Kind.EQUAL, a, inf), solver.mkTerm(Kind.EQUAL, a, nan)));
+      // Now, let's restrict `a` to be either NaN or positive infinity
+      Term nan = solver.mkNaN(8, 24);
+      Term inf = solver.mkPosInf(8, 24);
+      solver.assertFormula(solver.mkTerm(
+          Kind.OR, solver.mkTerm(Kind.EQUAL, a, inf), solver.mkTerm(Kind.EQUAL, a, nan)));
 
-    r = solver.checkSat(); // result is sat
-    assert r.isSat();
+      r = solver.checkSat(); // result is sat
+      assert r.isSat();
 
-    System.out.println("a = " + solver.getValue(a));
-    System.out.println("b = " + solver.getValue(b));
-    System.out.println("c = " + solver.getValue(c));
+      System.out.println("a = " + solver.getValue(a));
+      System.out.println("b = " + solver.getValue(b));
+      System.out.println("c = " + solver.getValue(c));
 
-    // And now for something completely different. Let's try to find a (normal)
-    // floating-point number that rounds to different integer values for
-    // different rounding modes.
-    Term rtp = solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE);
-    Term rtn = solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE);
-    Op op = solver.mkOp(Kind.FLOATINGPOINT_TO_SBV, 16); // (_ fp.to_sbv 16)
-    lhs = solver.mkTerm(op, rtp, d);
-    rhs = solver.mkTerm(op, rtn, d);
-    solver.assertFormula(solver.mkTerm(Kind.FLOATINGPOINT_ISN, d));
-    solver.assertFormula(solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, lhs, rhs)));
+      // And now for something completely different. Let's try to find a (normal)
+      // floating-point number that rounds to different integer values for
+      // different rounding modes.
+      Term rtp = solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_POSITIVE);
+      Term rtn = solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_NEGATIVE);
+      Op op = solver.mkOp(Kind.FLOATINGPOINT_TO_SBV, 16); // (_ fp.to_sbv 16)
+      lhs = solver.mkTerm(op, rtp, d);
+      rhs = solver.mkTerm(op, rtn, d);
+      solver.assertFormula(solver.mkTerm(Kind.FLOATINGPOINT_ISN, d));
+      solver.assertFormula(solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.EQUAL, lhs, rhs)));
 
-    r = solver.checkSat(); // result is sat
-    assert r.isSat();
+      r = solver.checkSat(); // result is sat
+      assert r.isSat();
 
-    // Convert the result to a rational and print it
-    Term val = solver.getValue(d);
-    Term realVal = solver.getValue(solver.mkTerm(FLOATINGPOINT_TO_REAL, val));
-    System.out.println("d = " + val + " = " + realVal);
-    System.out.println("((_ fp.to_sbv 16) RTP d) = " + solver.getValue(lhs));
-    System.out.println("((_ fp.to_sbv 16) RTN d) = " + solver.getValue(rhs));
+      // Convert the result to a rational and print it
+      Term val = solver.getValue(d);
+      Term realVal = solver.getValue(solver.mkTerm(FLOATINGPOINT_TO_REAL, val));
+      System.out.println("d = " + val + " = " + realVal);
+      System.out.println("((_ fp.to_sbv 16) RTP d) = " + solver.getValue(lhs));
+      System.out.println("((_ fp.to_sbv 16) RTN d) = " + solver.getValue(rhs));
 
-    // For our final trick, let's try to find a floating-point number between
-    // positive zero and the smallest positive floating-point number
-    Term zero = solver.mkPosZero(8, 24);
-    Term smallest = solver.mkFloatingPoint(8, 24, solver.mkBitVector(32, 0b001));
-    solver.assertFormula(solver.mkTerm(Kind.AND,
-        solver.mkTerm(Kind.FLOATINGPOINT_LT, zero, e),
-        solver.mkTerm(Kind.FLOATINGPOINT_LT, e, smallest)));
+      // For our final trick, let's try to find a floating-point number between
+      // positive zero and the smallest positive floating-point number
+      Term zero = solver.mkPosZero(8, 24);
+      Term smallest = solver.mkFloatingPoint(8, 24, solver.mkBitVector(32, 0b001));
+      solver.assertFormula(solver.mkTerm(Kind.AND,
+          solver.mkTerm(Kind.FLOATINGPOINT_LT, zero, e),
+          solver.mkTerm(Kind.FLOATINGPOINT_LT, e, smallest)));
 
-    r = solver.checkSat(); // result is unsat
-    assert !r.isSat();
+      r = solver.checkSat(); // result is unsat
+      assert !r.isSat();
+    }
   }
 }
diff --git a/examples/api/java/HelloWorld.java b/examples/api/java/HelloWorld.java
index 966bfb329..7535430e3 100644
--- a/examples/api/java/HelloWorld.java
+++ b/examples/api/java/HelloWorld.java
@@ -19,9 +19,11 @@ public class HelloWorld
 {
   public static void main(String[] args)
   {
-    Solver slv = new Solver();
-    Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!");
+    try (Solver slv = new Solver())
+    {
+      Term helloworld = slv.mkVar(slv.getBooleanSort(), "Hello World!");
 
-    System.out.println(helloworld + " is " + slv.checkEntailed(helloworld));
+      System.out.println(helloworld + " is " + slv.checkEntailed(helloworld));
+    }
   }
 }
diff --git a/examples/api/java/LinearArith.java b/examples/api/java/LinearArith.java
index 2e67d526f..1f8153e44 100644
--- a/examples/api/java/LinearArith.java
+++ b/examples/api/java/LinearArith.java
@@ -19,57 +19,59 @@ public class LinearArith
 {
   public static void main(String args[]) throws CVC5ApiException
   {
-    Solver slv = new Solver();
-    slv.setLogic("QF_LIRA"); // Set the logic
+    try (Solver slv = new Solver())
+    {
+      slv.setLogic("QF_LIRA"); // Set the logic
 
-    // Prove that if given x (Integer) and y (Real) then
-    // the maximum value of y - x is 2/3
+      // Prove that if given x (Integer) and y (Real) then
+      // the maximum value of y - x is 2/3
 
-    // Sorts
-    Sort real = slv.getRealSort();
-    Sort integer = slv.getIntegerSort();
+      // Sorts
+      Sort real = slv.getRealSort();
+      Sort integer = slv.getIntegerSort();
 
-    // Variables
-    Term x = slv.mkConst(integer, "x");
-    Term y = slv.mkConst(real, "y");
+      // Variables
+      Term x = slv.mkConst(integer, "x");
+      Term y = slv.mkConst(real, "y");
 
-    // Constants
-    Term three = slv.mkInteger(3);
-    Term neg2 = slv.mkInteger(-2);
-    Term two_thirds = slv.mkReal(2, 3);
+      // Constants
+      Term three = slv.mkInteger(3);
+      Term neg2 = slv.mkInteger(-2);
+      Term two_thirds = slv.mkReal(2, 3);
 
-    // Terms
-    Term three_y = slv.mkTerm(Kind.MULT, three, y);
-    Term diff = slv.mkTerm(Kind.MINUS, y, x);
+      // Terms
+      Term three_y = slv.mkTerm(Kind.MULT, three, y);
+      Term diff = slv.mkTerm(Kind.MINUS, y, x);
 
-    // Formulas
-    Term x_geq_3y = slv.mkTerm(Kind.GEQ, x, three_y);
-    Term x_leq_y = slv.mkTerm(Kind.LEQ, x, y);
-    Term neg2_lt_x = slv.mkTerm(Kind.LT, neg2, x);
+      // Formulas
+      Term x_geq_3y = slv.mkTerm(Kind.GEQ, x, three_y);
+      Term x_leq_y = slv.mkTerm(Kind.LEQ, x, y);
+      Term neg2_lt_x = slv.mkTerm(Kind.LT, neg2, x);
 
-    Term assertions = slv.mkTerm(Kind.AND, x_geq_3y, x_leq_y, neg2_lt_x);
+      Term assertions = slv.mkTerm(Kind.AND, x_geq_3y, x_leq_y, neg2_lt_x);
 
-    System.out.println("Given the assertions " + assertions);
-    slv.assertFormula(assertions);
+      System.out.println("Given the assertions " + assertions);
+      slv.assertFormula(assertions);
 
-    slv.push();
-    Term diff_leq_two_thirds = slv.mkTerm(Kind.LEQ, diff, two_thirds);
-    System.out.println("Prove that " + diff_leq_two_thirds + " with cvc5.");
-    System.out.println("cvc5 should report ENTAILED.");
-    System.out.println("Result from cvc5 is: " + slv.checkEntailed(diff_leq_two_thirds));
-    slv.pop();
+      slv.push();
+      Term diff_leq_two_thirds = slv.mkTerm(Kind.LEQ, diff, two_thirds);
+      System.out.println("Prove that " + diff_leq_two_thirds + " with cvc5.");
+      System.out.println("cvc5 should report ENTAILED.");
+      System.out.println("Result from cvc5 is: " + slv.checkEntailed(diff_leq_two_thirds));
+      slv.pop();
 
-    System.out.println();
+      System.out.println();
 
-    slv.push();
-    Term diff_is_two_thirds = slv.mkTerm(Kind.EQUAL, diff, two_thirds);
-    slv.assertFormula(diff_is_two_thirds);
-    System.out.println("Show that the assertions are consistent with ");
-    System.out.println(diff_is_two_thirds + " with cvc5.");
-    System.out.println("cvc5 should report SAT.");
-    System.out.println("Result from cvc5 is: " + slv.checkSat());
-    slv.pop();
+      slv.push();
+      Term diff_is_two_thirds = slv.mkTerm(Kind.EQUAL, diff, two_thirds);
+      slv.assertFormula(diff_is_two_thirds);
+      System.out.println("Show that the assertions are consistent with ");
+      System.out.println(diff_is_two_thirds + " with cvc5.");
+      System.out.println("cvc5 should report SAT.");
+      System.out.println("Result from cvc5 is: " + slv.checkSat());
+      slv.pop();
 
-    System.out.println("Thus the maximum value of (y - x) is 2/3.");
+      System.out.println("Thus the maximum value of (y - x) is 2/3.");
+    }
   }
 }
\ No newline at end of file
diff --git a/examples/api/java/QuickStart.java b/examples/api/java/QuickStart.java
index 73bddb083..a79263cbf 100644
--- a/examples/api/java/QuickStart.java
+++ b/examples/api/java/QuickStart.java
@@ -25,123 +25,124 @@ public class QuickStart
   public static void main(String args[]) throws CVC5ApiException
   {
     // Create a solver
-    Solver solver = new Solver();
-
-    // We will ask the solver to produce models and unsat cores,
-    // hence these options should be turned on.
-    solver.setOption("produce-models", "true");
-    solver.setOption("produce-unsat-cores", "true");
-
-    // The simplest way to set a logic for the solver is to choose "ALL".
-    // This enables all logics in the solver.
-    // Alternatively, "QF_ALL" enables all logics without quantifiers.
-    // To optimize the solver's behavior for a more specific logic,
-    // use the logic name, e.g. "QF_BV" or "QF_AUFBV".
-
-    // Set the logic
-    solver.setLogic("ALL");
-
-    // In this example, we will define constraints over reals and integers.
-    // Hence, we first obtain the corresponding sorts.
-    Sort realSort = solver.getRealSort();
-    Sort intSort = solver.getIntegerSort();
-
-    // x and y will be real variables, while a and b will be integer variables.
-    // Formally, their cpp type is Term,
-    // and they are called "constants" in SMT jargon:
-    Term x = solver.mkConst(realSort, "x");
-    Term y = solver.mkConst(realSort, "y");
-    Term a = solver.mkConst(intSort, "a");
-    Term b = solver.mkConst(intSort, "b");
-
-    // Our constraints regarding x and y will be:
-    //
-    //   (1)  0 < x
-    //   (2)  0 < y
-    //   (3)  x + y < 1
-    //   (4)  x <= y
-    //
-
-    // Formally, constraints are also terms. Their sort is Boolean.
-    // We will construct these constraints gradually,
-    // by defining each of their components.
-    // We start with the constant numerals 0 and 1:
-    Term zero = solver.mkReal(0);
-    Term one = solver.mkReal(1);
-
-    // Next, we construct the term x + y
-    Term xPlusY = solver.mkTerm(Kind.PLUS, x, y);
-
-    // Now we can define the constraints.
-    // They use the operators +, <=, and <.
-    // In the API, these are denoted by PLUS, LEQ, and LT.
-    // A list of available operators is available in:
-    // src/api/cpp/cvc5_kind.h
-    Term constraint1 = solver.mkTerm(Kind.LT, zero, x);
-    Term constraint2 = solver.mkTerm(Kind.LT, zero, y);
-    Term constraint3 = solver.mkTerm(Kind.LT, xPlusY, one);
-    Term constraint4 = solver.mkTerm(Kind.LEQ, x, y);
-
-    // Now we assert the constraints to the solver.
-    solver.assertFormula(constraint1);
-    solver.assertFormula(constraint2);
-    solver.assertFormula(constraint3);
-    solver.assertFormula(constraint4);
-
-    // Check if the formula is satisfiable, that is,
-    // are there real values for x and y that satisfy all the constraints?
-    Result r1 = solver.checkSat();
-
-    // The result is either SAT, UNSAT, or UNKNOWN.
-    // In this case, it is SAT.
-    System.out.println("expected: sat");
-    System.out.println("result: " + r1);
-
-    // We can get the values for x and y that satisfy the constraints.
-    Term xVal = solver.getValue(x);
-    Term yVal = solver.getValue(y);
-
-    // It is also possible to get values for compound terms,
-    // even if those did not appear in the original formula.
-    Term xMinusY = solver.mkTerm(Kind.MINUS, x, y);
-    Term xMinusYVal = solver.getValue(xMinusY);
-
-    // Further, we can convert the values to java types,
-    Pair<BigInteger, BigInteger> xRational = xVal.getRealValue();
-    Pair<BigInteger, BigInteger> yRational = yVal.getRealValue();
-    System.out.println("value for x: " + xRational.first + "/" + xRational.second);
-    System.out.println("value for y: " + yRational.first + "/" + yRational.second);
-
-    // Next, we will check satisfiability of the same formula,
-    // only this time over integer variables a and b.
-
-    // We start by resetting assertions added to the solver.
-    solver.resetAssertions();
-
-    // Next, we assert the same assertions above with integers.
-    // This time, we inline the construction of terms
-    // to the assertion command.
-    solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a));
-    solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b));
-    solver.assertFormula(
-        solver.mkTerm(Kind.LT, solver.mkTerm(Kind.PLUS, a, b), solver.mkInteger(1)));
-    solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b));
-
-    // We check whether the revised assertion is satisfiable.
-    Result r2 = solver.checkSat();
-
-    // This time the formula is unsatisfiable
-    System.out.println("expected: unsat");
-    System.out.println("result: " + r2);
-
-    // We can query the solver for an unsatisfiable core, i.e., a subset
-    // of the assertions that is already unsatisfiable.
-    List<Term> unsatCore = Arrays.asList(solver.getUnsatCore());
-    System.out.println("unsat core size: " + unsatCore.size());
-    System.out.println("unsat core: ");
-    for (Term t : unsatCore)
+    try (Solver solver = new Solver())
     {
-      System.out.println(t);
+      // We will ask the solver to produce models and unsat cores,
+      // hence these options should be turned on.
+      solver.setOption("produce-models", "true");
+      solver.setOption("produce-unsat-cores", "true");
+
+      // The simplest way to set a logic for the solver is to choose "ALL".
+      // This enables all logics in the solver.
+      // Alternatively, "QF_ALL" enables all logics without quantifiers.
+      // To optimize the solver's behavior for a more specific logic,
+      // use the logic name, e.g. "QF_BV" or "QF_AUFBV".
+
+      // Set the logic
+      solver.setLogic("ALL");
+
+      // In this example, we will define constraints over reals and integers.
+      // Hence, we first obtain the corresponding sorts.
+      Sort realSort = solver.getRealSort();
+      Sort intSort = solver.getIntegerSort();
+
+      // x and y will be real variables, while a and b will be integer variables.
+      // Formally, their cpp type is Term,
+      // and they are called "constants" in SMT jargon:
+      Term x = solver.mkConst(realSort, "x");
+      Term y = solver.mkConst(realSort, "y");
+      Term a = solver.mkConst(intSort, "a");
+      Term b = solver.mkConst(intSort, "b");
+
+      // Our constraints regarding x and y will be:
+      //
+      //   (1)  0 < x
+      //   (2)  0 < y
+      //   (3)  x + y < 1
+      //   (4)  x <= y
+      //
+
+      // Formally, constraints are also terms. Their sort is Boolean.
+      // We will construct these constraints gradually,
+      // by defining each of their components.
+      // We start with the constant numerals 0 and 1:
+      Term zero = solver.mkReal(0);
+      Term one = solver.mkReal(1);
+
+      // Next, we construct the term x + y
+      Term xPlusY = solver.mkTerm(Kind.PLUS, x, y);
+
+      // Now we can define the constraints.
+      // They use the operators +, <=, and <.
+      // In the API, these are denoted by PLUS, LEQ, and LT.
+      // A list of available operators is available in:
+      // src/api/cpp/cvc5_kind.h
+      Term constraint1 = solver.mkTerm(Kind.LT, zero, x);
+      Term constraint2 = solver.mkTerm(Kind.LT, zero, y);
+      Term constraint3 = solver.mkTerm(Kind.LT, xPlusY, one);
+      Term constraint4 = solver.mkTerm(Kind.LEQ, x, y);
+
+      // Now we assert the constraints to the solver.
+      solver.assertFormula(constraint1);
+      solver.assertFormula(constraint2);
+      solver.assertFormula(constraint3);
+      solver.assertFormula(constraint4);
+
+      // Check if the formula is satisfiable, that is,
+      // are there real values for x and y that satisfy all the constraints?
+      Result r1 = solver.checkSat();
+
+      // The result is either SAT, UNSAT, or UNKNOWN.
+      // In this case, it is SAT.
+      System.out.println("expected: sat");
+      System.out.println("result: " + r1);
+
+      // We can get the values for x and y that satisfy the constraints.
+      Term xVal = solver.getValue(x);
+      Term yVal = solver.getValue(y);
+
+      // It is also possible to get values for compound terms,
+      // even if those did not appear in the original formula.
+      Term xMinusY = solver.mkTerm(Kind.MINUS, x, y);
+      Term xMinusYVal = solver.getValue(xMinusY);
+
+      // Further, we can convert the values to java types,
+      Pair<BigInteger, BigInteger> xRational = xVal.getRealValue();
+      Pair<BigInteger, BigInteger> yRational = yVal.getRealValue();
+      System.out.println("value for x: " + xRational.first + "/" + xRational.second);
+      System.out.println("value for y: " + yRational.first + "/" + yRational.second);
+
+      // Next, we will check satisfiability of the same formula,
+      // only this time over integer variables a and b.
+
+      // We start by resetting assertions added to the solver.
+      solver.resetAssertions();
+
+      // Next, we assert the same assertions above with integers.
+      // This time, we inline the construction of terms
+      // to the assertion command.
+      solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), a));
+      solver.assertFormula(solver.mkTerm(Kind.LT, solver.mkInteger(0), b));
+      solver.assertFormula(
+          solver.mkTerm(Kind.LT, solver.mkTerm(Kind.PLUS, a, b), solver.mkInteger(1)));
+      solver.assertFormula(solver.mkTerm(Kind.LEQ, a, b));
+
+      // We check whether the revised assertion is satisfiable.
+      Result r2 = solver.checkSat();
+
+      // This time the formula is unsatisfiable
+      System.out.println("expected: unsat");
+      System.out.println("result: " + r2);
+
+      // We can query the solver for an unsatisfiable core, i.e., a subset
+      // of the assertions that is already unsatisfiable.
+      List<Term> unsatCore = Arrays.asList(solver.getUnsatCore());
+      System.out.println("unsat core size: " + unsatCore.size());
+      System.out.println("unsat core: ");
+      for (Term t : unsatCore)
+      {
+        System.out.println(t);
+      }
     }
   }
 }
\ No newline at end of file
diff --git a/examples/api/java/Relations.java b/examples/api/java/Relations.java
index f6454c812..0d78562bb 100644
--- a/examples/api/java/Relations.java
+++ b/examples/api/java/Relations.java
@@ -69,129 +69,131 @@ public class Relations
 {
   public static void main(String[] args) throws CVC5ApiException
   {
-    Solver solver = new Solver();
-
-    // Set the logic
-    solver.setLogic("ALL");
-
-    // options
-    solver.setOption("produce-models", "true");
-    solver.setOption("finite-model-find", "true");
-    solver.setOption("sets-ext", "true");
-    solver.setOption("output-language", "smt2");
-
-    // (declare-sort Person 0)
-    Sort personSort = solver.mkUninterpretedSort("Person");
-
-    // (Tuple Person)
-    Sort tupleArity1 = solver.mkTupleSort(new Sort[] {personSort});
-    // (Set (Tuple Person))
-    Sort relationArity1 = solver.mkSetSort(tupleArity1);
-
-    // (Tuple Person Person)
-    Sort tupleArity2 = solver.mkTupleSort(new Sort[] {personSort, personSort});
-    // (Set (Tuple Person Person))
-    Sort relationArity2 = solver.mkSetSort(tupleArity2);
-
-    // empty set
-    Term emptySetTerm = solver.mkEmptySet(relationArity1);
-
-    // empty relation
-    Term emptyRelationTerm = solver.mkEmptySet(relationArity2);
-
-    // universe set
-    Term universeSet = solver.mkUniverseSet(relationArity1);
-
-    // variables
-    Term people = solver.mkConst(relationArity1, "people");
-    Term males = solver.mkConst(relationArity1, "males");
-    Term females = solver.mkConst(relationArity1, "females");
-    Term father = solver.mkConst(relationArity2, "father");
-    Term mother = solver.mkConst(relationArity2, "mother");
-    Term parent = solver.mkConst(relationArity2, "parent");
-    Term ancestor = solver.mkConst(relationArity2, "ancestor");
-    Term descendant = solver.mkConst(relationArity2, "descendant");
-
-    Term isEmpty1 = solver.mkTerm(EQUAL, males, emptySetTerm);
-    Term isEmpty2 = solver.mkTerm(EQUAL, females, emptySetTerm);
-
-    // (assert (= people (as univset (Set (Tuple Person)))))
-    Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet);
-    // (assert (not (= males (as emptyset (Set (Tuple Person))))))
-    Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1);
-    // (assert (not (= females (as emptyset (Set (Tuple Person))))))
-    Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2);
-
-    // (assert (= (intersection males females) (as emptyset (Set (Tuple
-    // Person)))))
-    Term malesFemalesIntersection = solver.mkTerm(INTERSECTION, males, females);
-    Term malesAndFemalesAreDisjoint = solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm);
-
-    // (assert (not (= father (as emptyset (Set (Tuple Person Person))))))
-    // (assert (not (= mother (as emptyset (Set (Tuple Person Person))))))
-    Term isEmpty3 = solver.mkTerm(EQUAL, father, emptyRelationTerm);
-    Term isEmpty4 = solver.mkTerm(EQUAL, mother, emptyRelationTerm);
-    Term fatherIsNotEmpty = solver.mkTerm(NOT, isEmpty3);
-    Term motherIsNotEmpty = solver.mkTerm(NOT, isEmpty4);
-
-    // fathers are males
-    // (assert (subset (join father people) males))
-    Term fathers = solver.mkTerm(JOIN, father, people);
-    Term fathersAreMales = solver.mkTerm(SUBSET, fathers, males);
-
-    // mothers are females
-    // (assert (subset (join mother people) females))
-    Term mothers = solver.mkTerm(JOIN, mother, people);
-    Term mothersAreFemales = solver.mkTerm(SUBSET, mothers, females);
-
-    // (assert (= parent (union father mother)))
-    Term unionFatherMother = solver.mkTerm(UNION, father, mother);
-    Term parentIsFatherOrMother = solver.mkTerm(EQUAL, parent, unionFatherMother);
-
-    // (assert (= parent (union father mother)))
-    Term transitiveClosure = solver.mkTerm(TCLOSURE, parent);
-    Term descendantFormula = solver.mkTerm(EQUAL, descendant, transitiveClosure);
-
-    // (assert (= parent (union father mother)))
-    Term transpose = solver.mkTerm(TRANSPOSE, descendant);
-    Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transpose);
-
-    // (assert (forall ((x Person)) (not (member (mkTuple x x) ancestor))))
-    Term x = solver.mkVar(personSort, "x");
-    DatatypeConstructor constructor = tupleArity2.getDatatype().getConstructor(0);
-    Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getConstructorTerm(), x, x);
-    Term member = solver.mkTerm(MEMBER, xxTuple, ancestor);
-    Term notMember = solver.mkTerm(NOT, member);
-
-    Term quantifiedVariables = solver.mkTerm(BOUND_VAR_LIST, x);
-    Term noSelfAncestor = solver.mkTerm(FORALL, quantifiedVariables, notMember);
-
-    // formulas
-    solver.assertFormula(peopleAreTheUniverse);
-    solver.assertFormula(maleSetIsNotEmpty);
-    solver.assertFormula(femaleSetIsNotEmpty);
-    solver.assertFormula(malesAndFemalesAreDisjoint);
-    solver.assertFormula(fatherIsNotEmpty);
-    solver.assertFormula(motherIsNotEmpty);
-    solver.assertFormula(fathersAreMales);
-    solver.assertFormula(mothersAreFemales);
-    solver.assertFormula(parentIsFatherOrMother);
-    solver.assertFormula(descendantFormula);
-    solver.assertFormula(ancestorFormula);
-    solver.assertFormula(noSelfAncestor);
-
-    // check sat
-    Result result = solver.checkSat();
-
-    // output
-    System.out.println("Result     = " + result);
-    System.out.println("people     = " + solver.getValue(people));
-    System.out.println("males      = " + solver.getValue(males));
-    System.out.println("females    = " + solver.getValue(females));
-    System.out.println("father     = " + solver.getValue(father));
-    System.out.println("mother     = " + solver.getValue(mother));
-    System.out.println("parent     = " + solver.getValue(parent));
-    System.out.println("descendant = " + solver.getValue(descendant));
-    System.out.println("ancestor   = " + solver.getValue(ancestor));
+    try (Solver solver = new Solver())
+    {
+      // Set the logic
+      solver.setLogic("ALL");
+
+      // options
+      solver.setOption("produce-models", "true");
+      solver.setOption("finite-model-find", "true");
+      solver.setOption("sets-ext", "true");
+      solver.setOption("output-language", "smt2");
+
+      // (declare-sort Person 0)
+      Sort personSort = solver.mkUninterpretedSort("Person");
+
+      // (Tuple Person)
+      Sort tupleArity1 = solver.mkTupleSort(new Sort[] {personSort});
+      // (Set (Tuple Person))
+      Sort relationArity1 = solver.mkSetSort(tupleArity1);
+
+      // (Tuple Person Person)
+      Sort tupleArity2 = solver.mkTupleSort(new Sort[] {personSort, personSort});
+      // (Set (Tuple Person Person))
+      Sort relationArity2 = solver.mkSetSort(tupleArity2);
+
+      // empty set
+      Term emptySetTerm = solver.mkEmptySet(relationArity1);
+
+      // empty relation
+      Term emptyRelationTerm = solver.mkEmptySet(relationArity2);
+
+      // universe set
+      Term universeSet = solver.mkUniverseSet(relationArity1);
+
+      // variables
+      Term people = solver.mkConst(relationArity1, "people");
+      Term males = solver.mkConst(relationArity1, "males");
+      Term females = solver.mkConst(relationArity1, "females");
+      Term father = solver.mkConst(relationArity2, "father");
+      Term mother = solver.mkConst(relationArity2, "mother");
+      Term parent = solver.mkConst(relationArity2, "parent");
+      Term ancestor = solver.mkConst(relationArity2, "ancestor");
+      Term descendant = solver.mkConst(relationArity2, "descendant");
+
+      Term isEmpty1 = solver.mkTerm(EQUAL, males, emptySetTerm);
+      Term isEmpty2 = solver.mkTerm(EQUAL, females, emptySetTerm);
+
+      // (assert (= people (as univset (Set (Tuple Person)))))
+      Term peopleAreTheUniverse = solver.mkTerm(EQUAL, people, universeSet);
+      // (assert (not (= males (as emptyset (Set (Tuple Person))))))
+      Term maleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty1);
+      // (assert (not (= females (as emptyset (Set (Tuple Person))))))
+      Term femaleSetIsNotEmpty = solver.mkTerm(NOT, isEmpty2);
+
+      // (assert (= (intersection males females) (as emptyset (Set (Tuple
+      // Person)))))
+      Term malesFemalesIntersection = solver.mkTerm(INTERSECTION, males, females);
+      Term malesAndFemalesAreDisjoint =
+          solver.mkTerm(EQUAL, malesFemalesIntersection, emptySetTerm);
+
+      // (assert (not (= father (as emptyset (Set (Tuple Person Person))))))
+      // (assert (not (= mother (as emptyset (Set (Tuple Person Person))))))
+      Term isEmpty3 = solver.mkTerm(EQUAL, father, emptyRelationTerm);
+      Term isEmpty4 = solver.mkTerm(EQUAL, mother, emptyRelationTerm);
+      Term fatherIsNotEmpty = solver.mkTerm(NOT, isEmpty3);
+      Term motherIsNotEmpty = solver.mkTerm(NOT, isEmpty4);
+
+      // fathers are males
+      // (assert (subset (join father people) males))
+      Term fathers = solver.mkTerm(JOIN, father, people);
+      Term fathersAreMales = solver.mkTerm(SUBSET, fathers, males);
+
+      // mothers are females
+      // (assert (subset (join mother people) females))
+      Term mothers = solver.mkTerm(JOIN, mother, people);
+      Term mothersAreFemales = solver.mkTerm(SUBSET, mothers, females);
+
+      // (assert (= parent (union father mother)))
+      Term unionFatherMother = solver.mkTerm(UNION, father, mother);
+      Term parentIsFatherOrMother = solver.mkTerm(EQUAL, parent, unionFatherMother);
+
+      // (assert (= parent (union father mother)))
+      Term transitiveClosure = solver.mkTerm(TCLOSURE, parent);
+      Term descendantFormula = solver.mkTerm(EQUAL, descendant, transitiveClosure);
+
+      // (assert (= parent (union father mother)))
+      Term transpose = solver.mkTerm(TRANSPOSE, descendant);
+      Term ancestorFormula = solver.mkTerm(EQUAL, ancestor, transpose);
+
+      // (assert (forall ((x Person)) (not (member (mkTuple x x) ancestor))))
+      Term x = solver.mkVar(personSort, "x");
+      DatatypeConstructor constructor = tupleArity2.getDatatype().getConstructor(0);
+      Term xxTuple = solver.mkTerm(APPLY_CONSTRUCTOR, constructor.getConstructorTerm(), x, x);
+      Term member = solver.mkTerm(MEMBER, xxTuple, ancestor);
+      Term notMember = solver.mkTerm(NOT, member);
+
+      Term quantifiedVariables = solver.mkTerm(BOUND_VAR_LIST, x);
+      Term noSelfAncestor = solver.mkTerm(FORALL, quantifiedVariables, notMember);
+
+      // formulas
+      solver.assertFormula(peopleAreTheUniverse);
+      solver.assertFormula(maleSetIsNotEmpty);
+      solver.assertFormula(femaleSetIsNotEmpty);
+      solver.assertFormula(malesAndFemalesAreDisjoint);
+      solver.assertFormula(fatherIsNotEmpty);
+      solver.assertFormula(motherIsNotEmpty);
+      solver.assertFormula(fathersAreMales);
+      solver.assertFormula(mothersAreFemales);
+      solver.assertFormula(parentIsFatherOrMother);
+      solver.assertFormula(descendantFormula);
+      solver.assertFormula(ancestorFormula);
+      solver.assertFormula(noSelfAncestor);
+
+      // check sat
+      Result result = solver.checkSat();
+
+      // output
+      System.out.println("Result     = " + result);
+      System.out.println("people     = " + solver.getValue(people));
+      System.out.println("males      = " + solver.getValue(males));
+      System.out.println("females    = " + solver.getValue(females));
+      System.out.println("father     = " + solver.getValue(father));
+      System.out.println("mother     = " + solver.getValue(mother));
+      System.out.println("parent     = " + solver.getValue(parent));
+      System.out.println("descendant = " + solver.getValue(descendant));
+      System.out.println("ancestor   = " + solver.getValue(ancestor));
+    }
   }
 }
diff --git a/examples/api/java/Sequences.java b/examples/api/java/Sequences.java
index d1bb0440d..0fd578984 100644
--- a/examples/api/java/Sequences.java
+++ b/examples/api/java/Sequences.java
@@ -21,48 +21,49 @@ public class Sequences
 {
   public static void main(String args[]) throws CVC5ApiException
   {
-    Solver slv = new Solver();
-
-    // Set the logic
-    slv.setLogic("QF_SLIA");
-    // Produce models
-    slv.setOption("produce-models", "true");
-    // The option strings-exp is needed
-    slv.setOption("strings-exp", "true");
-    // Set output language to SMTLIB2
-    slv.setOption("output-language", "smt2");
+    try (Solver slv = new Solver())
+    {
+      // Set the logic
+      slv.setLogic("QF_SLIA");
+      // Produce models
+      slv.setOption("produce-models", "true");
+      // The option strings-exp is needed
+      slv.setOption("strings-exp", "true");
+      // Set output language to SMTLIB2
+      slv.setOption("output-language", "smt2");
 
-    // Sequence sort
-    Sort intSeq = slv.mkSequenceSort(slv.getIntegerSort());
+      // Sequence sort
+      Sort intSeq = slv.mkSequenceSort(slv.getIntegerSort());
 
-    // Sequence variables
-    Term x = slv.mkConst(intSeq, "x");
-    Term y = slv.mkConst(intSeq, "y");
+      // Sequence variables
+      Term x = slv.mkConst(intSeq, "x");
+      Term y = slv.mkConst(intSeq, "y");
 
-    // Empty sequence
-    Term empty = slv.mkEmptySequence(slv.getIntegerSort());
-    // Sequence concatenation: x.y.empty
-    Term concat = slv.mkTerm(SEQ_CONCAT, x, y, empty);
-    // Sequence length: |x.y.empty|
-    Term concat_len = slv.mkTerm(SEQ_LENGTH, concat);
-    // |x.y.empty| > 1
-    Term formula1 = slv.mkTerm(GT, concat_len, slv.mkInteger(1));
-    // Sequence unit: seq(1)
-    Term unit = slv.mkTerm(SEQ_UNIT, slv.mkInteger(1));
-    // x = seq(1)
-    Term formula2 = slv.mkTerm(EQUAL, x, unit);
+      // Empty sequence
+      Term empty = slv.mkEmptySequence(slv.getIntegerSort());
+      // Sequence concatenation: x.y.empty
+      Term concat = slv.mkTerm(SEQ_CONCAT, x, y, empty);
+      // Sequence length: |x.y.empty|
+      Term concat_len = slv.mkTerm(SEQ_LENGTH, concat);
+      // |x.y.empty| > 1
+      Term formula1 = slv.mkTerm(GT, concat_len, slv.mkInteger(1));
+      // Sequence unit: seq(1)
+      Term unit = slv.mkTerm(SEQ_UNIT, slv.mkInteger(1));
+      // x = seq(1)
+      Term formula2 = slv.mkTerm(EQUAL, x, unit);
 
-    // Make a query
-    Term q = slv.mkTerm(AND, formula1, formula2);
+      // Make a query
+      Term q = slv.mkTerm(AND, formula1, formula2);
 
-    // check sat
-    Result result = slv.checkSatAssuming(q);
-    System.out.println("cvc5 reports: " + q + " is " + result + ".");
+      // check sat
+      Result result = slv.checkSatAssuming(q);
+      System.out.println("cvc5 reports: " + q + " is " + result + ".");
 
-    if (result.isSat())
-    {
-      System.out.println("  x = " + slv.getValue(x));
-      System.out.println("  y = " + slv.getValue(y));
+      if (result.isSat())
+      {
+        System.out.println("  x = " + slv.getValue(x));
+        System.out.println("  y = " + slv.getValue(y));
+      }
     }
   }
 }
\ No newline at end of file
diff --git a/examples/api/java/Sets.java b/examples/api/java/Sets.java
index 602014c96..3edc49ae6 100644
--- a/examples/api/java/Sets.java
+++ b/examples/api/java/Sets.java
@@ -21,72 +21,73 @@ public class Sets
 {
   public static void main(String args[]) throws CVC5ApiException
   {
-    Solver slv = new Solver();
-
-    // Optionally, set the logic. We need at least UF for equality predicate,
-    // integers (LIA) and sets (FS).
-    slv.setLogic("QF_UFLIAFS");
+    try (Solver slv = new Solver())
+    {
+      // Optionally, set the logic. We need at least UF for equality predicate,
+      // integers (LIA) and sets (FS).
+      slv.setLogic("QF_UFLIAFS");
 
-    // Produce models
-    slv.setOption("produce-models", "true");
-    slv.setOption("output-language", "smt2");
+      // Produce models
+      slv.setOption("produce-models", "true");
+      slv.setOption("output-language", "smt2");
 
-    Sort integer = slv.getIntegerSort();
-    Sort set = slv.mkSetSort(integer);
+      Sort integer = slv.getIntegerSort();
+      Sort set = slv.mkSetSort(integer);
 
-    // Verify union distributions over intersection
-    // (A union B) intersection C = (A intersection C) union (B intersection C)
-    {
-      Term A = slv.mkConst(set, "A");
-      Term B = slv.mkConst(set, "B");
-      Term C = slv.mkConst(set, "C");
+      // Verify union distributions over intersection
+      // (A union B) intersection C = (A intersection C) union (B intersection C)
+      {
+        Term A = slv.mkConst(set, "A");
+        Term B = slv.mkConst(set, "B");
+        Term C = slv.mkConst(set, "C");
 
-      Term unionAB = slv.mkTerm(UNION, A, B);
-      Term lhs = slv.mkTerm(INTERSECTION, unionAB, C);
+        Term unionAB = slv.mkTerm(UNION, A, B);
+        Term lhs = slv.mkTerm(INTERSECTION, unionAB, C);
 
-      Term intersectionAC = slv.mkTerm(INTERSECTION, A, C);
-      Term intersectionBC = slv.mkTerm(INTERSECTION, B, C);
-      Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC);
+        Term intersectionAC = slv.mkTerm(INTERSECTION, A, C);
+        Term intersectionBC = slv.mkTerm(INTERSECTION, B, C);
+        Term rhs = slv.mkTerm(UNION, intersectionAC, intersectionBC);
 
-      Term theorem = slv.mkTerm(EQUAL, lhs, rhs);
+        Term theorem = slv.mkTerm(EQUAL, lhs, rhs);
 
-      System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + ".");
-    }
+        System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + ".");
+      }
 
-    // Verify emptset is a subset of any set
-    {
-      Term A = slv.mkConst(set, "A");
-      Term emptyset = slv.mkEmptySet(set);
+      // Verify emptset is a subset of any set
+      {
+        Term A = slv.mkConst(set, "A");
+        Term emptyset = slv.mkEmptySet(set);
 
-      Term theorem = slv.mkTerm(SUBSET, emptyset, A);
+        Term theorem = slv.mkTerm(SUBSET, emptyset, A);
 
-      System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + ".");
-    }
+        System.out.println("cvc5 reports: " + theorem + " is " + slv.checkEntailed(theorem) + ".");
+      }
 
-    // Find me an element in {1, 2} intersection {2, 3}, if there is one.
-    {
-      Term one = slv.mkInteger(1);
-      Term two = slv.mkInteger(2);
-      Term three = slv.mkInteger(3);
+      // Find me an element in {1, 2} intersection {2, 3}, if there is one.
+      {
+        Term one = slv.mkInteger(1);
+        Term two = slv.mkInteger(2);
+        Term three = slv.mkInteger(3);
 
-      Term singleton_one = slv.mkTerm(SINGLETON, one);
-      Term singleton_two = slv.mkTerm(SINGLETON, two);
-      Term singleton_three = slv.mkTerm(SINGLETON, three);
-      Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two);
-      Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three);
-      Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three);
+        Term singleton_one = slv.mkTerm(SINGLETON, one);
+        Term singleton_two = slv.mkTerm(SINGLETON, two);
+        Term singleton_three = slv.mkTerm(SINGLETON, three);
+        Term one_two = slv.mkTerm(UNION, singleton_one, singleton_two);
+        Term two_three = slv.mkTerm(UNION, singleton_two, singleton_three);
+        Term intersection = slv.mkTerm(INTERSECTION, one_two, two_three);
 
-      Term x = slv.mkConst(integer, "x");
+        Term x = slv.mkConst(integer, "x");
 
-      Term e = slv.mkTerm(MEMBER, x, intersection);
+        Term e = slv.mkTerm(MEMBER, x, intersection);
 
-      Result result = slv.checkSatAssuming(e);
-      System.out.println("cvc5 reports: " + e + " is " + result + ".");
+        Result result = slv.checkSatAssuming(e);
+        System.out.println("cvc5 reports: " + e + " is " + result + ".");
 
-      if (result.isSat())
-      {
-        System.out.println("For instance, " + slv.getValue(x) + " is a member.");
+        if (result.isSat())
+        {
+          System.out.println("For instance, " + slv.getValue(x) + " is a member.");
+        }
       }
     }
   }
-}
\ No newline at end of file
+}
diff --git a/examples/api/java/Statistics.java b/examples/api/java/Statistics.java
index e524eb3e3..751dda947 100644
--- a/examples/api/java/Statistics.java
+++ b/examples/api/java/Statistics.java
@@ -23,43 +23,45 @@ public class Statistics
 {
   public static void main(String[] args)
   {
-    Solver solver = getSolver();
-    // Get the statistics from the `Solver` and iterate over them. The
-    // `Statistics` class implements the `Iterable<Pair<String, Stat>>` interface.
-    io.github.cvc5.api.Statistics stats = solver.getStatistics();
-    // short version
-    System.out.println("Short version:");
-    System.out.println(stats);
+    try (Solver solver = new Solver())
+    {
+      // Get the statistics from the `Solver` and iterate over them. The
+      // `Statistics` class implements the `Iterable<Pair<String, Stat>>` interface.
+      io.github.cvc5.api.Statistics stats = solver.getStatistics();
+      // short version
+      System.out.println("Short version:");
+      System.out.println(stats);
 
-    System.out.println("-------------------------------------------------------");
+      System.out.println("-------------------------------------------------------");
 
-    System.out.println("Long version:");
+      System.out.println("Long version:");
 
-    // long version
-    for (Pair<String, Stat> pair : stats)
-    {
-      Stat stat = pair.second;
-      if (stat.isInt())
-      {
-        System.out.println(pair.first + " = " + stat.getInt());
-      }
-      else if (stat.isDouble())
-      {
-        System.out.println(pair.first + " = " + stat.getDouble());
-      }
-      else if (stat.isString())
-      {
-        System.out.println(pair.first + " = " + stat.getString());
-      }
-      else if (stat.isHistogram())
+      // long version
+      for (Pair<String, Stat> pair : stats)
       {
-        System.out.println("-------------------------------------------------------");
-        System.out.println(pair.first + " : Map");
-        for (Map.Entry<String, Long> entry : stat.getHistogram().entrySet())
+        Stat stat = pair.second;
+        if (stat.isInt())
+        {
+          System.out.println(pair.first + " = " + stat.getInt());
+        }
+        else if (stat.isDouble())
+        {
+          System.out.println(pair.first + " = " + stat.getDouble());
+        }
+        else if (stat.isString())
+        {
+          System.out.println(pair.first + " = " + stat.getString());
+        }
+        else if (stat.isHistogram())
         {
-          System.out.println(entry.getKey() + " = " + entry.getValue());
+          System.out.println("-------------------------------------------------------");
+          System.out.println(pair.first + " : Map");
+          for (Map.Entry<String, Long> entry : stat.getHistogram().entrySet())
+          {
+            System.out.println(entry.getKey() + " = " + entry.getValue());
+          }
+          System.out.println("-------------------------------------------------------");
         }
-        System.out.println("-------------------------------------------------------");
       }
     }
   }
diff --git a/examples/api/java/Strings.java b/examples/api/java/Strings.java
index 6cc152159..28487b852 100644
--- a/examples/api/java/Strings.java
+++ b/examples/api/java/Strings.java
@@ -21,71 +21,73 @@ public class Strings
 {
   public static void main(String args[]) throws CVC5ApiException
   {
-    Solver slv = new Solver();
-
-    // Set the logic
-    slv.setLogic("QF_SLIA");
-    // Produce models
-    slv.setOption("produce-models", "true");
-    // The option strings-exp is needed
-    slv.setOption("strings-exp", "true");
-    // Set output language to SMTLIB2
-    slv.setOption("output-language", "smt2");
+    try (Solver slv = new Solver())
+    {
+      // Set the logic
+      slv.setLogic("QF_SLIA");
+      // Produce models
+      slv.setOption("produce-models", "true");
+      // The option strings-exp is needed
+      slv.setOption("strings-exp", "true");
+      // Set output language to SMTLIB2
+      slv.setOption("output-language", "smt2");
 
-    // String type
-    Sort string = slv.getStringSort();
+      // String type
+      Sort string = slv.getStringSort();
 
-    // std::string
-    String str_ab = "ab";
-    // String constants
-    Term ab = slv.mkString(str_ab);
-    Term abc = slv.mkString("abc");
-    // String variables
-    Term x = slv.mkConst(string, "x");
-    Term y = slv.mkConst(string, "y");
-    Term z = slv.mkConst(string, "z");
+      // std::string
+      String str_ab = "ab";
+      // String constants
+      Term ab = slv.mkString(str_ab);
+      Term abc = slv.mkString("abc");
+      // String variables
+      Term x = slv.mkConst(string, "x");
+      Term y = slv.mkConst(string, "y");
+      Term z = slv.mkConst(string, "z");
 
-    // String concatenation: x.ab.y
-    Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y);
-    // String concatenation: abc.z
-    Term rhs = slv.mkTerm(STRING_CONCAT, abc, z);
-    // x.ab.y = abc.z
-    Term formula1 = slv.mkTerm(EQUAL, lhs, rhs);
+      // String concatenation: x.ab.y
+      Term lhs = slv.mkTerm(STRING_CONCAT, x, ab, y);
+      // String concatenation: abc.z
+      Term rhs = slv.mkTerm(STRING_CONCAT, abc, z);
+      // x.ab.y = abc.z
+      Term formula1 = slv.mkTerm(EQUAL, lhs, rhs);
 
-    // Length of y: |y|
-    Term leny = slv.mkTerm(STRING_LENGTH, y);
-    // |y| >= 0
-    Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(0));
+      // Length of y: |y|
+      Term leny = slv.mkTerm(STRING_LENGTH, y);
+      // |y| >= 0
+      Term formula2 = slv.mkTerm(GEQ, leny, slv.mkInteger(0));
 
-    // Regular expression: (ab[c-e]*f)|g|h
-    Term r = slv.mkTerm(REGEXP_UNION,
-        slv.mkTerm(REGEXP_CONCAT,
-            slv.mkTerm(STRING_TO_REGEXP, slv.mkString("ab")),
-            slv.mkTerm(REGEXP_STAR, slv.mkTerm(REGEXP_RANGE, slv.mkString("c"), slv.mkString("e"))),
-            slv.mkTerm(STRING_TO_REGEXP, slv.mkString("f"))),
-        slv.mkTerm(STRING_TO_REGEXP, slv.mkString("g")),
-        slv.mkTerm(STRING_TO_REGEXP, slv.mkString("h")));
+      // Regular expression: (ab[c-e]*f)|g|h
+      Term r = slv.mkTerm(REGEXP_UNION,
+          slv.mkTerm(REGEXP_CONCAT,
+              slv.mkTerm(STRING_TO_REGEXP, slv.mkString("ab")),
+              slv.mkTerm(
+                  REGEXP_STAR, slv.mkTerm(REGEXP_RANGE, slv.mkString("c"), slv.mkString("e"))),
+              slv.mkTerm(STRING_TO_REGEXP, slv.mkString("f"))),
+          slv.mkTerm(STRING_TO_REGEXP, slv.mkString("g")),
+          slv.mkTerm(STRING_TO_REGEXP, slv.mkString("h")));
 
-    // String variables
-    Term s1 = slv.mkConst(string, "s1");
-    Term s2 = slv.mkConst(string, "s2");
-    // String concatenation: s1.s2
-    Term s = slv.mkTerm(STRING_CONCAT, s1, s2);
+      // String variables
+      Term s1 = slv.mkConst(string, "s1");
+      Term s2 = slv.mkConst(string, "s2");
+      // String concatenation: s1.s2
+      Term s = slv.mkTerm(STRING_CONCAT, s1, s2);
 
-    // s1.s2 in (ab[c-e]*f)|g|h
-    Term formula3 = slv.mkTerm(STRING_IN_REGEXP, s, r);
+      // s1.s2 in (ab[c-e]*f)|g|h
+      Term formula3 = slv.mkTerm(STRING_IN_REGEXP, s, r);
 
-    // Make a query
-    Term q = slv.mkTerm(AND, formula1, formula2, formula3);
+      // Make a query
+      Term q = slv.mkTerm(AND, formula1, formula2, formula3);
 
-    // check sat
-    Result result = slv.checkSatAssuming(q);
-    System.out.println("cvc5 reports: " + q + " is " + result + ".");
+      // check sat
+      Result result = slv.checkSatAssuming(q);
+      System.out.println("cvc5 reports: " + q + " is " + result + ".");
 
-    if (result.isSat())
-    {
-      System.out.println("  x  = " + slv.getValue(x));
-      System.out.println("  s1.s2 = " + slv.getValue(s));
+      if (result.isSat())
+      {
+        System.out.println("  x  = " + slv.getValue(x));
+        System.out.println("  s1.s2 = " + slv.getValue(s));
+      }
     }
   }
-}
\ No newline at end of file
+}
diff --git a/examples/api/java/SygusFun.java b/examples/api/java/SygusFun.java
index 8b96dff50..bc1d7e6b1 100644
--- a/examples/api/java/SygusFun.java
+++ b/examples/api/java/SygusFun.java
@@ -56,84 +56,85 @@ public class SygusFun
 {
   public static void main(String args[]) throws CVC5ApiException
   {
-    Solver slv = new Solver();
-
-    // required options
-    slv.setOption("lang", "sygus2");
-    slv.setOption("incremental", "false");
-
-    // set the logic
-    slv.setLogic("LIA");
-
-    Sort integer = slv.getIntegerSort();
-    Sort bool = slv.getBooleanSort();
-
-    // declare input variables for the functions-to-synthesize
-    Term x = slv.mkVar(integer, "x");
-    Term y = slv.mkVar(integer, "y");
-
-    // declare the grammar non-terminals
-    Term start = slv.mkVar(integer, "Start");
-    Term start_bool = slv.mkVar(bool, "StartBool");
-
-    // define the rules
-    Term zero = slv.mkInteger(0);
-    Term one = slv.mkInteger(1);
-
-    Term plus = slv.mkTerm(PLUS, start, start);
-    Term minus = slv.mkTerm(MINUS, start, start);
-    Term ite = slv.mkTerm(ITE, start_bool, start, start);
-
-    Term And = slv.mkTerm(AND, start_bool, start_bool);
-    Term Not = slv.mkTerm(NOT, start_bool);
-    Term leq = slv.mkTerm(LEQ, start, start);
-
-    // create the grammar object
-    Grammar g = slv.mkSygusGrammar(new Term[] {x, y}, new Term[] {start, start_bool});
-
-    // bind each non-terminal to its rules
-    g.addRules(start, new Term[] {zero, one, x, y, plus, minus, ite});
-    g.addRules(start_bool, new Term[] {And, Not, leq});
-
-    // declare the functions-to-synthesize. Optionally, provide the grammar
-    // constraints
-    Term max = slv.synthFun("max", new Term[] {x, y}, integer, g);
-    Term min = slv.synthFun("min", new Term[] {x, y}, integer);
-
-    // declare universal variables.
-    Term varX = slv.mkSygusVar(integer, "x");
-    Term varY = slv.mkSygusVar(integer, "y");
-
-    Term max_x_y = slv.mkTerm(APPLY_UF, max, varX, varY);
-    Term min_x_y = slv.mkTerm(APPLY_UF, min, varX, varY);
-
-    // add semantic constraints
-    // (constraint (>= (max x y) x))
-    slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varX));
-
-    // (constraint (>= (max x y) y))
-    slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varY));
-
-    // (constraint (or (= x (max x y))
-    //                 (= y (max x y))))
-    slv.addSygusConstraint(
-        slv.mkTerm(OR, slv.mkTerm(EQUAL, max_x_y, varX), slv.mkTerm(EQUAL, max_x_y, varY)));
-
-    // (constraint (= (+ (max x y) (min x y))
-    //                (+ x y)))
-    slv.addSygusConstraint(
-        slv.mkTerm(EQUAL, slv.mkTerm(PLUS, max_x_y, min_x_y), slv.mkTerm(PLUS, varX, varY)));
-
-    // print solutions if available
-    if (slv.checkSynth().isUnsat())
+    try (Solver slv = new Solver())
     {
-      // Output should be equivalent to:
-      // (
-      //   (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
-      //   (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
-      // )
-      Term[] terms = new Term[] {max, min};
-      Utils.printSynthSolutions(terms, slv.getSynthSolutions(terms));
+      // required options
+      slv.setOption("lang", "sygus2");
+      slv.setOption("incremental", "false");
+
+      // set the logic
+      slv.setLogic("LIA");
+
+      Sort integer = slv.getIntegerSort();
+      Sort bool = slv.getBooleanSort();
+
+      // declare input variables for the functions-to-synthesize
+      Term x = slv.mkVar(integer, "x");
+      Term y = slv.mkVar(integer, "y");
+
+      // declare the grammar non-terminals
+      Term start = slv.mkVar(integer, "Start");
+      Term start_bool = slv.mkVar(bool, "StartBool");
+
+      // define the rules
+      Term zero = slv.mkInteger(0);
+      Term one = slv.mkInteger(1);
+
+      Term plus = slv.mkTerm(PLUS, start, start);
+      Term minus = slv.mkTerm(MINUS, start, start);
+      Term ite = slv.mkTerm(ITE, start_bool, start, start);
+
+      Term And = slv.mkTerm(AND, start_bool, start_bool);
+      Term Not = slv.mkTerm(NOT, start_bool);
+      Term leq = slv.mkTerm(LEQ, start, start);
+
+      // create the grammar object
+      Grammar g = slv.mkSygusGrammar(new Term[] {x, y}, new Term[] {start, start_bool});
+
+      // bind each non-terminal to its rules
+      g.addRules(start, new Term[] {zero, one, x, y, plus, minus, ite});
+      g.addRules(start_bool, new Term[] {And, Not, leq});
+
+      // declare the functions-to-synthesize. Optionally, provide the grammar
+      // constraints
+      Term max = slv.synthFun("max", new Term[] {x, y}, integer, g);
+      Term min = slv.synthFun("min", new Term[] {x, y}, integer);
+
+      // declare universal variables.
+      Term varX = slv.mkSygusVar(integer, "x");
+      Term varY = slv.mkSygusVar(integer, "y");
+
+      Term max_x_y = slv.mkTerm(APPLY_UF, max, varX, varY);
+      Term min_x_y = slv.mkTerm(APPLY_UF, min, varX, varY);
+
+      // add semantic constraints
+      // (constraint (>= (max x y) x))
+      slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varX));
+
+      // (constraint (>= (max x y) y))
+      slv.addSygusConstraint(slv.mkTerm(GEQ, max_x_y, varY));
+
+      // (constraint (or (= x (max x y))
+      //                 (= y (max x y))))
+      slv.addSygusConstraint(
+          slv.mkTerm(OR, slv.mkTerm(EQUAL, max_x_y, varX), slv.mkTerm(EQUAL, max_x_y, varY)));
+
+      // (constraint (= (+ (max x y) (min x y))
+      //                (+ x y)))
+      slv.addSygusConstraint(
+          slv.mkTerm(EQUAL, slv.mkTerm(PLUS, max_x_y, min_x_y), slv.mkTerm(PLUS, varX, varY)));
+
+      // print solutions if available
+      if (slv.checkSynth().isUnsat())
+      {
+        // Output should be equivalent to:
+        // (
+        //   (define-fun max ((x Int) (y Int)) Int (ite (<= x y) y x))
+        //   (define-fun min ((x Int) (y Int)) Int (ite (<= x y) x y))
+        // )
+        Term[] terms = new Term[] {max, min};
+        Utils.printSynthSolutions(terms, slv.getSynthSolutions(terms));
+      }
     }
   }
-}
\ No newline at end of file
+}
diff --git a/examples/api/java/SygusGrammar.java b/examples/api/java/SygusGrammar.java
index fb079d49f..230229fdd 100644
--- a/examples/api/java/SygusGrammar.java
+++ b/examples/api/java/SygusGrammar.java
@@ -53,77 +53,78 @@ public class SygusGrammar
 {
   public static void main(String args[]) throws CVC5ApiException
   {
-    Solver slv = new Solver();
-
-    // required options
-    slv.setOption("lang", "sygus2");
-    slv.setOption("incremental", "false");
+    try (Solver slv = new Solver())
+    {
+      // required options
+      slv.setOption("lang", "sygus2");
+      slv.setOption("incremental", "false");
 
-    // set the logic
-    slv.setLogic("LIA");
+      // set the logic
+      slv.setLogic("LIA");
 
-    Sort integer = slv.getIntegerSort();
-    Sort bool = slv.getBooleanSort();
+      Sort integer = slv.getIntegerSort();
+      Sort bool = slv.getBooleanSort();
 
-    // declare input variable for the function-to-synthesize
-    Term x = slv.mkVar(integer, "x");
+      // declare input variable for the function-to-synthesize
+      Term x = slv.mkVar(integer, "x");
 
-    // declare the grammar non-terminal
-    Term start = slv.mkVar(integer, "Start");
+      // declare the grammar non-terminal
+      Term start = slv.mkVar(integer, "Start");
 
-    // define the rules
-    Term zero = slv.mkInteger(0);
-    Term neg_x = slv.mkTerm(UMINUS, x);
-    Term plus = slv.mkTerm(PLUS, x, start);
+      // define the rules
+      Term zero = slv.mkInteger(0);
+      Term neg_x = slv.mkTerm(UMINUS, x);
+      Term plus = slv.mkTerm(PLUS, x, start);
 
-    // create the grammar object
-    Grammar g1 = slv.mkSygusGrammar(new Term[] {x}, new Term[] {start});
+      // create the grammar object
+      Grammar g1 = slv.mkSygusGrammar(new Term[] {x}, new Term[] {start});
 
-    // bind each non-terminal to its rules
-    g1.addRules(start, new Term[] {neg_x, plus});
+      // bind each non-terminal to its rules
+      g1.addRules(start, new Term[] {neg_x, plus});
 
-    // copy the first grammar with all of its non-terminals and their rules
-    Grammar g2 = new Grammar(g1);
-    Grammar g3 = new Grammar(g1);
+      // copy the first grammar with all of its non-terminals and their rules
+      Grammar g2 = new Grammar(g1);
+      Grammar g3 = new Grammar(g1);
 
-    // add parameters as rules for the start symbol. Similar to "(Variable Int)"
-    g2.addAnyVariable(start);
+      // add parameters as rules for the start symbol. Similar to "(Variable Int)"
+      g2.addAnyVariable(start);
 
-    // declare the functions-to-synthesize
-    Term id1 = slv.synthFun("id1", new Term[] {x}, integer, g1);
-    Term id2 = slv.synthFun("id2", new Term[] {x}, integer, g2);
+      // declare the functions-to-synthesize
+      Term id1 = slv.synthFun("id1", new Term[] {x}, integer, g1);
+      Term id2 = slv.synthFun("id2", new Term[] {x}, integer, g2);
 
-    g3.addRule(start, zero);
+      g3.addRule(start, zero);
 
-    Term id3 = slv.synthFun("id3", new Term[] {x}, integer, g3);
+      Term id3 = slv.synthFun("id3", new Term[] {x}, integer, g3);
 
-    // g1 is reusable as long as it remains unmodified after first use
-    Term id4 = slv.synthFun("id4", new Term[] {x}, integer, g1);
+      // g1 is reusable as long as it remains unmodified after first use
+      Term id4 = slv.synthFun("id4", new Term[] {x}, integer, g1);
 
-    // declare universal variables.
-    Term varX = slv.mkSygusVar(integer, "x");
+      // declare universal variables.
+      Term varX = slv.mkSygusVar(integer, "x");
 
-    Term id1_x = slv.mkTerm(APPLY_UF, id1, varX);
-    Term id2_x = slv.mkTerm(APPLY_UF, id2, varX);
-    Term id3_x = slv.mkTerm(APPLY_UF, id3, varX);
-    Term id4_x = slv.mkTerm(APPLY_UF, id4, varX);
+      Term id1_x = slv.mkTerm(APPLY_UF, id1, varX);
+      Term id2_x = slv.mkTerm(APPLY_UF, id2, varX);
+      Term id3_x = slv.mkTerm(APPLY_UF, id3, varX);
+      Term id4_x = slv.mkTerm(APPLY_UF, id4, varX);
 
-    // add semantic constraints
-    // (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x))
-    slv.addSygusConstraint(slv.mkTerm(EQUAL, new Term[] {id1_x, id2_x, id3_x, id4_x, varX}));
+      // add semantic constraints
+      // (constraint (= (id1 x) (id2 x) (id3 x) (id4 x) x))
+      slv.addSygusConstraint(slv.mkTerm(EQUAL, new Term[] {id1_x, id2_x, id3_x, id4_x, varX}));
 
-    // print solutions if available
-    if (slv.checkSynth().isUnsat())
-    {
-      // Output should be equivalent to:
-      // (
-      //   (define-fun id1 ((x Int)) Int (+ x (+ x (- x))))
-      //   (define-fun id2 ((x Int)) Int x)
-      //   (define-fun id3 ((x Int)) Int (+ x 0))
-      //   (define-fun id4 ((x Int)) Int (+ x (+ x (- x))))
-      // )
-      Term[] terms = new Term[] {id1, id2, id3, id4};
-      Utils.printSynthSolutions(terms, slv.getSynthSolutions(terms));
+      // print solutions if available
+      if (slv.checkSynth().isUnsat())
+      {
+        // Output should be equivalent to:
+        // (
+        //   (define-fun id1 ((x Int)) Int (+ x (+ x (- x))))
+        //   (define-fun id2 ((x Int)) Int x)
+        //   (define-fun id3 ((x Int)) Int (+ x 0))
+        //   (define-fun id4 ((x Int)) Int (+ x (+ x (- x))))
+        // )
+        Term[] terms = new Term[] {id1, id2, id3, id4};
+        Utils.printSynthSolutions(terms, slv.getSynthSolutions(terms));
+      }
     }
   }
-}
\ No newline at end of file
+}
diff --git a/examples/api/java/SygusInv.java b/examples/api/java/SygusInv.java
index 6c66c910b..be1311318 100644
--- a/examples/api/java/SygusInv.java
+++ b/examples/api/java/SygusInv.java
@@ -44,51 +44,52 @@ public class SygusInv
 {
   public static void main(String args[]) throws CVC5ApiException
   {
-    Solver slv = new Solver();
-
-    // required options
-    slv.setOption("lang", "sygus2");
-    slv.setOption("incremental", "false");
+    try (Solver slv = new Solver())
+    {
+      // required options
+      slv.setOption("lang", "sygus2");
+      slv.setOption("incremental", "false");
 
-    // set the logic
-    slv.setLogic("LIA");
+      // set the logic
+      slv.setLogic("LIA");
 
-    Sort integer = slv.getIntegerSort();
-    Sort bool = slv.getBooleanSort();
+      Sort integer = slv.getIntegerSort();
+      Sort bool = slv.getBooleanSort();
 
-    Term zero = slv.mkInteger(0);
-    Term one = slv.mkInteger(1);
-    Term ten = slv.mkInteger(10);
+      Term zero = slv.mkInteger(0);
+      Term one = slv.mkInteger(1);
+      Term ten = slv.mkInteger(10);
 
-    // declare input variables for functions
-    Term x = slv.mkVar(integer, "x");
-    Term xp = slv.mkVar(integer, "xp");
+      // declare input variables for functions
+      Term x = slv.mkVar(integer, "x");
+      Term xp = slv.mkVar(integer, "xp");
 
-    // (ite (< x 10) (= xp (+ x 1)) (= xp x))
-    Term ite = slv.mkTerm(ITE,
-        slv.mkTerm(LT, x, ten),
-        slv.mkTerm(EQUAL, xp, slv.mkTerm(PLUS, x, one)),
-        slv.mkTerm(EQUAL, xp, x));
+      // (ite (< x 10) (= xp (+ x 1)) (= xp x))
+      Term ite = slv.mkTerm(ITE,
+          slv.mkTerm(LT, x, ten),
+          slv.mkTerm(EQUAL, xp, slv.mkTerm(PLUS, x, one)),
+          slv.mkTerm(EQUAL, xp, x));
 
-    // define the pre-conditions, transition relations, and post-conditions
-    Term pre_f = slv.defineFun("pre-f", new Term[] {x}, bool, slv.mkTerm(EQUAL, x, zero));
-    Term trans_f = slv.defineFun("trans-f", new Term[] {x, xp}, bool, ite);
-    Term post_f = slv.defineFun("post-f", new Term[] {x}, bool, slv.mkTerm(LEQ, x, ten));
+      // define the pre-conditions, transition relations, and post-conditions
+      Term pre_f = slv.defineFun("pre-f", new Term[] {x}, bool, slv.mkTerm(EQUAL, x, zero));
+      Term trans_f = slv.defineFun("trans-f", new Term[] {x, xp}, bool, ite);
+      Term post_f = slv.defineFun("post-f", new Term[] {x}, bool, slv.mkTerm(LEQ, x, ten));
 
-    // declare the invariant-to-synthesize
-    Term inv_f = slv.synthInv("inv-f", new Term[] {x});
+      // declare the invariant-to-synthesize
+      Term inv_f = slv.synthInv("inv-f", new Term[] {x});
 
-    slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f);
+      slv.addSygusInvConstraint(inv_f, pre_f, trans_f, post_f);
 
-    // print solutions if available
-    if (slv.checkSynth().isUnsat())
-    {
-      // Output should be equivalent to:
-      // (
-      //   (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
-      // )
-      Term[] terms = new Term[] {inv_f};
-      Utils.printSynthSolutions(terms, slv.getSynthSolutions(terms));
+      // print solutions if available
+      if (slv.checkSynth().isUnsat())
+      {
+        // Output should be equivalent to:
+        // (
+        //   (define-fun inv-f ((x Int)) Bool (not (>= x 11)))
+        // )
+        Term[] terms = new Term[] {inv_f};
+        Utils.printSynthSolutions(terms, slv.getSynthSolutions(terms));
+      }
     }
   }
-}
\ No newline at end of file
+}
diff --git a/examples/api/java/Transcendentals.java b/examples/api/java/Transcendentals.java
index 026f9b826..a44a1e4c0 100644
--- a/examples/api/java/Transcendentals.java
+++ b/examples/api/java/Transcendentals.java
@@ -21,32 +21,34 @@ public class Transcendentals
 {
   public static void main(String args[]) throws CVC5ApiException
   {
-    Solver slv = new Solver();
-    slv.setLogic("QF_NRAT");
-
-    Sort real = slv.getRealSort();
-
-    // Variables
-    Term x = slv.mkConst(real, "x");
-    Term y = slv.mkConst(real, "y");
-
-    // Helper terms
-    Term two = slv.mkReal(2);
-    Term pi = slv.mkPi();
-    Term twopi = slv.mkTerm(MULT, two, pi);
-    Term ysq = slv.mkTerm(MULT, y, y);
-    Term sinx = slv.mkTerm(SINE, x);
-
-    // Formulas
-    Term x_gt_pi = slv.mkTerm(GT, x, pi);
-    Term x_lt_tpi = slv.mkTerm(LT, x, twopi);
-    Term ysq_lt_sinx = slv.mkTerm(LT, ysq, sinx);
-
-    slv.assertFormula(x_gt_pi);
-    slv.assertFormula(x_lt_tpi);
-    slv.assertFormula(ysq_lt_sinx);
-
-    System.out.println("cvc5 should report UNSAT.");
-    System.out.println("Result from cvc5 is: " + slv.checkSat());
+    try (Solver slv = new Solver())
+    {
+      slv.setLogic("QF_NRAT");
+
+      Sort real = slv.getRealSort();
+
+      // Variables
+      Term x = slv.mkConst(real, "x");
+      Term y = slv.mkConst(real, "y");
+
+      // Helper terms
+      Term two = slv.mkReal(2);
+      Term pi = slv.mkPi();
+      Term twopi = slv.mkTerm(MULT, two, pi);
+      Term ysq = slv.mkTerm(MULT, y, y);
+      Term sinx = slv.mkTerm(SINE, x);
+
+      // Formulas
+      Term x_gt_pi = slv.mkTerm(GT, x, pi);
+      Term x_lt_tpi = slv.mkTerm(LT, x, twopi);
+      Term ysq_lt_sinx = slv.mkTerm(LT, ysq, sinx);
+
+      slv.assertFormula(x_gt_pi);
+      slv.assertFormula(x_lt_tpi);
+      slv.assertFormula(ysq_lt_sinx);
+
+      System.out.println("cvc5 should report UNSAT.");
+      System.out.println("Result from cvc5 is: " + slv.checkSat());
+    }
   }
-}
\ No newline at end of file
+}
diff --git a/examples/api/java/UnsatCores.java b/examples/api/java/UnsatCores.java
index cefa90290..feec35dbd 100644
--- a/examples/api/java/UnsatCores.java
+++ b/examples/api/java/UnsatCores.java
@@ -20,33 +20,34 @@ public class UnsatCores
 {
   public static void main(String[] args) throws CVC5ApiException
   {
-    Solver solver = new Solver();
-
-    // Enable the production of unsat cores
-    solver.setOption("produce-unsat-cores", "true");
+    try (Solver solver = new Solver())
+    {
+      // Enable the production of unsat cores
+      solver.setOption("produce-unsat-cores", "true");
 
-    Sort boolSort = solver.getBooleanSort();
-    Term a = solver.mkConst(boolSort, "A");
-    Term b = solver.mkConst(boolSort, "B");
+      Sort boolSort = solver.getBooleanSort();
+      Term a = solver.mkConst(boolSort, "A");
+      Term b = solver.mkConst(boolSort, "B");
 
-    // A ^ B
-    solver.assertFormula(solver.mkTerm(Kind.AND, a, b));
-    // ~(A v B)
-    solver.assertFormula(solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.OR, a, b)));
+      // A ^ B
+      solver.assertFormula(solver.mkTerm(Kind.AND, a, b));
+      // ~(A v B)
+      solver.assertFormula(solver.mkTerm(Kind.NOT, solver.mkTerm(Kind.OR, a, b)));
 
-    Result res = solver.checkSat(); // result is unsat
+      Result res = solver.checkSat(); // result is unsat
 
-    // Retrieve the unsat core
-    Term[] unsatCore = solver.getUnsatCore();
+      // Retrieve the unsat core
+      Term[] unsatCore = solver.getUnsatCore();
 
-    // Print the unsat core
-    System.out.println("Unsat Core: " + Arrays.asList(unsatCore));
+      // Print the unsat core
+      System.out.println("Unsat Core: " + Arrays.asList(unsatCore));
 
-    // Iterate over expressions in the unsat core.
-    System.out.println("--- Unsat Core ---");
-    for (Term e : unsatCore)
-    {
-      System.out.println(e);
+      // Iterate over expressions in the unsat core.
+      System.out.println("--- Unsat Core ---");
+      for (Term e : unsatCore)
+      {
+        System.out.println(e);
+      }
     }
   }
 }
diff --git a/src/api/java/io/github/cvc5/api/AbstractPointer.java b/src/api/java/io/github/cvc5/api/AbstractPointer.java
index 092e33d43..c627dcf84 100644
--- a/src/api/java/io/github/cvc5/api/AbstractPointer.java
+++ b/src/api/java/io/github/cvc5/api/AbstractPointer.java
@@ -18,13 +18,24 @@ package io.github.cvc5.api;
 abstract class AbstractPointer implements IPointer
 {
   protected final Solver solver;
-  protected final long pointer;
+  protected long pointer;
 
   public long getPointer()
   {
     return pointer;
   }
 
+  protected abstract void deletePointer(long pointer);
+
+  void deletePointer()
+  {
+    if (pointer != 0)
+    {
+      deletePointer(pointer);
+    }
+    pointer = 0;
+  }
+
   public Solver getSolver()
   {
     return solver;
@@ -41,5 +52,6 @@ abstract class AbstractPointer implements IPointer
   {
     this.solver = solver;
     this.pointer = pointer;
+    solver.addAbstractPointer(this);
   }
 }
diff --git a/src/api/java/io/github/cvc5/api/Datatype.java b/src/api/java/io/github/cvc5/api/Datatype.java
index c5422c215..bc33ba10b 100644
--- a/src/api/java/io/github/cvc5/api/Datatype.java
+++ b/src/api/java/io/github/cvc5/api/Datatype.java
@@ -26,18 +26,13 @@ public class Datatype extends AbstractPointer implements Iterable<DatatypeConstr
     super(solver, pointer);
   }
 
-  protected static native void deletePointer(long pointer);
+  protected native void deletePointer(long pointer);
 
   public long getPointer()
   {
     return pointer;
   }
 
-  @Override public void finalize()
-  {
-    deletePointer(pointer);
-  }
-
   // endregion
 
   /**
diff --git a/src/api/java/io/github/cvc5/api/DatatypeConstructor.java b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java
index f41acee85..5fd9d8407 100644
--- a/src/api/java/io/github/cvc5/api/DatatypeConstructor.java
+++ b/src/api/java/io/github/cvc5/api/DatatypeConstructor.java
@@ -26,18 +26,13 @@ public class DatatypeConstructor extends AbstractPointer implements Iterable<Dat
     super(solver, pointer);
   }
 
-  protected static native void deletePointer(long pointer);
+  protected native void deletePointer(long pointer);
 
   public long getPointer()
   {
     return pointer;
   }
 
-  @Override public void finalize()
-  {
-    deletePointer(pointer);
-  }
-
   // endregion
 
   /** @return the name of this Datatype constructor. */
diff --git a/src/api/java/io/github/cvc5/api/DatatypeConstructorDecl.java b/src/api/java/io/github/cvc5/api/DatatypeConstructorDecl.java
index da3fa3582..e1f5ca746 100644
--- a/src/api/java/io/github/cvc5/api/DatatypeConstructorDecl.java
+++ b/src/api/java/io/github/cvc5/api/DatatypeConstructorDecl.java
@@ -23,18 +23,13 @@ public class DatatypeConstructorDecl extends AbstractPointer
     super(solver, pointer);
   }
 
-  protected static native void deletePointer(long pointer);
+  protected native void deletePointer(long pointer);
 
   public long getPointer()
   {
     return pointer;
   }
 
-  @Override public void finalize()
-  {
-    deletePointer(pointer);
-  }
-
   // endregion
 
   /**
diff --git a/src/api/java/io/github/cvc5/api/DatatypeDecl.java b/src/api/java/io/github/cvc5/api/DatatypeDecl.java
index ad90c0987..fb8da9abd 100644
--- a/src/api/java/io/github/cvc5/api/DatatypeDecl.java
+++ b/src/api/java/io/github/cvc5/api/DatatypeDecl.java
@@ -23,18 +23,13 @@ public class DatatypeDecl extends AbstractPointer
     super(solver, pointer);
   }
 
-  protected static native void deletePointer(long pointer);
+  protected native void deletePointer(long pointer);
 
   public long getPointer()
   {
     return pointer;
   }
 
-  @Override public void finalize()
-  {
-    deletePointer(pointer);
-  }
-
   // endregion
   /**
    * Add datatype constructor declaration.
diff --git a/src/api/java/io/github/cvc5/api/DatatypeSelector.java b/src/api/java/io/github/cvc5/api/DatatypeSelector.java
index 7a0907c9d..d388e7f2b 100644
--- a/src/api/java/io/github/cvc5/api/DatatypeSelector.java
+++ b/src/api/java/io/github/cvc5/api/DatatypeSelector.java
@@ -23,18 +23,13 @@ public class DatatypeSelector extends AbstractPointer
     super(solver, pointer);
   }
 
-  protected static native void deletePointer(long pointer);
+  protected native void deletePointer(long pointer);
 
   public long getPointer()
   {
     return pointer;
   }
 
-  @Override public void finalize()
-  {
-    deletePointer(pointer);
-  }
-
   // endregion
 
   /** @return the name of this Datatype selector. */
diff --git a/src/api/java/io/github/cvc5/api/Grammar.java b/src/api/java/io/github/cvc5/api/Grammar.java
index 860bb8302..49a29670d 100644
--- a/src/api/java/io/github/cvc5/api/Grammar.java
+++ b/src/api/java/io/github/cvc5/api/Grammar.java
@@ -30,18 +30,13 @@ public class Grammar extends AbstractPointer
 
   private static native long copyGrammar(long pointer);
 
-  protected static native void deletePointer(long pointer);
+  protected native void deletePointer(long pointer);
 
   public long getPointer()
   {
     return pointer;
   }
 
-  @Override public void finalize()
-  {
-    deletePointer(pointer);
-  }
-
   // endregion
 
   /**
diff --git a/src/api/java/io/github/cvc5/api/Op.java b/src/api/java/io/github/cvc5/api/Op.java
index 86d893785..096fd559d 100644
--- a/src/api/java/io/github/cvc5/api/Op.java
+++ b/src/api/java/io/github/cvc5/api/Op.java
@@ -23,18 +23,13 @@ public class Op extends AbstractPointer
     super(solver, pointer);
   }
 
-  protected static native void deletePointer(long pointer);
+  protected native void deletePointer(long pointer);
 
   public long getPointer()
   {
     return pointer;
   }
 
-  @Override public void finalize()
-  {
-    deletePointer(pointer);
-  }
-
   // endregion
 
   /**
diff --git a/src/api/java/io/github/cvc5/api/OptionInfo.java b/src/api/java/io/github/cvc5/api/OptionInfo.java
index 76633a8a6..6f6024420 100644
--- a/src/api/java/io/github/cvc5/api/OptionInfo.java
+++ b/src/api/java/io/github/cvc5/api/OptionInfo.java
@@ -46,18 +46,13 @@ public class OptionInfo extends AbstractPointer
     this.baseInfo = getBaseInfo(pointer);
   }
 
-  protected static native void deletePointer(long pointer);
+  protected native void deletePointer(long pointer);
 
   public long getPointer()
   {
     return pointer;
   }
 
-  @Override public void finalize()
-  {
-    deletePointer(pointer);
-  }
-
   /**
    * @return a string representation of this optionInfo.
    */
diff --git a/src/api/java/io/github/cvc5/api/Result.java b/src/api/java/io/github/cvc5/api/Result.java
index 500ec7f16..3a34fbda6 100644
--- a/src/api/java/io/github/cvc5/api/Result.java
+++ b/src/api/java/io/github/cvc5/api/Result.java
@@ -26,18 +26,13 @@ public class Result extends AbstractPointer
     super(solver, pointer);
   }
 
-  protected static native void deletePointer(long pointer);
+  protected native void deletePointer(long pointer);
 
   public long getPointer()
   {
     return pointer;
   }
 
-  @Override public void finalize()
-  {
-    deletePointer(pointer);
-  }
-
   // endregion
 
   public enum UnknownExplanation {
diff --git a/src/api/java/io/github/cvc5/api/Solver.java b/src/api/java/io/github/cvc5/api/Solver.java
index c57ba48b8..6c1399d9c 100644
--- a/src/api/java/io/github/cvc5/api/Solver.java
+++ b/src/api/java/io/github/cvc5/api/Solver.java
@@ -18,9 +18,9 @@ package io.github.cvc5.api;
 import java.io.IOException;
 import java.util.*;
 
-public class Solver implements IPointer
+public class Solver implements IPointer, AutoCloseable
 {
-  private final long pointer;
+  private long pointer;
 
   public long getPointer()
   {
@@ -31,14 +31,32 @@ public class Solver implements IPointer
 
   public void deletePointer()
   {
-    deletePointer(pointer);
+    if (pointer != 0)
+    {
+      deletePointer(pointer);
+    }
+    pointer = 0;
   }
 
   private static native void deletePointer(long pointer);
 
-  @Override public void finalize()
+  // store pointers for terms, sorts, etc
+  List<AbstractPointer> abstractPointers = new ArrayList<>();
+
+  @Override public void close()
+  {
+    // delete heap memory for terms, sorts, etc
+    for (int i = abstractPointers.size() - 1; i >= 0; i--)
+    {
+      abstractPointers.get(i).deletePointer();
+    }
+    // delete the heap memory for this solver
+    deletePointer();
+  }
+
+  void addAbstractPointer(AbstractPointer abstractPointer)
   {
-    deletePointer(pointer);
+    abstractPointers.add(abstractPointer);
   }
 
   static
diff --git a/src/api/java/io/github/cvc5/api/Sort.java b/src/api/java/io/github/cvc5/api/Sort.java
index ec7091e5c..440b1ba59 100644
--- a/src/api/java/io/github/cvc5/api/Sort.java
+++ b/src/api/java/io/github/cvc5/api/Sort.java
@@ -25,18 +25,13 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
     super(solver, pointer);
   }
 
-  protected static native void deletePointer(long pointer);
+  protected native void deletePointer(long pointer);
 
   public long getPointer()
   {
     return pointer;
   }
 
-  @Override public void finalize()
-  {
-    deletePointer(pointer);
-  }
-
   // endregion
 
   /**
@@ -799,4 +794,4 @@ public class Sort extends AbstractPointer implements Comparable<Sort>
   }
 
   private native long[] getTupleSorts(long pointer);
-}
\ No newline at end of file
+}
diff --git a/src/api/java/io/github/cvc5/api/Stat.java b/src/api/java/io/github/cvc5/api/Stat.java
index c0c81c472..6bcae5322 100644
--- a/src/api/java/io/github/cvc5/api/Stat.java
+++ b/src/api/java/io/github/cvc5/api/Stat.java
@@ -34,18 +34,13 @@ public class Stat extends AbstractPointer
     super(solver, pointer);
   }
 
-  protected static native void deletePointer(long pointer);
+  protected native void deletePointer(long pointer);
 
   public long getPointer()
   {
     return pointer;
   }
 
-  @Override public void finalize()
-  {
-    deletePointer(pointer);
-  }
-
   // endregion
 
   /**
diff --git a/src/api/java/io/github/cvc5/api/Statistics.java b/src/api/java/io/github/cvc5/api/Statistics.java
index c874e483a..ad904aa1f 100644
--- a/src/api/java/io/github/cvc5/api/Statistics.java
+++ b/src/api/java/io/github/cvc5/api/Statistics.java
@@ -26,18 +26,13 @@ public class Statistics extends AbstractPointer implements Iterable<Pair<String,
     super(solver, pointer);
   }
 
-  protected static native void deletePointer(long pointer);
+  protected native void deletePointer(long pointer);
 
   public long getPointer()
   {
     return pointer;
   }
 
-  @Override public void finalize()
-  {
-    deletePointer(pointer);
-  }
-
   // endregion
 
   /**
diff --git a/src/api/java/io/github/cvc5/api/Term.java b/src/api/java/io/github/cvc5/api/Term.java
index 7a1798b65..bbed609f7 100644
--- a/src/api/java/io/github/cvc5/api/Term.java
+++ b/src/api/java/io/github/cvc5/api/Term.java
@@ -31,18 +31,13 @@ public class Term extends AbstractPointer implements Comparable<Term>, Iterable<
     super(solver, pointer);
   }
 
-  protected static native void deletePointer(long pointer);
+  protected native void deletePointer(long pointer);
 
   public long getPointer()
   {
     return pointer;
   }
 
-  @Override public void finalize()
-  {
-    deletePointer(pointer);
-  }
-
   // endregion
 
   /**
diff --git a/src/api/java/jni/datatype.cpp b/src/api/java/jni/datatype.cpp
index 5efff9f2c..3f340c93c 100644
--- a/src/api/java/jni/datatype.cpp
+++ b/src/api/java/jni/datatype.cpp
@@ -25,7 +25,7 @@ using namespace cvc5::api;
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Datatype_deletePointer(
-    JNIEnv* env, jclass, jlong pointer)
+    JNIEnv* env, jobject, jlong pointer)
 {
   delete ((Datatype*)pointer);
 }
diff --git a/src/api/java/jni/datatype_constructor.cpp b/src/api/java/jni/datatype_constructor.cpp
index 853766c3c..7fe5f21c6 100644
--- a/src/api/java/jni/datatype_constructor.cpp
+++ b/src/api/java/jni/datatype_constructor.cpp
@@ -26,7 +26,7 @@ using namespace cvc5::api;
  */
 JNIEXPORT void JNICALL
 Java_io_github_cvc5_api_DatatypeConstructor_deletePointer(JNIEnv*,
-                                                          jclass,
+                                                          jobject,
                                                           jlong pointer)
 {
   delete ((DatatypeConstructor*)pointer);
diff --git a/src/api/java/jni/datatype_constructor_decl.cpp b/src/api/java/jni/datatype_constructor_decl.cpp
index b13b75e45..75cdb7aca 100644
--- a/src/api/java/jni/datatype_constructor_decl.cpp
+++ b/src/api/java/jni/datatype_constructor_decl.cpp
@@ -26,7 +26,7 @@ using namespace cvc5::api;
  */
 JNIEXPORT void JNICALL
 Java_io_github_cvc5_api_DatatypeConstructorDecl_deletePointer(JNIEnv*,
-                                                              jclass,
+                                                              jobject,
                                                               jlong pointer)
 {
   delete ((DatatypeConstructorDecl*)pointer);
diff --git a/src/api/java/jni/datatype_decl.cpp b/src/api/java/jni/datatype_decl.cpp
index 845afac9d..1940c37e1 100644
--- a/src/api/java/jni/datatype_decl.cpp
+++ b/src/api/java/jni/datatype_decl.cpp
@@ -25,7 +25,7 @@ using namespace cvc5::api;
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_io_github_cvc5_api_DatatypeDecl_deletePointer(
-    JNIEnv*, jclass, jlong pointer)
+    JNIEnv*, jobject, jlong pointer)
 {
   delete ((DatatypeDecl*)pointer);
 }
diff --git a/src/api/java/jni/datatype_selector.cpp b/src/api/java/jni/datatype_selector.cpp
index 964eb24f5..4a3358513 100644
--- a/src/api/java/jni/datatype_selector.cpp
+++ b/src/api/java/jni/datatype_selector.cpp
@@ -25,7 +25,7 @@ using namespace cvc5::api;
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_io_github_cvc5_api_DatatypeSelector_deletePointer(
-    JNIEnv*, jclass, jlong pointer)
+    JNIEnv*, jobject, jlong pointer)
 {
   delete ((DatatypeSelector*)pointer);
 }
diff --git a/src/api/java/jni/grammar.cpp b/src/api/java/jni/grammar.cpp
index 4bafd54d6..751e5ffdd 100644
--- a/src/api/java/jni/grammar.cpp
+++ b/src/api/java/jni/grammar.cpp
@@ -40,7 +40,7 @@ Java_io_github_cvc5_api_Grammar_copyGrammar(JNIEnv* env, jclass, jlong pointer)
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL
-Java_io_github_cvc5_api_Grammar_deletePointer(JNIEnv*, jclass, jlong pointer)
+Java_io_github_cvc5_api_Grammar_deletePointer(JNIEnv*, jobject, jlong pointer)
 {
   delete reinterpret_cast<Grammar*>(pointer);
 }
diff --git a/src/api/java/jni/op.cpp b/src/api/java/jni/op.cpp
index cb6a7a728..f34444001 100644
--- a/src/api/java/jni/op.cpp
+++ b/src/api/java/jni/op.cpp
@@ -25,7 +25,7 @@ using namespace cvc5::api;
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Op_deletePointer(JNIEnv*,
-                                                                jclass,
+                                                                jobject,
                                                                 jlong pointer)
 {
   delete reinterpret_cast<Op*>(pointer);
diff --git a/src/api/java/jni/option_info.cpp b/src/api/java/jni/option_info.cpp
index 031b1bae9..da2a485e3 100644
--- a/src/api/java/jni/option_info.cpp
+++ b/src/api/java/jni/option_info.cpp
@@ -24,8 +24,8 @@ using namespace cvc5::api;
  * Method:    deletePointer
  * Signature: (J)V
  */
-JNIEXPORT void JNICALL
-Java_io_github_cvc5_api_OptionInfo_deletePointer(JNIEnv*, jclass, jlong pointer)
+JNIEXPORT void JNICALL Java_io_github_cvc5_api_OptionInfo_deletePointer(
+    JNIEnv*, jobject, jlong pointer)
 {
   delete reinterpret_cast<OptionInfo*>(pointer);
 }
diff --git a/src/api/java/jni/result.cpp b/src/api/java/jni/result.cpp
index 34b3262ca..0534f240e 100644
--- a/src/api/java/jni/result.cpp
+++ b/src/api/java/jni/result.cpp
@@ -25,7 +25,7 @@ using namespace cvc5::api;
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL
-Java_io_github_cvc5_api_Result_deletePointer(JNIEnv*, jclass, jlong pointer)
+Java_io_github_cvc5_api_Result_deletePointer(JNIEnv*, jobject, jlong pointer)
 {
   delete ((Result*)pointer);
 }
diff --git a/src/api/java/jni/solver.cpp b/src/api/java/jni/solver.cpp
index bc4d7ff43..2d775c545 100644
--- a/src/api/java/jni/solver.cpp
+++ b/src/api/java/jni/solver.cpp
@@ -1679,15 +1679,14 @@ JNIEXPORT jlong JNICALL Java_io_github_cvc5_api_Solver_declareSort(
  * Signature: (JLjava/lang/String;[JJJZ)J
  */
 JNIEXPORT jlong JNICALL
-Java_io_github_cvc5_api_Solver_defineFun__JLjava_lang_String_2_3JJJZ(
-    JNIEnv* env,
-    jobject,
-    jlong pointer,
-    jstring jSymbol,
-    jlongArray jVars,
-    jlong sortPointer,
-    jlong termPointer,
-    jboolean global)
+Java_io_github_cvc5_api_Solver_defineFun(JNIEnv* env,
+                                         jobject,
+                                         jlong pointer,
+                                         jstring jSymbol,
+                                         jlongArray jVars,
+                                         jlong sortPointer,
+                                         jlong termPointer,
+                                         jboolean global)
 {
   CVC5_JAVA_API_TRY_CATCH_BEGIN;
   Solver* solver = reinterpret_cast<Solver*>(pointer);
diff --git a/src/api/java/jni/sort.cpp b/src/api/java/jni/sort.cpp
index e5b4f06fe..2c7ee4fd0 100644
--- a/src/api/java/jni/sort.cpp
+++ b/src/api/java/jni/sort.cpp
@@ -25,7 +25,7 @@ using namespace cvc5::api;
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Sort_deletePointer(JNIEnv*,
-                                                                  jclass,
+                                                                  jobject,
                                                                   jlong pointer)
 {
   delete reinterpret_cast<Sort*>(pointer);
@@ -655,7 +655,7 @@ Java_io_github_cvc5_api_Sort_getConstructorDomainSorts(JNIEnv* env,
   std::vector<jlong> sortPointers(sorts.size());
   for (size_t i = 0; i < sorts.size(); i++)
   {
-    sortPointers[i] = reinterpret_cast<jlong> (new Sort(sorts[i]));
+    sortPointers[i] = reinterpret_cast<jlong>(new Sort(sorts[i]));
   }
   jlongArray ret = env->NewLongArray(sorts.size());
   env->SetLongArrayRegion(ret, 0, sorts.size(), sortPointers.data());
diff --git a/src/api/java/jni/stat.cpp b/src/api/java/jni/stat.cpp
index 5db362ce2..8b9efbd3f 100644
--- a/src/api/java/jni/stat.cpp
+++ b/src/api/java/jni/stat.cpp
@@ -25,7 +25,7 @@ using namespace cvc5::api;
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Stat_deletePointer(JNIEnv*,
-                                                                  jclass,
+                                                                  jobject,
                                                                   jlong pointer)
 {
   delete reinterpret_cast<Stat*>(pointer);
diff --git a/src/api/java/jni/statistics.cpp b/src/api/java/jni/statistics.cpp
index 827c3184a..dfea8bf9d 100644
--- a/src/api/java/jni/statistics.cpp
+++ b/src/api/java/jni/statistics.cpp
@@ -26,8 +26,8 @@ using namespace cvc5::api;
  * Method:    deletePointer
  * Signature: (J)V
  */
-JNIEXPORT void JNICALL
-Java_io_github_cvc5_api_Statistics_deletePointer(JNIEnv*, jclass, jlong pointer)
+JNIEXPORT void JNICALL Java_io_github_cvc5_api_Statistics_deletePointer(
+    JNIEnv*, jobject, jlong pointer)
 {
   delete reinterpret_cast<Statistics*>(pointer);
 }
diff --git a/src/api/java/jni/term.cpp b/src/api/java/jni/term.cpp
index 5c8300e17..d54b0a2b5 100644
--- a/src/api/java/jni/term.cpp
+++ b/src/api/java/jni/term.cpp
@@ -25,7 +25,7 @@ using namespace cvc5::api;
  * Signature: (J)V
  */
 JNIEXPORT void JNICALL Java_io_github_cvc5_api_Term_deletePointer(JNIEnv* env,
-                                                                  jclass,
+                                                                  jobject,
                                                                   jlong pointer)
 {
   delete reinterpret_cast<Term*>(pointer);
diff --git a/test/unit/api/java/DatatypeTest.java b/test/unit/api/java/DatatypeTest.java
index cd9d7ee73..fb23ea515 100644
--- a/test/unit/api/java/DatatypeTest.java
+++ b/test/unit/api/java/DatatypeTest.java
@@ -33,6 +33,11 @@ class DatatypeTest
     d_solver = new Solver();
   }
 
+  @AfterEach void tearDown()
+  {
+    d_solver.close();
+  }
+
   @Test void mkDatatypeSort() throws CVC5ApiException
   {
     DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
diff --git a/test/unit/api/java/GrammarTest.java b/test/unit/api/java/GrammarTest.java
index e9b0d730c..37e1b5206 100644
--- a/test/unit/api/java/GrammarTest.java
+++ b/test/unit/api/java/GrammarTest.java
@@ -32,6 +32,11 @@ class GrammarTest
     d_solver = new Solver();
   }
 
+  @AfterEach void tearDown()
+  {
+    d_solver.close();
+  }
+
   @Test void addRule()
   {
     Sort bool = d_solver.getBooleanSort();
diff --git a/test/unit/api/java/OpTest.java b/test/unit/api/java/OpTest.java
index c63157155..9b4999211 100644
--- a/test/unit/api/java/OpTest.java
+++ b/test/unit/api/java/OpTest.java
@@ -32,6 +32,11 @@ class OpTest
     d_solver = new Solver();
   }
 
+  @AfterEach void tearDown()
+  {
+    d_solver.close();
+  }
+
   @Test void getKind() throws CVC5ApiException
   {
     Op x;
diff --git a/test/unit/api/java/ResultTest.java b/test/unit/api/java/ResultTest.java
index 38e981888..59bd752ca 100644
--- a/test/unit/api/java/ResultTest.java
+++ b/test/unit/api/java/ResultTest.java
@@ -31,6 +31,11 @@ class ResultTest
     d_solver = new Solver();
   }
 
+  @AfterEach void tearDown()
+  {
+    d_solver.close();
+  }
+
   @Test void isNull()
   {
     Result res_null = d_solver.getNullResult();
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 58b8d03aa..e61022e99 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -35,6 +35,11 @@ class SolverTest
     d_solver = new Solver();
   }
 
+  @AfterEach void tearDown()
+  {
+    d_solver.close();
+  }
+
   @Test void recoverableException() throws CVC5ApiException
   {
     d_solver.setOption("produce-models", "true");
@@ -102,6 +107,7 @@ class SolverTest
 
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.mkArraySort(boolSort, boolSort));
+    slv.close();
   }
 
   @Test void mkBitVectorSort() throws CVC5ApiException
@@ -132,6 +138,7 @@ class SolverTest
 
     DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list");
     assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSort(throwsDtypeSpec));
+    slv.close();
   }
 
   @Test void mkDatatypeSorts() throws CVC5ApiException
@@ -175,6 +182,7 @@ class SolverTest
 
     assertThrows(
         CVC5ApiException.class, () -> slv.mkDatatypeSorts(Arrays.asList(udecls), unresSorts));
+    slv.close();
 
     /* Note: More tests are in datatype_api_black. */
   }
@@ -227,6 +235,7 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> slv.mkFunctionSort(sorts1, slv.getIntegerSort()));
     assertThrows(
         CVC5ApiException.class, () -> slv.mkFunctionSort(sorts2, d_solver.getIntegerSort()));
+    slv.close();
   }
 
   @Test void mkParamSort() throws CVC5ApiException
@@ -248,6 +257,7 @@ class SolverTest
     Solver slv = new Solver();
     assertThrows(
         CVC5ApiException.class, () -> slv.mkPredicateSort(new Sort[] {d_solver.getIntegerSort()}));
+    slv.close();
   }
 
   @Test void mkRecordSort() throws CVC5ApiException
@@ -263,6 +273,7 @@ class SolverTest
 
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.mkRecordSort(fields));
+    slv.close();
   }
 
   @Test void mkSetSort() throws CVC5ApiException
@@ -272,6 +283,7 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.mkSetSort(d_solver.mkBitVectorSort(4)));
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.mkSetSort(d_solver.mkBitVectorSort(4)));
+    slv.close();
   }
 
   @Test void mkBagSort() throws CVC5ApiException
@@ -281,6 +293,7 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.mkBagSort(d_solver.mkBitVectorSort(4)));
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.mkBagSort(d_solver.mkBitVectorSort(4)));
+    slv.close();
   }
 
   @Test void mkSequenceSort() throws CVC5ApiException
@@ -290,6 +303,7 @@ class SolverTest
         () -> d_solver.mkSequenceSort(d_solver.mkSequenceSort(d_solver.getIntegerSort())));
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.mkSequenceSort(d_solver.getIntegerSort()));
+    slv.close();
   }
 
   @Test void mkUninterpretedSort() throws CVC5ApiException
@@ -316,6 +330,7 @@ class SolverTest
     Solver slv = new Solver();
     assertThrows(
         CVC5ApiException.class, () -> slv.mkTupleSort(new Sort[] {d_solver.getIntegerSort()}));
+    slv.close();
   }
 
   @Test void mkBitVector() throws CVC5ApiException
@@ -374,6 +389,7 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> d_solver.mkVar(d_solver.getNullSort(), "a"));
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.mkVar(boolSort, "x"));
+    slv.close();
   }
 
   @Test void mkBoolean() throws CVC5ApiException
@@ -422,6 +438,7 @@ class SolverTest
 
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.mkFloatingPoint(3, 5, t1));
+    slv.close();
   }
 
   @Test void mkCardinalityConstraint() throws CVC5ApiException
@@ -429,13 +446,11 @@ class SolverTest
     Sort su = d_solver.mkUninterpretedSort("u");
     Sort si = d_solver.getIntegerSort();
     assertDoesNotThrow(() -> d_solver.mkCardinalityConstraint(su, 3));
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(si, 3));
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(su, 0));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(si, 3));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkCardinalityConstraint(su, 0));
     Solver slv = new Solver();
-    assertThrows(
-        CVC5ApiException.class, () -> slv.mkCardinalityConstraint(su, 3));
+    assertThrows(CVC5ApiException.class, () -> slv.mkCardinalityConstraint(su, 3));
+    slv.close();
   }
 
   @Test void mkEmptySet() throws CVC5ApiException
@@ -446,6 +461,7 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.mkEmptySet(s));
     assertThrows(CVC5ApiException.class, () -> d_solver.mkEmptySet(d_solver.getBooleanSort()));
     assertThrows(CVC5ApiException.class, () -> slv.mkEmptySet(s));
+    slv.close();
   }
 
   @Test void mkEmptyBag() throws CVC5ApiException
@@ -457,6 +473,7 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> d_solver.mkEmptyBag(d_solver.getBooleanSort()));
 
     assertThrows(CVC5ApiException.class, () -> slv.mkEmptyBag(s));
+    slv.close();
   }
 
   @Test void mkEmptySequence() throws CVC5ApiException
@@ -466,6 +483,7 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.mkEmptySequence(s));
     assertDoesNotThrow(() -> d_solver.mkEmptySequence(d_solver.getBooleanSort()));
     assertThrows(CVC5ApiException.class, () -> slv.mkEmptySequence(s));
+    slv.close();
   }
 
   @Test void mkFalse() throws CVC5ApiException
@@ -639,6 +657,7 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> d_solver.mkSepNil(d_solver.getNullSort()));
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.mkSepNil(d_solver.getIntegerSort()));
+    slv.close();
   }
 
   @Test void mkString()
@@ -704,6 +723,7 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(EQUAL, v2));
     assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(EQUAL, v3));
     assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(DISTINCT, v6));
+    slv.close();
   }
 
   @Test void mkTermFromOp() throws CVC5ApiException
@@ -804,6 +824,7 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, v2));
     assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, v3));
     assertThrows(CVC5ApiException.class, () -> slv.mkTerm(opterm2, v4));
+    slv.close();
   }
 
   @Test void mkTrue()
@@ -844,6 +865,7 @@ class SolverTest
         ()
             -> slv.mkTuple(new Sort[] {slv.mkBitVectorSort(3)},
                 new Term[] {d_solver.mkBitVector(3, "101", 2)}));
+    slv.close();
   }
 
   @Test void mkUniverseSet()
@@ -852,6 +874,7 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> d_solver.mkUniverseSet(d_solver.getNullSort()));
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.mkUniverseSet(d_solver.getBooleanSort()));
+    slv.close();
   }
 
   @Test void mkConst()
@@ -870,6 +893,7 @@ class SolverTest
 
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.mkConst(boolSort));
+    slv.close();
   }
 
   @Test void mkConstArray()
@@ -892,6 +916,7 @@ class SolverTest
     Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort());
     assertThrows(CVC5ApiException.class, () -> slv.mkConstArray(arrSort2, zero));
     assertThrows(CVC5ApiException.class, () -> slv.mkConstArray(arrSort, zero2));
+    slv.close();
   }
 
   @Test void declareDatatype()
@@ -914,6 +939,7 @@ class SolverTest
 
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.declareDatatype(("a"), ctors1));
+    slv.close();
   }
 
   @Test void declareFun() throws CVC5ApiException
@@ -932,6 +958,7 @@ class SolverTest
 
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.declareFun("f1", new Sort[] {}, bvSort));
+    slv.close();
   }
 
   @Test void declareSort()
@@ -974,7 +1001,7 @@ class SolverTest
     assertThrows(
         CVC5ApiException.class, () -> d_solver.defineFun("fff", new Term[] {b1}, bvSort, v2));
     assertThrows(
-        CVC5ApiException.class, () -> d_solver.defineFun("ffff", new Term[] {b1}, funSort2, v2));
+        CVC5ApiException.class, () -> d_solver.defineFun("ffff", new Term[] {b1}, funSort, v2));
 
     // b3 has function sort, which is allowed as an argument
     assertDoesNotThrow(() -> d_solver.defineFun("fffff", new Term[] {b1, b3}, bvSort, v1));
@@ -994,6 +1021,7 @@ class SolverTest
         CVC5ApiException.class, () -> slv.defineFun("ff", new Term[] {b12, b22}, bvSort, v12));
     assertThrows(
         CVC5ApiException.class, () -> slv.defineFun("ff", new Term[] {b12, b22}, bvSort2, v1));
+    slv.close();
   }
 
   @Test void defineFunGlobal()
@@ -1074,6 +1102,7 @@ class SolverTest
 
     assertThrows(
         CVC5ApiException.class, () -> slv.defineFunRec("ff", new Term[] {b12, b22}, bvSort2, v1));
+    slv.close();
   }
 
   @Test void defineFunRecWrongLogic() throws CVC5ApiException
@@ -1201,6 +1230,7 @@ class SolverTest
         ()
             -> slv.defineFunsRec(
                 new Term[] {f12, f22}, new Term[][] {{b12, b112}, {b42}}, new Term[] {v12, v2}));
+    slv.close();
   }
 
   @Test void defineFunsRecWrongLogic() throws CVC5ApiException
@@ -1581,6 +1611,7 @@ class SolverTest
 
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.getValue(x));
+    slv.close();
   }
 
   @Test void getModelDomainElements()
@@ -1680,10 +1711,12 @@ class SolverTest
         d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
     assertThrows(
         CVC5ApiException.class, () -> d_solver.getQuantifierElimination(d_solver.getNullTerm()));
-    assertThrows(CVC5ApiException.class,
-        () -> d_solver.getQuantifierElimination(new Solver().mkBoolean(false)));
+    Solver slv = new Solver();
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.getQuantifierElimination(slv.mkBoolean(false)));
 
     assertDoesNotThrow(() -> d_solver.getQuantifierElimination(forall));
+    slv.close();
   }
 
   @Test void getQuantifierEliminationDisjunct()
@@ -1695,10 +1728,12 @@ class SolverTest
     assertThrows(CVC5ApiException.class,
         () -> d_solver.getQuantifierEliminationDisjunct(d_solver.getNullTerm()));
 
+    Solver slv = new Solver();
     assertThrows(CVC5ApiException.class,
-        () -> d_solver.getQuantifierEliminationDisjunct(new Solver().mkBoolean(false)));
+        () -> d_solver.getQuantifierEliminationDisjunct(slv.mkBoolean(false)));
 
     assertDoesNotThrow(() -> d_solver.getQuantifierEliminationDisjunct(forall));
+    slv.close();
   }
 
   @Test void declareSeparationHeap() throws CVC5ApiException
@@ -1910,8 +1945,10 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {}));
     assertThrows(CVC5ApiException.class,
         () -> d_solver.blockModelValues(new Term[] {d_solver.getNullTerm()}));
-    assertThrows(CVC5ApiException.class,
-        () -> d_solver.blockModelValues(new Term[] {new Solver().mkBoolean(false)}));
+    Solver slv = new Solver();
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {slv.mkBoolean(false)}));
+    slv.close();
   }
 
   @Test void blockModelValues2() throws CVC5ApiException
@@ -2049,6 +2086,7 @@ class SolverTest
     d_solver.defineFunsRec(new Term[] {f1, f2}, new Term[][] {{b1, b2}, {b3}}, new Term[] {v1, v2});
     assertDoesNotThrow(() -> d_solver.simplify(f1));
     assertDoesNotThrow(() -> d_solver.simplify(f2));
+    slv.close();
   }
 
   @Test void assertFormula()
@@ -2057,6 +2095,7 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> d_solver.assertFormula(d_solver.getNullTerm()));
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.assertFormula(d_solver.mkTrue()));
+    slv.close();
   }
 
   @Test void checkEntailed()
@@ -2066,6 +2105,7 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> d_solver.checkEntailed(d_solver.mkTrue()));
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue()));
+    slv.close();
   }
 
   @Test void checkEntailed1()
@@ -2081,6 +2121,7 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.checkEntailed(z));
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue()));
+    slv.close();
   }
 
   @Test void checkEntailed2()
@@ -2131,6 +2172,7 @@ class SolverTest
 
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue()));
+    slv.close();
   }
 
   @Test void checkSat() throws CVC5ApiException
@@ -2147,6 +2189,7 @@ class SolverTest
     assertThrows(CVC5ApiException.class, () -> d_solver.checkSatAssuming(d_solver.mkTrue()));
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue()));
+    slv.close();
   }
 
   @Test void checkSatAssuming1() throws CVC5ApiException
@@ -2162,6 +2205,7 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.checkSatAssuming(z));
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue()));
+    slv.close();
   }
 
   @Test void checkSatAssuming2() throws CVC5ApiException
@@ -2212,6 +2256,7 @@ class SolverTest
 
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue()));
+    slv.close();
   }
 
   @Test void setLogic() throws CVC5ApiException
@@ -2261,6 +2306,7 @@ class SolverTest
 
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.mkSygusVar(boolSort));
+    slv.close();
   }
 
   @Test void mkSygusGrammar() throws CVC5ApiException
@@ -2291,6 +2337,7 @@ class SolverTest
         () -> slv.mkSygusGrammar(new Term[] {boolVar}, new Term[] {intVar2}));
     assertThrows(CVC5ApiException.class,
         () -> slv.mkSygusGrammar(new Term[] {boolVar2}, new Term[] {intVar}));
+    slv.close();
   }
 
   @Test void synthFun() throws CVC5ApiException
@@ -2328,6 +2375,7 @@ class SolverTest
         CVC5ApiException.class, () -> slv.synthFun("", new Term[] {}, d_solver.getBooleanSort()));
     assertThrows(CVC5ApiException.class,
         () -> slv.synthFun("f1", new Term[] {x}, d_solver.getBooleanSort()));
+    slv.close();
   }
 
   @Test void synthInv() throws CVC5ApiException
@@ -2367,6 +2415,7 @@ class SolverTest
 
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.addSygusConstraint(boolTerm));
+    slv.close();
   }
 
   @Test void addSygusAssume()
@@ -2381,6 +2430,7 @@ class SolverTest
 
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.addSygusAssume(boolTerm));
+    slv.close();
   }
 
   @Test void addSygusInvConstraint() throws CVC5ApiException
@@ -2445,6 +2495,7 @@ class SolverTest
         CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv22, pre22, trans, post22));
     assertThrows(
         CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv22, pre22, trans22, post));
+    slv.close();
   }
 
   @Test void getSynthSolution() throws CVC5ApiException
@@ -2468,6 +2519,7 @@ class SolverTest
 
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.getSynthSolution(f));
+    slv.close();
   }
 
   @Test void getSynthSolutions() throws CVC5ApiException
@@ -2493,6 +2545,7 @@ class SolverTest
 
     Solver slv = new Solver();
     assertThrows(CVC5ApiException.class, () -> slv.getSynthSolutions(new Term[] {x}));
+    slv.close();
   }
 
   @Test void tupleProject() throws CVC5ApiException
diff --git a/test/unit/api/java/SortTest.java b/test/unit/api/java/SortTest.java
index 6649e5de0..977ba483e 100644
--- a/test/unit/api/java/SortTest.java
+++ b/test/unit/api/java/SortTest.java
@@ -36,6 +36,11 @@ class SortTest
     d_solver = new Solver();
   }
 
+  @AfterEach void tearDown()
+  {
+    d_solver.close();
+  }
+
   Sort create_datatype_sort() throws CVC5ApiException
   {
     DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java
index cb59849e0..94f35e97f 100644
--- a/test/unit/api/java/TermTest.java
+++ b/test/unit/api/java/TermTest.java
@@ -39,6 +39,11 @@ class TermTest
     d_solver = new Solver();
   }
 
+  @AfterEach void tearDown()
+  {
+    d_solver.close();
+  }
+
   @Test void eq()
   {
     Sort uSort = d_solver.mkUninterpretedSort("u");