Finish the Java Api (#6396)

This commit finishes the implementation of the Java API.
It also includes all java files in the build along with their unit tests.

6 files changed, 2459 insertions, 208 deletions

diff --git a/test/unit/api/java/CMakeLists.txt b/test/unit/api/java/CMakeLists.txt
index fe497ef3b..66b764ca4 100644
--- a/test/unit/api/java/CMakeLists.txt
+++ b/test/unit/api/java/CMakeLists.txt
@@ -21,7 +21,13 @@ get_target_property(CVC5_JAR_PATH cvc5jar JAR_FILE)
 
 # specify source files for junit tests
 set(java_test_src_files
+  ${CMAKE_CURRENT_SOURCE_DIR}/cvc5/DatatypeTest.java
+  ${CMAKE_CURRENT_SOURCE_DIR}/cvc5/GrammarTest.java
+  ${CMAKE_CURRENT_SOURCE_DIR}/cvc5/OpTest.java
+  ${CMAKE_CURRENT_SOURCE_DIR}/cvc5/ResultTest.java
   ${CMAKE_CURRENT_SOURCE_DIR}/cvc5/SolverTest.java
+  ${CMAKE_CURRENT_SOURCE_DIR}/cvc5/SortTest.java
+  ${CMAKE_CURRENT_SOURCE_DIR}/cvc5/TermTest.java
 )
 
 # build junit tests
@@ -59,4 +65,5 @@ add_custom_target(
 )
 
 add_dependencies(run-junit-tests build-junit-tests)
-add_dependencies(units run-junit-tests)
\ No newline at end of file
+add_dependencies(units run-junit-tests)
+add_dependencies(check run-junit-tests)
\ No newline at end of file
diff --git a/test/unit/api/java/cvc5/GrammarTest.java b/test/unit/api/java/cvc5/GrammarTest.java
index 76a80f55e..6e7c6ce5e 100644
--- a/test/unit/api/java/cvc5/GrammarTest.java
+++ b/test/unit/api/java/cvc5/GrammarTest.java
@@ -23,16 +23,17 @@ import org.junit.jupiter.api.AfterEach;
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
 
-class GrammarTest {
+class GrammarTest
+{
   private Solver d_solver;
 
-  @BeforeEach
-  void setUp() {
+  @BeforeEach void setUp()
+  {
     d_solver = new Solver();
   }
 
-  @Test
-  void addRule() {
+  @Test void addRule()
+  {
     Sort bool = d_solver.getBooleanSort();
     Sort integer = d_solver.getIntegerSort();
 
@@ -44,23 +45,19 @@ class GrammarTest {
 
     assertDoesNotThrow(() -> g.addRule(start, d_solver.mkBoolean(false)));
 
-    assertThrows(CVC5ApiException.class,
-        () -> g.addRule(nullTerm, d_solver.mkBoolean(false)));
+    assertThrows(CVC5ApiException.class, () -> g.addRule(nullTerm, d_solver.mkBoolean(false)));
     assertThrows(CVC5ApiException.class, () -> g.addRule(start, nullTerm));
-    assertThrows(CVC5ApiException.class,
-        () -> g.addRule(nts, d_solver.mkBoolean(false)));
-    assertThrows(
-        CVC5ApiException.class, () -> g.addRule(start, d_solver.mkInteger(0)));
+    assertThrows(CVC5ApiException.class, () -> g.addRule(nts, d_solver.mkBoolean(false)));
+    assertThrows(CVC5ApiException.class, () -> g.addRule(start, d_solver.mkInteger(0)));
     assertThrows(CVC5ApiException.class, () -> g.addRule(start, nts));
 
     d_solver.synthFun("f", new Term[] {}, bool, g);
 
-    assertThrows(CVC5ApiException.class,
-        () -> g.addRule(start, d_solver.mkBoolean(false)));
+    assertThrows(CVC5ApiException.class, () -> g.addRule(start, d_solver.mkBoolean(false)));
   }
 
-  @Test
-  void addRules() {
+  @Test void addRules()
+  {
     Sort bool = d_solver.getBooleanSort();
     Sort integer = d_solver.getIntegerSort();
 
@@ -70,28 +67,25 @@ class GrammarTest {
 
     Grammar g = d_solver.mkSygusGrammar(new Term[] {}, new Term[] {start});
 
-    assertDoesNotThrow(
-        () -> g.addRules(start, new Term[] {d_solver.mkBoolean(false)}));
+    assertDoesNotThrow(() -> g.addRules(start, new Term[] {d_solver.mkBoolean(false)}));
 
-    assertThrows(CVC5ApiException.class,
-        () -> g.addRules(nullTerm, new Term[] {d_solver.mkBoolean(false)}));
     assertThrows(
-        CVC5ApiException.class, () -> g.addRules(start, new Term[] {nullTerm}));
-    assertThrows(CVC5ApiException.class,
-        () -> g.addRules(nts, new Term[] {d_solver.mkBoolean(false)}));
-    assertThrows(CVC5ApiException.class,
-        () -> g.addRules(start, new Term[] {d_solver.mkInteger(0)}));
+        CVC5ApiException.class, () -> g.addRules(nullTerm, new Term[] {d_solver.mkBoolean(false)}));
+    assertThrows(CVC5ApiException.class, () -> g.addRules(start, new Term[] {nullTerm}));
+    assertThrows(
+        CVC5ApiException.class, () -> g.addRules(nts, new Term[] {d_solver.mkBoolean(false)}));
     assertThrows(
-        CVC5ApiException.class, () -> g.addRules(start, new Term[] {nts}));
+        CVC5ApiException.class, () -> g.addRules(start, new Term[] {d_solver.mkInteger(0)}));
+    assertThrows(CVC5ApiException.class, () -> g.addRules(start, new Term[] {nts}));
 
     d_solver.synthFun("f", new Term[] {}, bool, g);
 
-    assertThrows(CVC5ApiException.class,
-        () -> g.addRules(start, new Term[] {d_solver.mkBoolean(false)}));
+    assertThrows(
+        CVC5ApiException.class, () -> g.addRules(start, new Term[] {d_solver.mkBoolean(false)}));
   }
 
-  @Test
-  void addAnyConstant() {
+  @Test void addAnyConstant()
+  {
     Sort bool = d_solver.getBooleanSort();
 
     Term nullTerm = d_solver.getNullTerm();
@@ -111,8 +105,8 @@ class GrammarTest {
     assertThrows(CVC5ApiException.class, () -> g.addAnyConstant(start));
   }
 
-  @Test
-  void addAnyVariable() {
+  @Test void addAnyVariable()
+  {
     Sort bool = d_solver.getBooleanSort();
 
     Term nullTerm = d_solver.getNullTerm();
diff --git a/test/unit/api/java/cvc5/OpTest.java b/test/unit/api/java/cvc5/OpTest.java
index afe728b88..f4dd181f4 100644
--- a/test/unit/api/java/cvc5/OpTest.java
+++ b/test/unit/api/java/cvc5/OpTest.java
@@ -23,38 +23,38 @@ import org.junit.jupiter.api.AfterEach;
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
 
-class OpTest {
+class OpTest
+{
   private Solver d_solver;
 
-  @BeforeEach
-  void setUp() {
+  @BeforeEach void setUp()
+  {
     d_solver = new Solver();
   }
 
-  @Test
-  void getKind() throws CVC5ApiException {
+  @Test void getKind() throws CVC5ApiException
+  {
     Op x;
     x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
     assertDoesNotThrow(() -> x.getKind());
   }
 
-  @Test
-  void isNull() throws CVC5ApiException {
+  @Test void isNull() throws CVC5ApiException
+  {
     Op x = d_solver.getNullOp();
     assertTrue(x.isNull());
     x = d_solver.mkOp(BITVECTOR_EXTRACT, 31, 1);
     assertFalse(x.isNull());
   }
 
-  @Test
-  void opFromKind() {
+  @Test void opFromKind()
+  {
     assertDoesNotThrow(() -> d_solver.mkOp(PLUS));
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.mkOp(BITVECTOR_EXTRACT));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkOp(BITVECTOR_EXTRACT));
   }
 
-  @Test
-  void getIndicesString() throws CVC5ApiException {
+  @Test void getIndicesString() throws CVC5ApiException
+  {
     Op x = d_solver.getNullOp();
     assertThrows(CVC5ApiException.class, () -> x.getStringIndices());
 
@@ -64,8 +64,8 @@ class OpTest {
     assertEquals(divisible_idx, "4");
   }
 
-  @Test
-  void getIndicesUint() throws CVC5ApiException {
+  @Test void getIndicesUint() throws CVC5ApiException
+  {
     Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
     assertTrue(bitvector_repeat_ot.isIndexed());
     int bitvector_repeat_idx = bitvector_repeat_ot.getIntegerIndices()[0];
@@ -77,23 +77,19 @@ class OpTest {
     //              () -> bitvector_repeat_ot.getIntegerIndices());
 
     Op bitvector_zero_extend_ot = d_solver.mkOp(BITVECTOR_ZERO_EXTEND, 6);
-    int bitvector_zero_extend_idx =
-        bitvector_zero_extend_ot.getIntegerIndices()[0];
+    int bitvector_zero_extend_idx = bitvector_zero_extend_ot.getIntegerIndices()[0];
     assertEquals(bitvector_zero_extend_idx, 6);
 
     Op bitvector_sign_extend_ot = d_solver.mkOp(BITVECTOR_SIGN_EXTEND, 7);
-    int bitvector_sign_extend_idx =
-        bitvector_sign_extend_ot.getIntegerIndices()[0];
+    int bitvector_sign_extend_idx = bitvector_sign_extend_ot.getIntegerIndices()[0];
     assertEquals(bitvector_sign_extend_idx, 7);
 
     Op bitvector_rotate_left_ot = d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 8);
-    int bitvector_rotate_left_idx =
-        bitvector_rotate_left_ot.getIntegerIndices()[0];
+    int bitvector_rotate_left_idx = bitvector_rotate_left_ot.getIntegerIndices()[0];
     assertEquals(bitvector_rotate_left_idx, 8);
 
     Op bitvector_rotate_right_ot = d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 9);
-    int bitvector_rotate_right_idx =
-        bitvector_rotate_right_ot.getIntegerIndices()[0];
+    int bitvector_rotate_right_idx = bitvector_rotate_right_ot.getIntegerIndices()[0];
     assertEquals(bitvector_rotate_right_idx, 9);
 
     Op int_to_bitvector_ot = d_solver.mkOp(INT_TO_BITVECTOR, 10);
@@ -101,18 +97,16 @@ class OpTest {
     assertEquals(int_to_bitvector_idx, 10);
 
     Op floatingpoint_to_ubv_ot = d_solver.mkOp(FLOATINGPOINT_TO_UBV, 11);
-    int floatingpoint_to_ubv_idx =
-        floatingpoint_to_ubv_ot.getIntegerIndices()[0];
+    int floatingpoint_to_ubv_idx = floatingpoint_to_ubv_ot.getIntegerIndices()[0];
     assertEquals(floatingpoint_to_ubv_idx, 11);
 
     Op floatingpoint_to_sbv_ot = d_solver.mkOp(FLOATINGPOINT_TO_SBV, 13);
-    int floatingpoint_to_sbv_idx =
-        floatingpoint_to_sbv_ot.getIntegerIndices()[0];
+    int floatingpoint_to_sbv_idx = floatingpoint_to_sbv_ot.getIntegerIndices()[0];
     assertEquals(floatingpoint_to_sbv_idx, 13);
   }
 
-  @Test
-  void getIndicesPairUint() throws CVC5ApiException {
+  @Test void getIndicesPairUint() throws CVC5ApiException
+  {
     Op bitvector_extract_ot = d_solver.mkOp(BITVECTOR_EXTRACT, 4, 0);
     assertTrue(bitvector_extract_ot.isIndexed());
     int[] bitvector_extract_indices = bitvector_extract_ot.getIntegerIndices();
@@ -122,47 +116,38 @@ class OpTest {
         d_solver.mkOp(FLOATINGPOINT_TO_FP_IEEE_BITVECTOR, 4, 25);
     int[] floatingpoint_to_fp_ieee_bitvector_indices =
         floatingpoint_to_fp_ieee_bitvector_ot.getIntegerIndices();
-    assertArrayEquals(
-        floatingpoint_to_fp_ieee_bitvector_indices, new int[] {4, 25});
+    assertArrayEquals(floatingpoint_to_fp_ieee_bitvector_indices, new int[] {4, 25});
 
     Op floatingpoint_to_fp_floatingpoint_ot =
         d_solver.mkOp(FLOATINGPOINT_TO_FP_FLOATINGPOINT, 4, 25);
     int[] floatingpoint_to_fp_floatingpoint_indices =
         floatingpoint_to_fp_floatingpoint_ot.getIntegerIndices();
-    assertArrayEquals(
-        floatingpoint_to_fp_floatingpoint_indices, new int[] {4, 25});
+    assertArrayEquals(floatingpoint_to_fp_floatingpoint_indices, new int[] {4, 25});
 
-    Op floatingpoint_to_fp_real_ot =
-        d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25);
-    int[] floatingpoint_to_fp_real_indices =
-        floatingpoint_to_fp_real_ot.getIntegerIndices();
+    Op floatingpoint_to_fp_real_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_REAL, 4, 25);
+    int[] floatingpoint_to_fp_real_indices = floatingpoint_to_fp_real_ot.getIntegerIndices();
     assertArrayEquals(floatingpoint_to_fp_real_indices, new int[] {4, 25});
 
     Op floatingpoint_to_fp_signed_bitvector_ot =
         d_solver.mkOp(FLOATINGPOINT_TO_FP_SIGNED_BITVECTOR, 4, 25);
     int[] floatingpoint_to_fp_signed_bitvector_indices =
         floatingpoint_to_fp_signed_bitvector_ot.getIntegerIndices();
-    assertArrayEquals(
-        floatingpoint_to_fp_signed_bitvector_indices, new int[] {4, 25});
+    assertArrayEquals(floatingpoint_to_fp_signed_bitvector_indices, new int[] {4, 25});
 
     Op floatingpoint_to_fp_unsigned_bitvector_ot =
         d_solver.mkOp(FLOATINGPOINT_TO_FP_UNSIGNED_BITVECTOR, 4, 25);
     int[] floatingpoint_to_fp_unsigned_bitvector_indices =
         floatingpoint_to_fp_unsigned_bitvector_ot.getIntegerIndices();
-    assertArrayEquals(
-        floatingpoint_to_fp_unsigned_bitvector_indices, new int[] {4, 25});
+    assertArrayEquals(floatingpoint_to_fp_unsigned_bitvector_indices, new int[] {4, 25});
 
-    Op floatingpoint_to_fp_generic_ot =
-        d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25);
-    int[] floatingpoint_to_fp_generic_indices =
-        floatingpoint_to_fp_generic_ot.getIntegerIndices();
+    Op floatingpoint_to_fp_generic_ot = d_solver.mkOp(FLOATINGPOINT_TO_FP_GENERIC, 4, 25);
+    int[] floatingpoint_to_fp_generic_indices = floatingpoint_to_fp_generic_ot.getIntegerIndices();
     assertArrayEquals(floatingpoint_to_fp_generic_indices, new int[] {4, 25});
-    assertThrows(CVC5ApiException.class,
-        () -> floatingpoint_to_fp_generic_ot.getStringIndices());
+    assertThrows(CVC5ApiException.class, () -> floatingpoint_to_fp_generic_ot.getStringIndices());
   }
 
-  @Test
-  void opScopingToString() throws CVC5ApiException {
+  @Test void opScopingToString() throws CVC5ApiException
+  {
     Op bitvector_repeat_ot = d_solver.mkOp(BITVECTOR_REPEAT, 5);
     String op_repr = bitvector_repeat_ot.toString();
 
diff --git a/test/unit/api/java/cvc5/SolverTest.java b/test/unit/api/java/cvc5/SolverTest.java
index 57758ff88..18560f2dc 100644
--- a/test/unit/api/java/cvc5/SolverTest.java
+++ b/test/unit/api/java/cvc5/SolverTest.java
@@ -13,11 +13,14 @@
  * Black box testing of the Solver class of the Java API.
  */
 
-
 package cvc5;
 
+import static cvc5.Kind.*;
+import static cvc5.RoundingMode.*;
 import static org.junit.jupiter.api.Assertions.*;
 
+import java.util.*;
+import java.util.concurrent.atomic.AtomicReference;
 import org.junit.jupiter.api.AfterEach;
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
@@ -31,14 +34,2312 @@ class SolverTest
     d_solver = new Solver();
   }
 
-  @AfterEach void tearDown()
+  @Test void recoverableException() throws CVC5ApiException
+  {
+    d_solver.setOption("produce-models", "true");
+    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+    d_solver.assertFormula(x.eqTerm(x).notTerm());
+    assertThrows(CVC5ApiRecoverableException.class, () -> d_solver.getValue(x));
+  }
+
+  @Test void supportsFloatingPoint() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkRoundingMode(ROUND_NEAREST_TIES_TO_EVEN));
+  }
+
+  @Test void getBooleanSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.getBooleanSort());
+  }
+
+  @Test void getIntegerSort()
+  {
+    assertDoesNotThrow(() -> d_solver.getIntegerSort());
+  }
+
+  @Test void getNullSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.getNullSort());
+  }
+
+  @Test void getRealSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.getRealSort());
+  }
+
+  @Test void getRegExpSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.getRegExpSort());
+  }
+
+  @Test void getStringSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.getStringSort());
+  }
+
+  @Test void getRoundingModeSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.getRoundingModeSort());
+  }
+
+  @Test void mkArraySort() throws CVC5ApiException
+  {
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort intSort = d_solver.getIntegerSort();
+    Sort realSort = d_solver.getRealSort();
+    Sort bvSort = d_solver.mkBitVectorSort(32);
+    assertDoesNotThrow(() -> d_solver.mkArraySort(boolSort, boolSort));
+    assertDoesNotThrow(() -> d_solver.mkArraySort(intSort, intSort));
+    assertDoesNotThrow(() -> d_solver.mkArraySort(realSort, realSort));
+    assertDoesNotThrow(() -> d_solver.mkArraySort(bvSort, bvSort));
+    assertDoesNotThrow(() -> d_solver.mkArraySort(boolSort, intSort));
+    assertDoesNotThrow(() -> d_solver.mkArraySort(realSort, bvSort));
+
+    Sort fpSort = d_solver.mkFloatingPointSort(3, 5);
+    assertDoesNotThrow(() -> d_solver.mkArraySort(fpSort, fpSort));
+    assertDoesNotThrow(() -> d_solver.mkArraySort(bvSort, fpSort));
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.mkArraySort(boolSort, boolSort));
+  }
+
+  @Test void mkBitVectorSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkBitVectorSort(32));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVectorSort(0));
+  }
+
+  @Test void mkFloatingPointSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkFloatingPointSort(4, 8));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkFloatingPointSort(0, 8));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkFloatingPointSort(4, 0));
+  }
+
+  @Test void mkDatatypeSort() throws CVC5ApiException
+  {
+    DatatypeDecl dtypeSpec = d_solver.mkDatatypeDecl("list");
+    DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+    cons.addSelector("head", d_solver.getIntegerSort());
+    dtypeSpec.addConstructor(cons);
+    DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+    dtypeSpec.addConstructor(nil);
+    assertDoesNotThrow(() -> d_solver.mkDatatypeSort(dtypeSpec));
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.mkDatatypeSort(dtypeSpec));
+
+    DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list");
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSort(throwsDtypeSpec));
+  }
+
+  @Test void mkDatatypeSorts() throws CVC5ApiException
+  {
+    Solver slv = new Solver();
+
+    DatatypeDecl dtypeSpec1 = d_solver.mkDatatypeDecl("list1");
+    DatatypeConstructorDecl cons1 = d_solver.mkDatatypeConstructorDecl("cons1");
+    cons1.addSelector("head1", d_solver.getIntegerSort());
+    dtypeSpec1.addConstructor(cons1);
+    DatatypeConstructorDecl nil1 = d_solver.mkDatatypeConstructorDecl("nil1");
+    dtypeSpec1.addConstructor(nil1);
+    DatatypeDecl dtypeSpec2 = d_solver.mkDatatypeDecl("list2");
+    DatatypeConstructorDecl cons2 = d_solver.mkDatatypeConstructorDecl("cons2");
+    cons2.addSelector("head2", d_solver.getIntegerSort());
+    dtypeSpec2.addConstructor(cons2);
+    DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil2");
+    dtypeSpec2.addConstructor(nil2);
+    DatatypeDecl[] decls = {dtypeSpec1, dtypeSpec2};
+    assertDoesNotThrow(() -> d_solver.mkDatatypeSorts(decls));
+
+    assertThrows(CVC5ApiException.class, () -> slv.mkDatatypeSorts(decls));
+
+    DatatypeDecl throwsDtypeSpec = d_solver.mkDatatypeDecl("list");
+    DatatypeDecl[] throwsDecls = new DatatypeDecl[] {throwsDtypeSpec};
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkDatatypeSorts(throwsDecls));
+
+    /* with unresolved sorts */
+    Sort unresList = d_solver.mkUninterpretedSort("ulist");
+    Set<Sort> unresSorts = new HashSet<>();
+    unresSorts.add(unresList);
+    DatatypeDecl ulist = d_solver.mkDatatypeDecl("ulist");
+    DatatypeConstructorDecl ucons = d_solver.mkDatatypeConstructorDecl("ucons");
+    ucons.addSelector("car", unresList);
+    ucons.addSelector("cdr", unresList);
+    ulist.addConstructor(ucons);
+    DatatypeConstructorDecl unil = d_solver.mkDatatypeConstructorDecl("unil");
+    ulist.addConstructor(unil);
+    DatatypeDecl[] udecls = new DatatypeDecl[] {ulist};
+    assertDoesNotThrow(() -> d_solver.mkDatatypeSorts(Arrays.asList(udecls), unresSorts));
+
+    assertThrows(
+        CVC5ApiException.class, () -> slv.mkDatatypeSorts(Arrays.asList(udecls), unresSorts));
+
+    /* Note: More tests are in datatype_api_black. */
+  }
+
+  @Test void mkFunctionSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(()
+                           -> d_solver.mkFunctionSort(
+                               d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()));
+    Sort funSort =
+        d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
+    // function arguments are allowed
+    assertDoesNotThrow(() -> d_solver.mkFunctionSort(funSort, d_solver.getIntegerSort()));
+    // non-first-class arguments are not allowed
+    Sort reSort = d_solver.getRegExpSort();
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.mkFunctionSort(reSort, d_solver.getIntegerSort()));
+
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.mkFunctionSort(d_solver.getIntegerSort(), funSort));
+
+    assertDoesNotThrow(()
+                           -> d_solver.mkFunctionSort(new Sort[] {d_solver.mkUninterpretedSort("u"),
+                                                          d_solver.getIntegerSort()},
+                               d_solver.getIntegerSort()));
+    Sort funSort2 =
+        d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
+    // function arguments are allowed
+    assertDoesNotThrow(
+        ()
+            -> d_solver.mkFunctionSort(new Sort[] {funSort2, d_solver.mkUninterpretedSort("u")},
+                d_solver.getIntegerSort()));
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> d_solver.mkFunctionSort(
+                new Sort[] {d_solver.getIntegerSort(), d_solver.mkUninterpretedSort("u")},
+                funSort2));
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class,
+        () -> slv.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort()));
+
+    assertThrows(CVC5ApiException.class,
+        () -> slv.mkFunctionSort(slv.mkUninterpretedSort("u"), d_solver.getIntegerSort()));
+
+    Sort[] sorts1 =
+        new Sort[] {d_solver.getBooleanSort(), slv.getIntegerSort(), d_solver.getIntegerSort()};
+    Sort[] sorts2 = new Sort[] {slv.getBooleanSort(), slv.getIntegerSort()};
+    assertDoesNotThrow(() -> slv.mkFunctionSort(sorts2, slv.getIntegerSort()));
+    assertThrows(CVC5ApiException.class, () -> slv.mkFunctionSort(sorts1, slv.getIntegerSort()));
+    assertThrows(
+        CVC5ApiException.class, () -> slv.mkFunctionSort(sorts2, d_solver.getIntegerSort()));
+  }
+
+  @Test void mkParamSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkParamSort("T"));
+    assertDoesNotThrow(() -> d_solver.mkParamSort(""));
+  }
+
+  @Test void mkPredicateSort()
+  {
+    assertDoesNotThrow(() -> d_solver.mkPredicateSort(new Sort[] {d_solver.getIntegerSort()}));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkPredicateSort(new Sort[] {}));
+    Sort funSort =
+        d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
+    // functions as arguments are allowed
+    assertDoesNotThrow(
+        () -> d_solver.mkPredicateSort(new Sort[] {d_solver.getIntegerSort(), funSort}));
+
+    Solver slv = new Solver();
+    assertThrows(
+        CVC5ApiException.class, () -> slv.mkPredicateSort(new Sort[] {d_solver.getIntegerSort()}));
+  }
+
+  @Test void mkRecordSort() throws CVC5ApiException
+  {
+    Pair<String, Sort>[] fields = new Pair[] {new Pair<>("b", d_solver.getBooleanSort()),
+        new Pair<>("bv", d_solver.mkBitVectorSort(8)),
+        new Pair<>("i", d_solver.getIntegerSort())};
+    Pair<String, Sort>[] empty = new Pair[0];
+    assertDoesNotThrow(() -> d_solver.mkRecordSort(fields));
+    assertDoesNotThrow(() -> d_solver.mkRecordSort(empty));
+    Sort recSort = d_solver.mkRecordSort(fields);
+    assertDoesNotThrow(() -> recSort.getDatatype());
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.mkRecordSort(fields));
+  }
+
+  @Test void mkSetSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkSetSort(d_solver.getBooleanSort()));
+    assertDoesNotThrow(() -> d_solver.mkSetSort(d_solver.getIntegerSort()));
+    assertDoesNotThrow(() -> d_solver.mkSetSort(d_solver.mkBitVectorSort(4)));
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.mkSetSort(d_solver.mkBitVectorSort(4)));
+  }
+
+  @Test void mkBagSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkBagSort(d_solver.getBooleanSort()));
+    assertDoesNotThrow(() -> d_solver.mkBagSort(d_solver.getIntegerSort()));
+    assertDoesNotThrow(() -> d_solver.mkBagSort(d_solver.mkBitVectorSort(4)));
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.mkBagSort(d_solver.mkBitVectorSort(4)));
+  }
+
+  @Test void mkSequenceSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkSequenceSort(d_solver.getBooleanSort()));
+    assertDoesNotThrow(
+        () -> d_solver.mkSequenceSort(d_solver.mkSequenceSort(d_solver.getIntegerSort())));
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.mkSequenceSort(d_solver.getIntegerSort()));
+  }
+
+  @Test void mkUninterpretedSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkUninterpretedSort("u"));
+    assertDoesNotThrow(() -> d_solver.mkUninterpretedSort(""));
+  }
+
+  @Test void mkSortConstructorSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkSortConstructorSort("s", 2));
+    assertDoesNotThrow(() -> d_solver.mkSortConstructorSort("", 2));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkSortConstructorSort("", 0));
+  }
+
+  @Test void mkTupleSort() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkTupleSort(new Sort[] {d_solver.getIntegerSort()}));
+    Sort funSort =
+        d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkTupleSort(new Sort[] {d_solver.getIntegerSort(), funSort}));
+
+    Solver slv = new Solver();
+    assertThrows(
+        CVC5ApiException.class, () -> slv.mkTupleSort(new Sort[] {d_solver.getIntegerSort()}));
+  }
+
+  @Test void mkBitVector() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkBitVector(8, 2));
+    assertDoesNotThrow(() -> d_solver.mkBitVector(32, 2));
+    assertDoesNotThrow(() -> d_solver.mkBitVector(8, "-1111111", 2));
+    assertDoesNotThrow(() -> d_solver.mkBitVector(8, "0101", 2));
+    assertDoesNotThrow(() -> d_solver.mkBitVector(8, "00000101", 2));
+    assertDoesNotThrow(() -> d_solver.mkBitVector(8, "-127", 10));
+    assertDoesNotThrow(() -> d_solver.mkBitVector(8, "255", 10));
+    assertDoesNotThrow(() -> d_solver.mkBitVector(8, "-7f", 16));
+    assertDoesNotThrow(() -> d_solver.mkBitVector(8, "a0", 16));
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(0, 2));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(0, "-127", 10));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(0, "a0", 16));
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(8, "", 2));
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(8, "101", 5));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(8, "128", 11));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(8, "a0", 21));
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(8, "-11111111", 2));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(8, "101010101", 2));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(8, "-256", 10));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(8, "257", 10));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(8, "-a0", 16));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(8, "fffff", 16));
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(8, "10201010", 2));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(8, "-25x", 10));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(8, "2x7", 10));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkBitVector(8, "fzff", 16));
+
+    assertEquals(d_solver.mkBitVector(8, "0101", 2), d_solver.mkBitVector(8, "00000101", 2));
+    assertEquals(d_solver.mkBitVector(4, "-1", 2), d_solver.mkBitVector(4, "1111", 2));
+    assertEquals(d_solver.mkBitVector(4, "-1", 16), d_solver.mkBitVector(4, "1111", 2));
+    assertEquals(d_solver.mkBitVector(4, "-1", 10), d_solver.mkBitVector(4, "1111", 2));
+    assertEquals(d_solver.mkBitVector(8, "01010101", 2).toString(), "#b01010101");
+    assertEquals(d_solver.mkBitVector(8, "F", 16).toString(), "#b00001111");
+    assertEquals(d_solver.mkBitVector(8, "-1", 10), d_solver.mkBitVector(8, "FF", 16));
+  }
+
+  @Test void mkVar() throws CVC5ApiException
+  {
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort intSort = d_solver.getIntegerSort();
+    Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
+    assertDoesNotThrow(() -> d_solver.mkVar(boolSort));
+    assertDoesNotThrow(() -> d_solver.mkVar(funSort));
+    assertDoesNotThrow(() -> d_solver.mkVar(boolSort, ("b")));
+    assertDoesNotThrow(() -> d_solver.mkVar(funSort, ""));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkVar(d_solver.getNullSort()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkVar(d_solver.getNullSort(), "a"));
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.mkVar(boolSort, "x"));
+  }
+
+  @Test void mkBoolean() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkBoolean(true));
+    assertDoesNotThrow(() -> d_solver.mkBoolean(false));
+  }
+
+  @Test void mkRoundingMode() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkRoundingMode(RoundingMode.ROUND_TOWARD_ZERO));
+  }
+
+  @Test void mkUninterpretedConst() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.mkUninterpretedConst(d_solver.getNullSort(), 1));
+    Solver slv = new Solver();
+    assertThrows(
+        CVC5ApiException.class, () -> slv.mkUninterpretedConst(d_solver.getBooleanSort(), 1));
+  }
+
+  @Test void mkAbstractValue() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkAbstractValue(("1")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("0")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("-1")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(("1.2")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue("1/2"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue("asdf"));
+
+    assertDoesNotThrow(() -> d_solver.mkAbstractValue((int) 1));
+    assertDoesNotThrow(() -> d_solver.mkAbstractValue((int) 1));
+    assertDoesNotThrow(() -> d_solver.mkAbstractValue((long) 1));
+    assertDoesNotThrow(() -> d_solver.mkAbstractValue((long) 1));
+    // java does not have specific types for unsigned integers, therefore the two lines below do not
+    // make sense in java. assertDoesNotThrow(() -> d_solver.mkAbstractValue((int)-1));
+    // assertDoesNotThrow(() -> d_solver.mkAbstractValue((long)-1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkAbstractValue(0));
+  }
+
+  @Test void mkFloatingPoint() throws CVC5ApiException
+  {
+    Term t1 = d_solver.mkBitVector(8);
+    Term t2 = d_solver.mkBitVector(4);
+    Term t3 = d_solver.mkInteger(2);
+    assertDoesNotThrow(() -> d_solver.mkFloatingPoint(3, 5, t1));
+
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.mkFloatingPoint(0, 5, d_solver.getNullTerm()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkFloatingPoint(0, 5, t1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkFloatingPoint(3, 0, t1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkFloatingPoint(3, 5, t2));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkFloatingPoint(3, 5, t2));
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.mkFloatingPoint(3, 5, t1));
+  }
+
+  @Test void mkEmptySet() throws CVC5ApiException
+  {
+    Solver slv = new Solver();
+    Sort s = d_solver.mkSetSort(d_solver.getBooleanSort());
+    assertDoesNotThrow(() -> d_solver.mkEmptySet(d_solver.getNullSort()));
+    assertDoesNotThrow(() -> d_solver.mkEmptySet(s));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkEmptySet(d_solver.getBooleanSort()));
+    assertThrows(CVC5ApiException.class, () -> slv.mkEmptySet(s));
+  }
+
+  @Test void mkEmptyBag() throws CVC5ApiException
+  {
+    Solver slv = new Solver();
+    Sort s = d_solver.mkBagSort(d_solver.getBooleanSort());
+    assertDoesNotThrow(() -> d_solver.mkEmptyBag(d_solver.getNullSort()));
+    assertDoesNotThrow(() -> d_solver.mkEmptyBag(s));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkEmptyBag(d_solver.getBooleanSort()));
+
+    assertThrows(CVC5ApiException.class, () -> slv.mkEmptyBag(s));
+  }
+
+  @Test void mkEmptySequence() throws CVC5ApiException
+  {
+    Solver slv = new Solver();
+    Sort s = d_solver.mkSequenceSort(d_solver.getBooleanSort());
+    assertDoesNotThrow(() -> d_solver.mkEmptySequence(s));
+    assertDoesNotThrow(() -> d_solver.mkEmptySequence(d_solver.getBooleanSort()));
+    assertThrows(CVC5ApiException.class, () -> slv.mkEmptySequence(s));
+  }
+
+  @Test void mkFalse() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkFalse());
+    assertDoesNotThrow(() -> d_solver.mkFalse());
+  }
+
+  @Test void mkNaN() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkNaN(3, 5));
+  }
+
+  @Test void mkNegZero() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.mkNegZero(3, 5));
+  }
+
+  @Test void mkNegInf()
+  {
+    assertDoesNotThrow(() -> d_solver.mkNegInf(3, 5));
+  }
+
+  @Test void mkPosInf()
+  {
+    assertDoesNotThrow(() -> d_solver.mkPosInf(3, 5));
+  }
+
+  @Test void mkPosZero()
+  {
+    assertDoesNotThrow(() -> d_solver.mkPosZero(3, 5));
+  }
+
+  @Test void mkOp()
+  {
+    // Unlike c++,  mkOp(Kind kind, Kind k) is a type error in java
+    // assertThrows(CVC5ApiException.class, () -> d_solver.mkOp(BITVECTOR_EXTRACT, EQUAL));
+
+    // mkOp(Kind kind, const std::string& arg)
+    assertDoesNotThrow(() -> d_solver.mkOp(DIVISIBLE, "2147483648"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkOp(BITVECTOR_EXTRACT, "asdf"));
+
+    // mkOp(Kind kind, int arg)
+    assertDoesNotThrow(() -> d_solver.mkOp(DIVISIBLE, 1));
+    assertDoesNotThrow(() -> d_solver.mkOp(BITVECTOR_ROTATE_LEFT, 1));
+    assertDoesNotThrow(() -> d_solver.mkOp(BITVECTOR_ROTATE_RIGHT, 1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkOp(BITVECTOR_EXTRACT, 1));
+
+    // mkOp(Kind kind, int arg1, int arg2)
+    assertDoesNotThrow(() -> d_solver.mkOp(BITVECTOR_EXTRACT, 1, 1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkOp(DIVISIBLE, 1, 2));
+
+    // mkOp(Kind kind, int[] args)
+    int[] args = new int[] {1, 2, 2};
+    assertDoesNotThrow(() -> d_solver.mkOp(TUPLE_PROJECT, args));
+  }
+
+  @Test void mkPi()
+  {
+    assertDoesNotThrow(() -> d_solver.mkPi());
+  }
+
+  @Test void mkInteger()
+  {
+    assertDoesNotThrow(() -> d_solver.mkInteger("123"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("1.23"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("1/23"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("12/3"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(".2"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("2."));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(""));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("asdf"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("1.2/3"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("."));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("/"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("2/"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger("/2"));
+
+    assertDoesNotThrow(() -> d_solver.mkReal(("123")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(("1.23")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(("1/23")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(("12/3")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger((".2")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(("2.")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(("")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(("asdf")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(("1.2/3")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger((".")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(("/")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(("2/")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkInteger(("/2")));
+
+    int val1 = 1;
+    long val2 = -1;
+    int val3 = 1;
+    long val4 = -1;
+    assertDoesNotThrow(() -> d_solver.mkInteger(val1));
+    assertDoesNotThrow(() -> d_solver.mkInteger(val2));
+    assertDoesNotThrow(() -> d_solver.mkInteger(val3));
+    assertDoesNotThrow(() -> d_solver.mkInteger(val4));
+    assertDoesNotThrow(() -> d_solver.mkInteger(val4));
+  }
+
+  @Test void mkReal()
+  {
+    assertDoesNotThrow(() -> d_solver.mkReal("123"));
+    assertDoesNotThrow(() -> d_solver.mkReal("1.23"));
+    assertDoesNotThrow(() -> d_solver.mkReal("1/23"));
+    assertDoesNotThrow(() -> d_solver.mkReal("12/3"));
+    assertDoesNotThrow(() -> d_solver.mkReal(".2"));
+    assertDoesNotThrow(() -> d_solver.mkReal("2."));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkReal(""));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkReal("asdf"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkReal("1.2/3"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkReal("."));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkReal("/"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkReal("2/"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkReal("/2"));
+
+    assertDoesNotThrow(() -> d_solver.mkReal(("123")));
+    assertDoesNotThrow(() -> d_solver.mkReal(("1.23")));
+    assertDoesNotThrow(() -> d_solver.mkReal(("1/23")));
+    assertDoesNotThrow(() -> d_solver.mkReal(("12/3")));
+    assertDoesNotThrow(() -> d_solver.mkReal((".2")));
+    assertDoesNotThrow(() -> d_solver.mkReal(("2.")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkReal(("")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkReal(("asdf")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkReal(("1.2/3")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkReal((".")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkReal(("/")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkReal(("2/")));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkReal(("/2")));
+
+    int val1 = 1;
+    long val2 = -1;
+    int val3 = 1;
+    long val4 = -1;
+    assertDoesNotThrow(() -> d_solver.mkReal(val1));
+    assertDoesNotThrow(() -> d_solver.mkReal(val2));
+    assertDoesNotThrow(() -> d_solver.mkReal(val3));
+    assertDoesNotThrow(() -> d_solver.mkReal(val4));
+    assertDoesNotThrow(() -> d_solver.mkReal(val4));
+    assertDoesNotThrow(() -> d_solver.mkReal(val1, val1));
+    assertDoesNotThrow(() -> d_solver.mkReal(val2, val2));
+    assertDoesNotThrow(() -> d_solver.mkReal(val3, val3));
+    assertDoesNotThrow(() -> d_solver.mkReal(val4, val4));
+  }
+
+  @Test void mkRegexpEmpty()
+  {
+    Sort strSort = d_solver.getStringSort();
+    Term s = d_solver.mkConst(strSort, "s");
+    assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpEmpty()));
+  }
+
+  @Test void mkRegexpSigma()
+  {
+    Sort strSort = d_solver.getStringSort();
+    Term s = d_solver.mkConst(strSort, "s");
+    assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpSigma()));
+  }
+
+  @Test void mkSepNil()
+  {
+    assertDoesNotThrow(() -> d_solver.mkSepNil(d_solver.getBooleanSort()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkSepNil(d_solver.getNullSort()));
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.mkSepNil(d_solver.getIntegerSort()));
+  }
+
+  @Test void mkString()
+  {
+    assertDoesNotThrow(() -> d_solver.mkString(""));
+    assertDoesNotThrow(() -> d_solver.mkString("asdfasdf"));
+    assertEquals(d_solver.mkString("asdf\\nasdf").toString(), "\"asdf\\u{5c}nasdf\"");
+    assertEquals(d_solver.mkString("asdf\\u{005c}nasdf", true).toString(), "\"asdf\\u{5c}nasdf\"");
+  }
+
+  @Test void mkTerm() throws CVC5ApiException
+  {
+    Sort bv32 = d_solver.mkBitVectorSort(32);
+    Term a = d_solver.mkConst(bv32, "a");
+    Term b = d_solver.mkConst(bv32, "b");
+    Term[] v1 = new Term[] {a, b};
+    Term[] v2 = new Term[] {a, d_solver.getNullTerm()};
+    Term[] v3 = new Term[] {a, d_solver.mkTrue()};
+    Term[] v4 = new Term[] {d_solver.mkInteger(1), d_solver.mkInteger(2)};
+    Term[] v5 = new Term[] {d_solver.mkInteger(1), d_solver.getNullTerm()};
+    Term[] v6 = new Term[] {};
+    Solver slv = new Solver();
+
+    // mkTerm(Kind kind) const
+    assertDoesNotThrow(() -> d_solver.mkTerm(PI));
+    assertDoesNotThrow(() -> d_solver.mkTerm(REGEXP_EMPTY));
+    assertDoesNotThrow(() -> d_solver.mkTerm(REGEXP_SIGMA));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(CONST_BITVECTOR));
+
+    // mkTerm(Kind kind, Term child) const
+    assertDoesNotThrow(() -> d_solver.mkTerm(NOT, d_solver.mkTrue()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(NOT, d_solver.getNullTerm()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(NOT, a));
+    assertThrows(CVC5ApiException.class, () -> slv.mkTerm(NOT, d_solver.mkTrue()));
+
+    // mkTerm(Kind kind, Term child1, Term child2) const
+    assertDoesNotThrow(() -> d_solver.mkTerm(EQUAL, a, b));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(EQUAL, d_solver.getNullTerm(), b));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(EQUAL, a, d_solver.getNullTerm()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(EQUAL, a, d_solver.mkTrue()));
+    assertThrows(CVC5ApiException.class, () -> slv.mkTerm(EQUAL, a, b));
+
+    // mkTerm(Kind kind, Term child1, Term child2, Term child3) const
+    assertDoesNotThrow(
+        () -> d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()));
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkTerm(ITE, d_solver.getNullTerm(), d_solver.mkTrue(), d_solver.mkTrue()));
+
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.getNullTerm(), d_solver.mkTrue()));
+
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.getNullTerm()));
+
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), b));
+
+    assertThrows(CVC5ApiException.class,
+        () -> slv.mkTerm(ITE, d_solver.mkTrue(), d_solver.mkTrue(), d_solver.mkTrue()));
+
+    // mkTerm(Kind kind, const Term[]& children) const
+    assertDoesNotThrow(() -> d_solver.mkTerm(EQUAL, v1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(EQUAL, v2));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(EQUAL, v3));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(DISTINCT, v6));
+  }
+
+  @Test void mkTermFromOp() throws CVC5ApiException
+  {
+    Sort bv32 = d_solver.mkBitVectorSort(32);
+    Term a = d_solver.mkConst(bv32, "a");
+    Term b = d_solver.mkConst(bv32, "b");
+    Term[] v1 = new Term[] {d_solver.mkInteger(1), d_solver.mkInteger(2)};
+    Term[] v2 = new Term[] {d_solver.mkInteger(1), d_solver.getNullTerm()};
+    Term[] v3 = new Term[] {};
+    Term[] v4 = new Term[] {d_solver.mkInteger(5)};
+    Solver slv = new Solver();
+
+    // simple operator terms
+    Op opterm1 = d_solver.mkOp(BITVECTOR_EXTRACT, 2, 1);
+    Op opterm2 = d_solver.mkOp(DIVISIBLE, 1);
+
+    // list datatype
+    Sort sort = d_solver.mkParamSort("T");
+    DatatypeDecl listDecl = d_solver.mkDatatypeDecl("paramlist", sort);
+    DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+    DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+    cons.addSelector("head", sort);
+    cons.addSelectorSelf("tail");
+    listDecl.addConstructor(cons);
+    listDecl.addConstructor(nil);
+    Sort listSort = d_solver.mkDatatypeSort(listDecl);
+    Sort intListSort = listSort.instantiate(new Sort[] {d_solver.getIntegerSort()});
+    Term c = d_solver.mkConst(intListSort, "c");
+    Datatype list = listSort.getDatatype();
+
+    // list datatype constructor and selector operator terms
+    Term consTerm1 = list.getConstructorTerm("cons");
+    Term consTerm2 = list.getConstructor("cons").getConstructorTerm();
+    Term nilTerm1 = list.getConstructorTerm("nil");
+    Term nilTerm2 = list.getConstructor("nil").getConstructorTerm();
+    Term headTerm1 = list.getConstructor("cons").getSelectorTerm("head");
+    Term headTerm2 = list.getConstructor("cons").getSelector("head").getSelectorTerm();
+    Term tailTerm1 = list.getConstructor("cons").getSelectorTerm("tail");
+    Term tailTerm2 = list.getConstructor("cons").getSelector("tail").getSelectorTerm();
+
+    // mkTerm(Op op, Term term) const
+    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1));
+    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm2));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, nilTerm1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, consTerm1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm2));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(APPLY_SELECTOR, headTerm1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1));
+    assertThrows(CVC5ApiException.class, () -> slv.mkTerm(APPLY_CONSTRUCTOR, nilTerm1));
+
+    // mkTerm(Op op, Term child) const
+    assertDoesNotThrow(() -> d_solver.mkTerm(opterm1, a));
+    assertDoesNotThrow(() -> d_solver.mkTerm(opterm2, d_solver.mkInteger(1)));
+    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_SELECTOR, headTerm1, c));
+    assertDoesNotThrow(() -> d_solver.mkTerm(APPLY_SELECTOR, tailTerm2, c));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, a));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1, d_solver.getNullTerm()));
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm1, d_solver.mkInteger(0)));
+
+    assertThrows(CVC5ApiException.class, () -> slv.mkTerm(opterm1, a));
+
+    // mkTerm(Op op, Term child1, Term child2) const
+    assertDoesNotThrow(()
+                           -> d_solver.mkTerm(APPLY_CONSTRUCTOR,
+                               consTerm1,
+                               d_solver.mkInteger(0),
+                               d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkTerm(opterm2, d_solver.mkInteger(1), d_solver.mkInteger(2)));
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1, a, b));
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkTerm(opterm2, d_solver.mkInteger(1), d_solver.getNullTerm()));
+
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkTerm(opterm2, d_solver.getNullTerm(), d_solver.mkInteger(1)));
+
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> slv.mkTerm(APPLY_CONSTRUCTOR,
+                consTerm1,
+                d_solver.mkInteger(0),
+                d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm1)));
+
+    // mkTerm(Op op, Term child1, Term child2, Term child3) const
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm1, a, b, a));
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> d_solver.mkTerm(
+                opterm2, d_solver.mkInteger(1), d_solver.mkInteger(1), d_solver.getNullTerm()));
+
+    // mkTerm(Op op, Term[] children)
+    assertDoesNotThrow(() -> d_solver.mkTerm(opterm2, v4));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, v1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, v2));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkTerm(opterm2, v3));
+    assertThrows(CVC5ApiException.class, () -> slv.mkTerm(opterm2, v4));
+  }
+
+  @Test void mkTrue()
+  {
+    assertDoesNotThrow(() -> d_solver.mkTrue());
+    assertDoesNotThrow(() -> d_solver.mkTrue());
+  }
+
+  @Test void mkTuple()
+  {
+    assertDoesNotThrow(()
+                           -> d_solver.mkTuple(new Sort[] {d_solver.mkBitVectorSort(3)},
+                               new Term[] {d_solver.mkBitVector(3, "101", 2)}));
+    assertDoesNotThrow(()
+                           -> d_solver.mkTuple(new Sort[] {d_solver.getRealSort()},
+                               new Term[] {d_solver.mkInteger("5")}));
+
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkTuple(new Sort[] {}, new Term[] {d_solver.mkBitVector(3, "101", 2)}));
+
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> d_solver.mkTuple(new Sort[] {d_solver.mkBitVectorSort(4)},
+                new Term[] {d_solver.mkBitVector(3, "101", 2)}));
+
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> d_solver.mkTuple(
+                new Sort[] {d_solver.getIntegerSort()}, new Term[] {d_solver.mkReal("5.3")}));
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> slv.mkTuple(new Sort[] {d_solver.mkBitVectorSort(3)},
+                new Term[] {slv.mkBitVector(3, "101", 2)}));
+
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> slv.mkTuple(new Sort[] {slv.mkBitVectorSort(3)},
+                new Term[] {d_solver.mkBitVector(3, "101", 2)}));
+  }
+
+  @Test void mkUniverseSet()
+  {
+    assertDoesNotThrow(() -> d_solver.mkUniverseSet(d_solver.getBooleanSort()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkUniverseSet(d_solver.getNullSort()));
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.mkUniverseSet(d_solver.getBooleanSort()));
+  }
+
+  @Test void mkConst()
+  {
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort intSort = d_solver.getIntegerSort();
+    Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
+    assertDoesNotThrow(() -> d_solver.mkConst(boolSort));
+    assertDoesNotThrow(() -> d_solver.mkConst(funSort));
+    assertDoesNotThrow(() -> d_solver.mkConst(boolSort, ("b")));
+    assertDoesNotThrow(() -> d_solver.mkConst(intSort, ("i")));
+    assertDoesNotThrow(() -> d_solver.mkConst(funSort, "f"));
+    assertDoesNotThrow(() -> d_solver.mkConst(funSort, ""));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkConst(d_solver.getNullSort()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkConst(d_solver.getNullSort(), "a"));
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.mkConst(boolSort));
+  }
+
+  @Test void mkConstArray()
+  {
+    Sort intSort = d_solver.getIntegerSort();
+    Sort arrSort = d_solver.mkArraySort(intSort, intSort);
+    Term zero = d_solver.mkInteger(0);
+    Term constArr = d_solver.mkConstArray(arrSort, zero);
+
+    assertDoesNotThrow(() -> d_solver.mkConstArray(arrSort, zero));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkConstArray(d_solver.getNullSort(), zero));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.mkConstArray(arrSort, d_solver.getNullTerm()));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.mkConstArray(arrSort, d_solver.mkBitVector(1, 1)));
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkConstArray(intSort, zero));
+    Solver slv = new Solver();
+    Term zero2 = slv.mkInteger(0);
+    Sort arrSort2 = slv.mkArraySort(slv.getIntegerSort(), slv.getIntegerSort());
+    assertThrows(CVC5ApiException.class, () -> slv.mkConstArray(arrSort2, zero));
+    assertThrows(CVC5ApiException.class, () -> slv.mkConstArray(arrSort, zero2));
+  }
+
+  @Test void declareDatatype()
+  {
+    DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+    DatatypeConstructorDecl[] ctors1 = new DatatypeConstructorDecl[] {nil};
+    assertDoesNotThrow(() -> d_solver.declareDatatype(("a"), ctors1));
+    DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+    DatatypeConstructorDecl nil2 = d_solver.mkDatatypeConstructorDecl("nil");
+    DatatypeConstructorDecl[] ctors2 = new DatatypeConstructorDecl[] {cons, nil2};
+    assertDoesNotThrow(() -> d_solver.declareDatatype(("b"), ctors2));
+    DatatypeConstructorDecl cons2 = d_solver.mkDatatypeConstructorDecl("cons");
+    DatatypeConstructorDecl nil3 = d_solver.mkDatatypeConstructorDecl("nil");
+    DatatypeConstructorDecl[] ctors3 = new DatatypeConstructorDecl[] {cons2, nil3};
+    assertDoesNotThrow(() -> d_solver.declareDatatype((""), ctors3));
+    DatatypeConstructorDecl[] ctors4 = new DatatypeConstructorDecl[0];
+    assertThrows(CVC5ApiException.class, () -> d_solver.declareDatatype(("c"), ctors4));
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.declareDatatype((""), ctors4));
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.declareDatatype(("a"), ctors1));
+  }
+
+  @Test void declareFun() throws CVC5ApiException
+  {
+    Sort bvSort = d_solver.mkBitVectorSort(32);
+    Sort funSort =
+        d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
+    assertDoesNotThrow(() -> d_solver.declareFun("f1", new Sort[] {}, bvSort));
+    assertDoesNotThrow(
+        () -> d_solver.declareFun("f3", new Sort[] {bvSort, d_solver.getIntegerSort()}, bvSort));
+    assertThrows(CVC5ApiException.class, () -> d_solver.declareFun("f2", new Sort[] {}, funSort));
+    // functions as arguments is allowed
+    assertDoesNotThrow(() -> d_solver.declareFun("f4", new Sort[] {bvSort, funSort}, bvSort));
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.declareFun("f5", new Sort[] {bvSort, bvSort}, funSort));
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.declareFun("f1", new Sort[] {}, bvSort));
+  }
+
+  @Test void declareSort()
+  {
+    assertDoesNotThrow(() -> d_solver.declareSort("s", 0));
+    assertDoesNotThrow(() -> d_solver.declareSort("s", 2));
+    assertDoesNotThrow(() -> d_solver.declareSort("", 2));
+  }
+
+  @Test void defineSort()
+  {
+    Sort sortVar0 = d_solver.mkParamSort("T0");
+    Sort sortVar1 = d_solver.mkParamSort("T1");
+    Sort intSort = d_solver.getIntegerSort();
+    Sort realSort = d_solver.getRealSort();
+    Sort arraySort0 = d_solver.mkArraySort(sortVar0, sortVar0);
+    Sort arraySort1 = d_solver.mkArraySort(sortVar0, sortVar1);
+    // Now create instantiations of the defined sorts
+    assertDoesNotThrow(() -> arraySort0.substitute(sortVar0, intSort));
+    assertDoesNotThrow(()
+                           -> arraySort1.substitute(
+                               new Sort[] {sortVar0, sortVar1}, new Sort[] {intSort, realSort}));
+  }
+
+  @Test void defineFun() throws CVC5ApiException
+  {
+    Sort bvSort = d_solver.mkBitVectorSort(32);
+    Sort funSort1 = d_solver.mkFunctionSort(new Sort[] {bvSort, bvSort}, bvSort);
+    Sort funSort2 =
+        d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
+    Term b1 = d_solver.mkVar(bvSort, "b1");
+    Term b11 = d_solver.mkVar(bvSort, "b1");
+    Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
+    Term b3 = d_solver.mkVar(funSort2, "b3");
+    Term v1 = d_solver.mkConst(bvSort, "v1");
+    Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
+    Term v3 = d_solver.mkConst(funSort2, "v3");
+    Term f1 = d_solver.mkConst(funSort1, "f1");
+    Term f2 = d_solver.mkConst(funSort2, "f2");
+    Term f3 = d_solver.mkConst(bvSort, "f3");
+    assertDoesNotThrow(() -> d_solver.defineFun("f", new Term[] {}, bvSort, v1));
+    assertDoesNotThrow(() -> d_solver.defineFun("ff", new Term[] {b1, b2}, bvSort, v1));
+    assertDoesNotThrow(() -> d_solver.defineFun(f1, new Term[] {b1, b11}, v1));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.defineFun("ff", new Term[] {v1, b2}, bvSort, v1));
+
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.defineFun("fff", new Term[] {b1}, bvSort, v3));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.defineFun("ffff", new Term[] {b1}, funSort2, v3));
+
+    // b3 has function sort, which is allowed as an argument
+    assertDoesNotThrow(() -> d_solver.defineFun("fffff", new Term[] {b1, b3}, bvSort, v1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f1, new Term[] {v1, b11}, v1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f1, new Term[] {b1}, v1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f1, new Term[] {b1, b11}, v2));
+    assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f1, new Term[] {b1, b11}, v3));
+    assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f2, new Term[] {b1}, v2));
+    assertThrows(CVC5ApiException.class, () -> d_solver.defineFun(f3, new Term[] {b1}, v1));
+
+    Solver slv = new Solver();
+    Sort bvSort2 = slv.mkBitVectorSort(32);
+    Term v12 = slv.mkConst(bvSort2, "v1");
+    Term b12 = slv.mkVar(bvSort2, "b1");
+    Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
+    assertThrows(CVC5ApiException.class, () -> slv.defineFun("f", new Term[] {}, bvSort, v12));
+    assertThrows(CVC5ApiException.class, () -> slv.defineFun("f", new Term[] {}, bvSort2, v1));
+    assertThrows(
+        CVC5ApiException.class, () -> slv.defineFun("ff", new Term[] {b1, b22}, bvSort2, v12));
+    assertThrows(
+        CVC5ApiException.class, () -> slv.defineFun("ff", new Term[] {b12, b2}, bvSort2, v12));
+    assertThrows(
+        CVC5ApiException.class, () -> slv.defineFun("ff", new Term[] {b12, b22}, bvSort, v12));
+    assertThrows(
+        CVC5ApiException.class, () -> slv.defineFun("ff", new Term[] {b12, b22}, bvSort2, v1));
+  }
+
+  @Test void defineFunGlobal()
+  {
+    Sort bSort = d_solver.getBooleanSort();
+    Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
+
+    Term bTrue = d_solver.mkBoolean(true);
+    // (define-fun f () Bool true)
+    Term f = d_solver.defineFun("f", new Term[] {}, bSort, bTrue, true);
+    Term b = d_solver.mkVar(bSort, "b");
+    Term gSym = d_solver.mkConst(fSort, "g");
+    // (define-fun g (b Bool) Bool b)
+    Term g = d_solver.defineFun(gSym, new Term[] {b}, b, true);
+
+    // (assert (or (not f) (not (g true))))
+    d_solver.assertFormula(
+        d_solver.mkTerm(OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
+    assertTrue(d_solver.checkSat().isUnsat());
+    d_solver.resetAssertions();
+    // (assert (or (not f) (not (g true))))
+    d_solver.assertFormula(
+        d_solver.mkTerm(OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
+    assertTrue(d_solver.checkSat().isUnsat());
+  }
+
+  @Test void defineFunRec() throws CVC5ApiException
+  {
+    Sort bvSort = d_solver.mkBitVectorSort(32);
+    Sort funSort1 = d_solver.mkFunctionSort(new Sort[] {bvSort, bvSort}, bvSort);
+    Sort funSort2 =
+        d_solver.mkFunctionSort(d_solver.mkUninterpretedSort("u"), d_solver.getIntegerSort());
+    Term b1 = d_solver.mkVar(bvSort, "b1");
+    Term b11 = d_solver.mkVar(bvSort, "b1");
+    Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
+    Term b3 = d_solver.mkVar(funSort2, "b3");
+    Term v1 = d_solver.mkConst(bvSort, "v1");
+    Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
+    Term v3 = d_solver.mkConst(funSort2, "v3");
+    Term f1 = d_solver.mkConst(funSort1, "f1");
+    Term f2 = d_solver.mkConst(funSort2, "f2");
+    Term f3 = d_solver.mkConst(bvSort, "f3");
+    assertDoesNotThrow(() -> d_solver.defineFunRec("f", new Term[] {}, bvSort, v1));
+    assertDoesNotThrow(() -> d_solver.defineFunRec("ff", new Term[] {b1, b2}, bvSort, v1));
+    assertDoesNotThrow(() -> d_solver.defineFunRec(f1, new Term[] {b1, b11}, v1));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.defineFunRec("fff", new Term[] {b1}, bvSort, v3));
+
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.defineFunRec("ff", new Term[] {b1, v2}, bvSort, v1));
+
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.defineFunRec("ffff", new Term[] {b1}, funSort2, v3));
+
+    // b3 has function sort, which is allowed as an argument
+    assertDoesNotThrow(() -> d_solver.defineFunRec("fffff", new Term[] {b1, b3}, bvSort, v1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.defineFunRec(f1, new Term[] {b1}, v1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.defineFunRec(f1, new Term[] {b1, b11}, v2));
+    assertThrows(CVC5ApiException.class, () -> d_solver.defineFunRec(f1, new Term[] {b1, b11}, v3));
+    assertThrows(CVC5ApiException.class, () -> d_solver.defineFunRec(f2, new Term[] {b1}, v2));
+    assertThrows(CVC5ApiException.class, () -> d_solver.defineFunRec(f3, new Term[] {b1}, v1));
+
+    Solver slv = new Solver();
+    Sort bvSort2 = slv.mkBitVectorSort(32);
+    Term v12 = slv.mkConst(bvSort2, "v1");
+    Term b12 = slv.mkVar(bvSort2, "b1");
+    Term b22 = slv.mkVar(slv.getIntegerSort(), "b2");
+    assertDoesNotThrow(() -> slv.defineFunRec("f", new Term[] {}, bvSort2, v12));
+    assertDoesNotThrow(() -> slv.defineFunRec("ff", new Term[] {b12, b22}, bvSort2, v12));
+    assertThrows(CVC5ApiException.class, () -> slv.defineFunRec("f", new Term[] {}, bvSort, v12));
+    assertThrows(CVC5ApiException.class, () -> slv.defineFunRec("f", new Term[] {}, bvSort2, v1));
+    assertThrows(
+        CVC5ApiException.class, () -> slv.defineFunRec("ff", new Term[] {b1, b22}, bvSort2, v12));
+
+    assertThrows(
+        CVC5ApiException.class, () -> slv.defineFunRec("ff", new Term[] {b12, b2}, bvSort2, v12));
+
+    assertThrows(
+        CVC5ApiException.class, () -> slv.defineFunRec("ff", new Term[] {b12, b22}, bvSort, v12));
+
+    assertThrows(
+        CVC5ApiException.class, () -> slv.defineFunRec("ff", new Term[] {b12, b22}, bvSort2, v1));
+  }
+
+  @Test void defineFunRecWrongLogic() throws CVC5ApiException
+  {
+    d_solver.setLogic("QF_BV");
+    Sort bvSort = d_solver.mkBitVectorSort(32);
+    Sort funSort = d_solver.mkFunctionSort(new Sort[] {bvSort, bvSort}, bvSort);
+    Term b = d_solver.mkVar(bvSort, "b");
+    Term v = d_solver.mkConst(bvSort, "v");
+    Term f = d_solver.mkConst(funSort, "f");
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.defineFunRec("f", new Term[] {}, bvSort, v));
+    assertThrows(CVC5ApiException.class, () -> d_solver.defineFunRec(f, new Term[] {b, b}, v));
+  }
+
+  @Test void defineFunRecGlobal() throws CVC5ApiException
+  {
+    Sort bSort = d_solver.getBooleanSort();
+    Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
+
+    d_solver.push();
+    Term bTrue = d_solver.mkBoolean(true);
+    // (define-fun f () Bool true)
+    Term f = d_solver.defineFunRec("f", new Term[] {}, bSort, bTrue, true);
+    Term b = d_solver.mkVar(bSort, "b");
+    Term gSym = d_solver.mkConst(fSort, "g");
+    // (define-fun g (b Bool) Bool b)
+    Term g = d_solver.defineFunRec(gSym, new Term[] {b}, b, true);
+
+    // (assert (or (not f) (not (g true))))
+    d_solver.assertFormula(
+        d_solver.mkTerm(OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
+    assertTrue(d_solver.checkSat().isUnsat());
+    d_solver.pop();
+    // (assert (or (not f) (not (g true))))
+    d_solver.assertFormula(
+        d_solver.mkTerm(OR, f.notTerm(), d_solver.mkTerm(APPLY_UF, g, bTrue).notTerm()));
+    assertTrue(d_solver.checkSat().isUnsat());
+  }
+
+  @Test void defineFunsRec() throws CVC5ApiException
+  {
+    Sort uSort = d_solver.mkUninterpretedSort("u");
+    Sort bvSort = d_solver.mkBitVectorSort(32);
+    Sort funSort1 = d_solver.mkFunctionSort(new Sort[] {bvSort, bvSort}, bvSort);
+    Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
+    Term b1 = d_solver.mkVar(bvSort, "b1");
+    Term b11 = d_solver.mkVar(bvSort, "b1");
+    Term b2 = d_solver.mkVar(d_solver.getIntegerSort(), "b2");
+    Term b3 = d_solver.mkVar(funSort2, "b3");
+    Term b4 = d_solver.mkVar(uSort, "b4");
+    Term v1 = d_solver.mkConst(bvSort, "v1");
+    Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
+    Term v3 = d_solver.mkConst(funSort2, "v3");
+    Term v4 = d_solver.mkConst(uSort, "v4");
+    Term f1 = d_solver.mkConst(funSort1, "f1");
+    Term f2 = d_solver.mkConst(funSort2, "f2");
+    Term f3 = d_solver.mkConst(bvSort, "f3");
+    assertDoesNotThrow(
+        ()
+            -> d_solver.defineFunsRec(
+                new Term[] {f1, f2}, new Term[][] {{b1, b11}, {b4}}, new Term[] {v1, v2}));
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> d_solver.defineFunsRec(
+                new Term[] {f1, f2}, new Term[][] {{v1, b11}, {b4}}, new Term[] {v1, v2}));
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> d_solver.defineFunsRec(
+                new Term[] {f1, f3}, new Term[][] {{b1, b11}, {b4}}, new Term[] {v1, v2}));
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> d_solver.defineFunsRec(
+                new Term[] {f1, f2}, new Term[][] {{b1}, {b4}}, new Term[] {v1, v2}));
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> d_solver.defineFunsRec(
+                new Term[] {f1, f2}, new Term[][] {{b1, b2}, {b4}}, new Term[] {v1, v2}));
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> d_solver.defineFunsRec(
+                new Term[] {f1, f2}, new Term[][] {{b1, b11}, {b4}}, new Term[] {v1, v4}));
+
+    Solver slv = new Solver();
+    Sort uSort2 = slv.mkUninterpretedSort("u");
+    Sort bvSort2 = slv.mkBitVectorSort(32);
+    Sort funSort12 = slv.mkFunctionSort(new Sort[] {bvSort2, bvSort2}, bvSort2);
+    Sort funSort22 = slv.mkFunctionSort(uSort2, slv.getIntegerSort());
+    Term b12 = slv.mkVar(bvSort2, "b1");
+    Term b112 = slv.mkVar(bvSort2, "b1");
+    Term b42 = slv.mkVar(uSort2, "b4");
+    Term v12 = slv.mkConst(bvSort2, "v1");
+    Term v22 = slv.mkConst(slv.getIntegerSort(), "v2");
+    Term f12 = slv.mkConst(funSort12, "f1");
+    Term f22 = slv.mkConst(funSort22, "f2");
+    assertDoesNotThrow(
+        ()
+            -> slv.defineFunsRec(
+                new Term[] {f12, f22}, new Term[][] {{b12, b112}, {b42}}, new Term[] {v12, v22}));
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> slv.defineFunsRec(
+                new Term[] {f1, f22}, new Term[][] {{b12, b112}, {b42}}, new Term[] {v12, v22}));
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> slv.defineFunsRec(
+                new Term[] {f12, f2}, new Term[][] {{b12, b112}, {b42}}, new Term[] {v12, v22}));
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> slv.defineFunsRec(
+                new Term[] {f12, f22}, new Term[][] {{b1, b112}, {b42}}, new Term[] {v12, v22}));
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> slv.defineFunsRec(
+                new Term[] {f12, f22}, new Term[][] {{b12, b11}, {b42}}, new Term[] {v12, v22}));
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> slv.defineFunsRec(
+                new Term[] {f12, f22}, new Term[][] {{b12, b112}, {b4}}, new Term[] {v12, v22}));
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> slv.defineFunsRec(
+                new Term[] {f12, f22}, new Term[][] {{b12, b112}, {b42}}, new Term[] {v1, v22}));
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> slv.defineFunsRec(
+                new Term[] {f12, f22}, new Term[][] {{b12, b112}, {b42}}, new Term[] {v12, v2}));
+  }
+
+  @Test void defineFunsRecWrongLogic() throws CVC5ApiException
+  {
+    d_solver.setLogic("QF_BV");
+    Sort uSort = d_solver.mkUninterpretedSort("u");
+    Sort bvSort = d_solver.mkBitVectorSort(32);
+    Sort funSort1 = d_solver.mkFunctionSort(new Sort[] {bvSort, bvSort}, bvSort);
+    Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
+    Term b = d_solver.mkVar(bvSort, "b");
+    Term u = d_solver.mkVar(uSort, "u");
+    Term v1 = d_solver.mkConst(bvSort, "v1");
+    Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
+    Term f1 = d_solver.mkConst(funSort1, "f1");
+    Term f2 = d_solver.mkConst(funSort2, "f2");
+    assertThrows(CVC5ApiException.class,
+        ()
+            -> d_solver.defineFunsRec(
+                new Term[] {f1, f2}, new Term[][] {{b, b}, {u}}, new Term[] {v1, v2}));
+  }
+
+  @Test void defineFunsRecGlobal() throws CVC5ApiException
+  {
+    Sort bSort = d_solver.getBooleanSort();
+    Sort fSort = d_solver.mkFunctionSort(bSort, bSort);
+
+    d_solver.push();
+    Term bTrue = d_solver.mkBoolean(true);
+    Term b = d_solver.mkVar(bSort, "b");
+    Term gSym = d_solver.mkConst(fSort, "g");
+    // (define-funs-rec ((g ((b Bool)) Bool)) (b))
+    d_solver.defineFunsRec(new Term[] {gSym}, new Term[][] {{b}}, new Term[] {b}, true);
+
+    // (assert (not (g true)))
+    d_solver.assertFormula(d_solver.mkTerm(APPLY_UF, gSym, bTrue).notTerm());
+    assertTrue(d_solver.checkSat().isUnsat());
+    d_solver.pop();
+    // (assert (not (g true)))
+    d_solver.assertFormula(d_solver.mkTerm(APPLY_UF, gSym, bTrue).notTerm());
+    assertTrue(d_solver.checkSat().isUnsat());
+  }
+
+  @Test void uFIteration()
+  {
+    Sort intSort = d_solver.getIntegerSort();
+    Sort funSort = d_solver.mkFunctionSort(new Sort[] {intSort, intSort}, intSort);
+    Term x = d_solver.mkConst(intSort, "x");
+    Term y = d_solver.mkConst(intSort, "y");
+    Term f = d_solver.mkConst(funSort, "f");
+    Term fxy = d_solver.mkTerm(APPLY_UF, f, x, y);
+
+    // Expecting the uninterpreted function to be one of the children
+    Term expected_children[] = new Term[] {f, x, y};
+    int idx = 0;
+    for (Term c : fxy)
+    {
+      assertEquals(c, expected_children[idx]);
+      idx++;
+    }
+  }
+
+  @Test void getInfo()
+  {
+    assertDoesNotThrow(() -> d_solver.getInfo("name"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.getInfo("asdf"));
+  }
+
+  @Test void getInterpolant() throws CVC5ApiException
+  {
+    d_solver.setLogic("QF_LIA");
+    d_solver.setOption("produce-interpols", "default");
+    d_solver.setOption("incremental", "false");
+
+    Sort intSort = d_solver.getIntegerSort();
+    Term zero = d_solver.mkInteger(0);
+    Term x = d_solver.mkConst(intSort, "x");
+    Term y = d_solver.mkConst(intSort, "y");
+    Term z = d_solver.mkConst(intSort, "z");
+
+    // Assumptions for interpolation: x + y > 0 /\ x < 0
+    d_solver.assertFormula(d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, x, y), zero));
+    d_solver.assertFormula(d_solver.mkTerm(LT, x, zero));
+    // Conjecture for interpolation: y + z > 0 \/ z < 0
+    Term conj = d_solver.mkTerm(
+        OR, d_solver.mkTerm(GT, d_solver.mkTerm(PLUS, y, z), zero), d_solver.mkTerm(LT, z, zero));
+    Term output = d_solver.getNullTerm();
+    // Call the interpolation api, while the resulting interpolant is the output
+    d_solver.getInterpolant(conj, output);
+
+    // We expect the resulting output to be a boolean formula
+    assertTrue(output.getSort().isBoolean());
+  }
+
+  @Test void getOp() throws CVC5ApiException
+  {
+    Sort bv32 = d_solver.mkBitVectorSort(32);
+    Term a = d_solver.mkConst(bv32, "a");
+    Op ext = d_solver.mkOp(BITVECTOR_EXTRACT, 2, 1);
+    Term exta = d_solver.mkTerm(ext, a);
+
+    assertFalse(a.hasOp());
+    assertThrows(CVC5ApiException.class, () -> a.getOp());
+    assertTrue(exta.hasOp());
+    assertEquals(exta.getOp(), ext);
+
+    // Test Datatypes -- more complicated
+    DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
+    DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+    cons.addSelector("head", d_solver.getIntegerSort());
+    cons.addSelectorSelf("tail");
+    consListSpec.addConstructor(cons);
+    DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+    consListSpec.addConstructor(nil);
+    Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
+    Datatype consList = consListSort.getDatatype();
+
+    Term consTerm = consList.getConstructorTerm("cons");
+    Term nilTerm = consList.getConstructorTerm("nil");
+    Term headTerm = consList.getConstructor("cons").getSelectorTerm("head");
+
+    Term listnil = d_solver.mkTerm(APPLY_CONSTRUCTOR, nilTerm);
+    Term listcons1 = d_solver.mkTerm(APPLY_CONSTRUCTOR, consTerm, d_solver.mkInteger(1), listnil);
+    Term listhead = d_solver.mkTerm(APPLY_SELECTOR, headTerm, listcons1);
+
+    assertTrue(listnil.hasOp());
+    assertTrue(listcons1.hasOp());
+    assertTrue(listhead.hasOp());
+  }
+
+  @Test void getOption()
+  {
+    assertDoesNotThrow(() -> d_solver.getOption("incremental"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.getOption("asdf"));
+  }
+
+  @Test void getUnsatAssumptions1()
+  {
+    d_solver.setOption("incremental", "false");
+    d_solver.checkSatAssuming(d_solver.mkFalse());
+    assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatAssumptions());
+  }
+
+  @Test void getUnsatAssumptions2()
+  {
+    d_solver.setOption("incremental", "true");
+    d_solver.setOption("produce-unsat-assumptions", "false");
+    d_solver.checkSatAssuming(d_solver.mkFalse());
+    assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatAssumptions());
+  }
+
+  @Test void getUnsatAssumptions3()
   {
-    d_solver.deletePointer();
+    d_solver.setOption("incremental", "true");
+    d_solver.setOption("produce-unsat-assumptions", "true");
+    d_solver.checkSatAssuming(d_solver.mkFalse());
+    assertDoesNotThrow(() -> d_solver.getUnsatAssumptions());
+    d_solver.checkSatAssuming(d_solver.mkTrue());
+    assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatAssumptions());
   }
 
-  @Test void setLogic()
+  @Test void getUnsatCore1()
+  {
+    d_solver.setOption("incremental", "false");
+    d_solver.assertFormula(d_solver.mkFalse());
+    d_solver.checkSat();
+    assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatCore());
+  }
+
+  @Test void getUnsatCore2()
+  {
+    d_solver.setOption("incremental", "false");
+    d_solver.setOption("produce-unsat-cores", "false");
+    d_solver.assertFormula(d_solver.mkFalse());
+    d_solver.checkSat();
+    assertThrows(CVC5ApiException.class, () -> d_solver.getUnsatCore());
+  }
+
+  @Test void getUnsatCore3()
+  {
+    d_solver.setOption("incremental", "true");
+    d_solver.setOption("produce-unsat-cores", "true");
+
+    Sort uSort = d_solver.mkUninterpretedSort("u");
+    Sort intSort = d_solver.getIntegerSort();
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
+    Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
+    Term[] unsat_core;
+
+    Term x = d_solver.mkConst(uSort, "x");
+    Term y = d_solver.mkConst(uSort, "y");
+    Term f = d_solver.mkConst(uToIntSort, "f");
+    Term p = d_solver.mkConst(intPredSort, "p");
+    Term zero = d_solver.mkInteger(0);
+    Term one = d_solver.mkInteger(1);
+    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+    Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+    Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+    Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+    d_solver.assertFormula(d_solver.mkTerm(GT, zero, f_x));
+    d_solver.assertFormula(d_solver.mkTerm(GT, zero, f_y));
+    d_solver.assertFormula(d_solver.mkTerm(GT, sum, one));
+    d_solver.assertFormula(p_0);
+    d_solver.assertFormula(p_f_y.notTerm());
+    assertTrue(d_solver.checkSat().isUnsat());
+
+    AtomicReference<Term[]> atomic = new AtomicReference<>();
+    assertDoesNotThrow(() -> atomic.set(d_solver.getUnsatCore()));
+    unsat_core = atomic.get();
+
+    d_solver.resetAssertions();
+    for (Term t : unsat_core)
+    {
+      d_solver.assertFormula(t);
+    }
+    Result res = d_solver.checkSat();
+    assertTrue(res.isUnsat());
+  }
+
+  @Test void getValue1()
+  {
+    d_solver.setOption("produce-models", "false");
+    Term t = d_solver.mkTrue();
+    d_solver.assertFormula(t);
+    d_solver.checkSat();
+    assertThrows(CVC5ApiException.class, () -> d_solver.getValue(t));
+  }
+
+  @Test void getValue2()
+  {
+    d_solver.setOption("produce-models", "true");
+    Term t = d_solver.mkFalse();
+    d_solver.assertFormula(t);
+    d_solver.checkSat();
+    assertThrows(CVC5ApiException.class, () -> d_solver.getValue(t));
+  }
+
+  @Test void getValue3()
+  {
+    d_solver.setOption("produce-models", "true");
+    Sort uSort = d_solver.mkUninterpretedSort("u");
+    Sort intSort = d_solver.getIntegerSort();
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
+    Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
+    Term[] unsat_core;
+
+    Term x = d_solver.mkConst(uSort, "x");
+    Term y = d_solver.mkConst(uSort, "y");
+    Term z = d_solver.mkConst(uSort, "z");
+    Term f = d_solver.mkConst(uToIntSort, "f");
+    Term p = d_solver.mkConst(intPredSort, "p");
+    Term zero = d_solver.mkInteger(0);
+    Term one = d_solver.mkInteger(1);
+    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+    Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+    Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+    Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+
+    d_solver.assertFormula(d_solver.mkTerm(LEQ, zero, f_x));
+    d_solver.assertFormula(d_solver.mkTerm(LEQ, zero, f_y));
+    d_solver.assertFormula(d_solver.mkTerm(LEQ, sum, one));
+    d_solver.assertFormula(p_0.notTerm());
+    d_solver.assertFormula(p_f_y);
+    assertTrue(d_solver.checkSat().isSat());
+    assertDoesNotThrow(() -> d_solver.getValue(x));
+    assertDoesNotThrow(() -> d_solver.getValue(y));
+    assertDoesNotThrow(() -> d_solver.getValue(z));
+    assertDoesNotThrow(() -> d_solver.getValue(sum));
+    assertDoesNotThrow(() -> d_solver.getValue(p_f_y));
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.getValue(x));
+  }
+
+  @Test void getQuantifierElimination()
+  {
+    Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
+    Term forall = d_solver.mkTerm(FORALL,
+        d_solver.mkTerm(BOUND_VAR_LIST, x),
+        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)));
+
+    assertDoesNotThrow(() -> d_solver.getQuantifierElimination(forall));
+  }
+
+  @Test void getQuantifierEliminationDisjunct()
+  {
+    Term x = d_solver.mkVar(d_solver.getBooleanSort(), "x");
+    Term forall = d_solver.mkTerm(FORALL,
+        d_solver.mkTerm(BOUND_VAR_LIST, x),
+        d_solver.mkTerm(OR, x, d_solver.mkTerm(NOT, x)));
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.getQuantifierEliminationDisjunct(d_solver.getNullTerm()));
+
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.getQuantifierEliminationDisjunct(new Solver().mkBoolean(false)));
+
+    assertDoesNotThrow(() -> d_solver.getQuantifierEliminationDisjunct(forall));
+  }
+
+  @Test void declareSeparationHeap() throws CVC5ApiException
+  {
+    d_solver.setLogic("ALL");
+    Sort integer = d_solver.getIntegerSort();
+    assertDoesNotThrow(() -> d_solver.declareSeparationHeap(integer, integer));
+    // cannot declare separation logic heap more than once
+    assertThrows(CVC5ApiException.class, () -> d_solver.declareSeparationHeap(integer, integer));
+  }
+
+  /**
+   * Helper function for testGetSeparation{Heap,Nil}TermX. Asserts and checks
+   * some simple separation logic constraints.
+   */
+
+  void checkSimpleSeparationConstraints(Solver solver)
+  {
+    Sort integer = solver.getIntegerSort();
+    // declare the separation heap
+    solver.declareSeparationHeap(integer, integer);
+    Term x = solver.mkConst(integer, "x");
+    Term p = solver.mkConst(integer, "p");
+    Term heap = solver.mkTerm(SEP_PTO, p, x);
+    solver.assertFormula(heap);
+    Term nil = solver.mkSepNil(integer);
+    solver.assertFormula(nil.eqTerm(solver.mkReal(5)));
+    solver.checkSat();
+  }
+
+  @Test void getSeparationHeapTerm1() throws CVC5ApiException
+  {
+    d_solver.setLogic("QF_BV");
+    d_solver.setOption("incremental", "false");
+    d_solver.setOption("produce-models", "true");
+    Term t = d_solver.mkTrue();
+    d_solver.assertFormula(t);
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationHeap());
+  }
+
+  @Test void getSeparationHeapTerm2() throws CVC5ApiException
+  {
+    d_solver.setLogic("ALL");
+    d_solver.setOption("incremental", "false");
+    d_solver.setOption("produce-models", "false");
+    checkSimpleSeparationConstraints(d_solver);
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationHeap());
+  }
+
+  @Test void getSeparationHeapTerm3() throws CVC5ApiException
+  {
+    d_solver.setLogic("ALL");
+    d_solver.setOption("incremental", "false");
+    d_solver.setOption("produce-models", "true");
+    Term t = d_solver.mkFalse();
+    d_solver.assertFormula(t);
+    d_solver.checkSat();
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationHeap());
+  }
+
+  @Test void getSeparationHeapTerm4() throws CVC5ApiException
+  {
+    d_solver.setLogic("ALL");
+    d_solver.setOption("incremental", "false");
+    d_solver.setOption("produce-models", "true");
+    Term t = d_solver.mkTrue();
+    d_solver.assertFormula(t);
+    d_solver.checkSat();
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationHeap());
+  }
+
+  @Test void getSeparationHeapTerm5() throws CVC5ApiException
+  {
+    d_solver.setLogic("ALL");
+    d_solver.setOption("incremental", "false");
+    d_solver.setOption("produce-models", "true");
+    checkSimpleSeparationConstraints(d_solver);
+    assertDoesNotThrow(() -> d_solver.getSeparationHeap());
+  }
+
+  @Test void getSeparationNilTerm1() throws CVC5ApiException
+  {
+    d_solver.setLogic("QF_BV");
+    d_solver.setOption("incremental", "false");
+    d_solver.setOption("produce-models", "true");
+    Term t = d_solver.mkTrue();
+    d_solver.assertFormula(t);
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationNilTerm());
+  }
+
+  @Test void getSeparationNilTerm2() throws CVC5ApiException
+  {
+    d_solver.setLogic("ALL");
+    d_solver.setOption("incremental", "false");
+    d_solver.setOption("produce-models", "false");
+    checkSimpleSeparationConstraints(d_solver);
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationNilTerm());
+  }
+
+  @Test void getSeparationNilTerm3() throws CVC5ApiException
+  {
+    d_solver.setLogic("ALL");
+    d_solver.setOption("incremental", "false");
+    d_solver.setOption("produce-models", "true");
+    Term t = d_solver.mkFalse();
+    d_solver.assertFormula(t);
+    d_solver.checkSat();
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationNilTerm());
+  }
+
+  @Test void getSeparationNilTerm4() throws CVC5ApiException
+  {
+    d_solver.setLogic("ALL");
+    d_solver.setOption("incremental", "false");
+    d_solver.setOption("produce-models", "true");
+    Term t = d_solver.mkTrue();
+    d_solver.assertFormula(t);
+    d_solver.checkSat();
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSeparationNilTerm());
+  }
+
+  @Test void getSeparationNilTerm5() throws CVC5ApiException
+  {
+    d_solver.setLogic("ALL");
+    d_solver.setOption("incremental", "false");
+    d_solver.setOption("produce-models", "true");
+    checkSimpleSeparationConstraints(d_solver);
+    assertDoesNotThrow(() -> d_solver.getSeparationNilTerm());
+  }
+
+  @Test void push1()
+  {
+    d_solver.setOption("incremental", "true");
+    assertDoesNotThrow(() -> d_solver.push(1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.setOption("incremental", "false"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.setOption("incremental", "true"));
+  }
+
+  @Test void push2()
+  {
+    d_solver.setOption("incremental", "false");
+    assertThrows(CVC5ApiException.class, () -> d_solver.push(1));
+  }
+
+  @Test void pop1()
+  {
+    d_solver.setOption("incremental", "false");
+    assertThrows(CVC5ApiException.class, () -> d_solver.pop(1));
+  }
+
+  @Test void pop2()
+  {
+    d_solver.setOption("incremental", "true");
+    assertThrows(CVC5ApiException.class, () -> d_solver.pop(1));
+  }
+
+  @Test void pop3()
+  {
+    d_solver.setOption("incremental", "true");
+    assertDoesNotThrow(() -> d_solver.push(1));
+    assertDoesNotThrow(() -> d_solver.pop(1));
+    assertThrows(CVC5ApiException.class, () -> d_solver.pop(1));
+  }
+
+  @Test void blockModel1()
+  {
+    d_solver.setOption("produce-models", "true");
+    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+    d_solver.assertFormula(x.eqTerm(x));
+    d_solver.checkSat();
+    assertThrows(CVC5ApiException.class, () -> d_solver.blockModel());
+  }
+
+  @Test void blockModel2() throws CVC5ApiException
+  {
+    d_solver.setOption("block-models", "literals");
+    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+    d_solver.assertFormula(x.eqTerm(x));
+    d_solver.checkSat();
+    assertThrows(CVC5ApiException.class, () -> d_solver.blockModel());
+  }
+
+  @Test void blockModel3() throws CVC5ApiException
+  {
+    d_solver.setOption("produce-models", "true");
+    d_solver.setOption("block-models", "literals");
+    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+    d_solver.assertFormula(x.eqTerm(x));
+    assertThrows(CVC5ApiException.class, () -> d_solver.blockModel());
+  }
+
+  @Test void blockModel4() throws CVC5ApiException
+  {
+    d_solver.setOption("produce-models", "true");
+    d_solver.setOption("block-models", "literals");
+    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+    d_solver.assertFormula(x.eqTerm(x));
+    d_solver.checkSat();
+    assertDoesNotThrow(() -> d_solver.blockModel());
+  }
+
+  @Test void blockModelValues1() throws CVC5ApiException
+  {
+    d_solver.setOption("produce-models", "true");
+    d_solver.setOption("block-models", "literals");
+    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+    d_solver.assertFormula(x.eqTerm(x));
+    d_solver.checkSat();
+    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)}));
+  }
+
+  @Test void blockModelValues2() throws CVC5ApiException
+  {
+    d_solver.setOption("produce-models", "true");
+    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+    d_solver.assertFormula(x.eqTerm(x));
+    d_solver.checkSat();
+    assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {x}));
+  }
+
+  @Test void blockModelValues3() throws CVC5ApiException
+  {
+    d_solver.setOption("block-models", "literals");
+    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+    d_solver.assertFormula(x.eqTerm(x));
+    d_solver.checkSat();
+    assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {x}));
+  }
+
+  @Test void blockModelValues4() throws CVC5ApiException
+  {
+    d_solver.setOption("produce-models", "true");
+    d_solver.setOption("block-models", "literals");
+    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+    d_solver.assertFormula(x.eqTerm(x));
+    assertThrows(CVC5ApiException.class, () -> d_solver.blockModelValues(new Term[] {x}));
+  }
+
+  @Test void blockModelValues5() throws CVC5ApiException
+  {
+    d_solver.setOption("produce-models", "true");
+    d_solver.setOption("block-models", "literals");
+    Term x = d_solver.mkConst(d_solver.getBooleanSort(), "x");
+    d_solver.assertFormula(x.eqTerm(x));
+    d_solver.checkSat();
+    assertDoesNotThrow(() -> d_solver.blockModelValues(new Term[] {x}));
+  }
+
+  @Test void setInfo() throws CVC5ApiException
+  {
+    assertThrows(CVC5ApiException.class, () -> d_solver.setInfo("cvc4-lagic", "QF_BV"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.setInfo("cvc2-logic", "QF_BV"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.setInfo("cvc4-logic", "asdf"));
+
+    assertDoesNotThrow(() -> d_solver.setInfo("source", "asdf"));
+    assertDoesNotThrow(() -> d_solver.setInfo("category", "asdf"));
+    assertDoesNotThrow(() -> d_solver.setInfo("difficulty", "asdf"));
+    assertDoesNotThrow(() -> d_solver.setInfo("filename", "asdf"));
+    assertDoesNotThrow(() -> d_solver.setInfo("license", "asdf"));
+    assertDoesNotThrow(() -> d_solver.setInfo("name", "asdf"));
+    assertDoesNotThrow(() -> d_solver.setInfo("notes", "asdf"));
+
+    assertDoesNotThrow(() -> d_solver.setInfo("smt-lib-version", "2"));
+    assertDoesNotThrow(() -> d_solver.setInfo("smt-lib-version", "2.0"));
+    assertDoesNotThrow(() -> d_solver.setInfo("smt-lib-version", "2.5"));
+    assertDoesNotThrow(() -> d_solver.setInfo("smt-lib-version", "2.6"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.setInfo("smt-lib-version", ".0"));
+
+    assertDoesNotThrow(() -> d_solver.setInfo("status", "sat"));
+    assertDoesNotThrow(() -> d_solver.setInfo("status", "unsat"));
+    assertDoesNotThrow(() -> d_solver.setInfo("status", "unknown"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.setInfo("status", "asdf"));
+  }
+
+  @Test void simplify() throws CVC5ApiException
+  {
+    assertThrows(CVC5ApiException.class, () -> d_solver.simplify(d_solver.getNullTerm()));
+
+    Sort bvSort = d_solver.mkBitVectorSort(32);
+    Sort uSort = d_solver.mkUninterpretedSort("u");
+    Sort funSort1 = d_solver.mkFunctionSort(new Sort[] {bvSort, bvSort}, bvSort);
+    Sort funSort2 = d_solver.mkFunctionSort(uSort, d_solver.getIntegerSort());
+    DatatypeDecl consListSpec = d_solver.mkDatatypeDecl("list");
+    DatatypeConstructorDecl cons = d_solver.mkDatatypeConstructorDecl("cons");
+    cons.addSelector("head", d_solver.getIntegerSort());
+    cons.addSelectorSelf("tail");
+    consListSpec.addConstructor(cons);
+    DatatypeConstructorDecl nil = d_solver.mkDatatypeConstructorDecl("nil");
+    consListSpec.addConstructor(nil);
+    Sort consListSort = d_solver.mkDatatypeSort(consListSpec);
+
+    Term x = d_solver.mkConst(bvSort, "x");
+    assertDoesNotThrow(() -> d_solver.simplify(x));
+    Term a = d_solver.mkConst(bvSort, "a");
+    assertDoesNotThrow(() -> d_solver.simplify(a));
+    Term b = d_solver.mkConst(bvSort, "b");
+    assertDoesNotThrow(() -> d_solver.simplify(b));
+    Term x_eq_x = d_solver.mkTerm(EQUAL, x, x);
+    assertDoesNotThrow(() -> d_solver.simplify(x_eq_x));
+    assertNotEquals(d_solver.mkTrue(), x_eq_x);
+    assertEquals(d_solver.mkTrue(), d_solver.simplify(x_eq_x));
+    Term x_eq_b = d_solver.mkTerm(EQUAL, x, b);
+    assertDoesNotThrow(() -> d_solver.simplify(x_eq_b));
+    assertNotEquals(d_solver.mkTrue(), x_eq_b);
+    assertNotEquals(d_solver.mkTrue(), d_solver.simplify(x_eq_b));
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.simplify(x));
+
+    Term i1 = d_solver.mkConst(d_solver.getIntegerSort(), "i1");
+    assertDoesNotThrow(() -> d_solver.simplify(i1));
+    Term i2 = d_solver.mkTerm(MULT, i1, d_solver.mkInteger("23"));
+    assertDoesNotThrow(() -> d_solver.simplify(i2));
+    assertNotEquals(i1, i2);
+    assertNotEquals(i1, d_solver.simplify(i2));
+    Term i3 = d_solver.mkTerm(PLUS, i1, d_solver.mkInteger(0));
+    assertDoesNotThrow(() -> d_solver.simplify(i3));
+    assertNotEquals(i1, i3);
+    assertEquals(i1, d_solver.simplify(i3));
+
+    Datatype consList = consListSort.getDatatype();
+    Term dt1 = d_solver.mkTerm(APPLY_CONSTRUCTOR,
+        consList.getConstructorTerm("cons"),
+        d_solver.mkInteger(0),
+        d_solver.mkTerm(APPLY_CONSTRUCTOR, consList.getConstructorTerm("nil")));
+    assertDoesNotThrow(() -> d_solver.simplify(dt1));
+    Term dt2 = d_solver.mkTerm(
+        APPLY_SELECTOR, consList.getConstructor("cons").getSelectorTerm("head"), dt1);
+    assertDoesNotThrow(() -> d_solver.simplify(dt2));
+
+    Term b1 = d_solver.mkVar(bvSort, "b1");
+    assertDoesNotThrow(() -> d_solver.simplify(b1));
+    Term b2 = d_solver.mkVar(bvSort, "b1");
+    assertDoesNotThrow(() -> d_solver.simplify(b2));
+    Term b3 = d_solver.mkVar(uSort, "b3");
+    assertDoesNotThrow(() -> d_solver.simplify(b3));
+    Term v1 = d_solver.mkConst(bvSort, "v1");
+    assertDoesNotThrow(() -> d_solver.simplify(v1));
+    Term v2 = d_solver.mkConst(d_solver.getIntegerSort(), "v2");
+    assertDoesNotThrow(() -> d_solver.simplify(v2));
+    Term f1 = d_solver.mkConst(funSort1, "f1");
+    assertDoesNotThrow(() -> d_solver.simplify(f1));
+    Term f2 = d_solver.mkConst(funSort2, "f2");
+    assertDoesNotThrow(() -> d_solver.simplify(f2));
+    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));
+  }
+
+  @Test void assertFormula()
+  {
+    assertDoesNotThrow(() -> d_solver.assertFormula(d_solver.mkTrue()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.assertFormula(d_solver.getNullTerm()));
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.assertFormula(d_solver.mkTrue()));
+  }
+
+  @Test void checkEntailed()
+  {
+    d_solver.setOption("incremental", "false");
+    assertDoesNotThrow(() -> d_solver.checkEntailed(d_solver.mkTrue()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.checkEntailed(d_solver.mkTrue()));
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue()));
+  }
+
+  @Test void checkEntailed1()
+  {
+    Sort boolSort = d_solver.getBooleanSort();
+    Term x = d_solver.mkConst(boolSort, "x");
+    Term y = d_solver.mkConst(boolSort, "y");
+    Term z = d_solver.mkTerm(AND, x, y);
+    d_solver.setOption("incremental", "true");
+    assertDoesNotThrow(() -> d_solver.checkEntailed(d_solver.mkTrue()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.checkEntailed(d_solver.getNullTerm()));
+    assertDoesNotThrow(() -> d_solver.checkEntailed(d_solver.mkTrue()));
+    assertDoesNotThrow(() -> d_solver.checkEntailed(z));
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue()));
+  }
+
+  @Test void checkEntailed2()
+  {
+    d_solver.setOption("incremental", "true");
+
+    Sort uSort = d_solver.mkUninterpretedSort("u");
+    Sort intSort = d_solver.getIntegerSort();
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
+    Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
+
+    Term n = d_solver.getNullTerm();
+    // Constants
+    Term x = d_solver.mkConst(uSort, "x");
+    Term y = d_solver.mkConst(uSort, "y");
+    // Functions
+    Term f = d_solver.mkConst(uToIntSort, "f");
+    Term p = d_solver.mkConst(intPredSort, "p");
+    // Values
+    Term zero = d_solver.mkInteger(0);
+    Term one = d_solver.mkInteger(1);
+    // Terms
+    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+    Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+    Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+    Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+    // Assertions
+    Term assertions = d_solver.mkTerm(AND,
+        new Term[] {
+            d_solver.mkTerm(LEQ, zero, f_x), // 0 <= f(x)
+            d_solver.mkTerm(LEQ, zero, f_y), // 0 <= f(y)
+            d_solver.mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1
+            p_0.notTerm(), // not p(0)
+            p_f_y // p(f(y))
+        });
+
+    assertDoesNotThrow(() -> d_solver.checkEntailed(d_solver.mkTrue()));
+    d_solver.assertFormula(assertions);
+    assertDoesNotThrow(() -> d_solver.checkEntailed(d_solver.mkTerm(DISTINCT, x, y)));
+    assertDoesNotThrow(()
+                           -> d_solver.checkEntailed(
+                               new Term[] {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, x, y)}));
+    assertThrows(CVC5ApiException.class, () -> d_solver.checkEntailed(n));
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.checkEntailed(new Term[] {n, d_solver.mkTerm(DISTINCT, x, y)}));
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.checkEntailed(d_solver.mkTrue()));
+  }
+
+  @Test void checkSat() throws CVC5ApiException
+  {
+    d_solver.setOption("incremental", "false");
+    assertDoesNotThrow(() -> d_solver.checkSat());
+    assertThrows(CVC5ApiException.class, () -> d_solver.checkSat());
+  }
+
+  @Test void checkSatAssuming() throws CVC5ApiException
+  {
+    d_solver.setOption("incremental", "false");
+    assertDoesNotThrow(() -> d_solver.checkSatAssuming(d_solver.mkTrue()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.checkSatAssuming(d_solver.mkTrue()));
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue()));
+  }
+
+  @Test void checkSatAssuming1() throws CVC5ApiException
+  {
+    Sort boolSort = d_solver.getBooleanSort();
+    Term x = d_solver.mkConst(boolSort, "x");
+    Term y = d_solver.mkConst(boolSort, "y");
+    Term z = d_solver.mkTerm(AND, x, y);
+    d_solver.setOption("incremental", "true");
+    assertDoesNotThrow(() -> d_solver.checkSatAssuming(d_solver.mkTrue()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.checkSatAssuming(d_solver.getNullTerm()));
+    assertDoesNotThrow(() -> d_solver.checkSatAssuming(d_solver.mkTrue()));
+    assertDoesNotThrow(() -> d_solver.checkSatAssuming(z));
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue()));
+  }
+
+  @Test void checkSatAssuming2() throws CVC5ApiException
+  {
+    d_solver.setOption("incremental", "true");
+
+    Sort uSort = d_solver.mkUninterpretedSort("u");
+    Sort intSort = d_solver.getIntegerSort();
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort uToIntSort = d_solver.mkFunctionSort(uSort, intSort);
+    Sort intPredSort = d_solver.mkFunctionSort(intSort, boolSort);
+
+    Term n = d_solver.getNullTerm();
+    // Constants
+    Term x = d_solver.mkConst(uSort, "x");
+    Term y = d_solver.mkConst(uSort, "y");
+    // Functions
+    Term f = d_solver.mkConst(uToIntSort, "f");
+    Term p = d_solver.mkConst(intPredSort, "p");
+    // Values
+    Term zero = d_solver.mkInteger(0);
+    Term one = d_solver.mkInteger(1);
+    // Terms
+    Term f_x = d_solver.mkTerm(APPLY_UF, f, x);
+    Term f_y = d_solver.mkTerm(APPLY_UF, f, y);
+    Term sum = d_solver.mkTerm(PLUS, f_x, f_y);
+    Term p_0 = d_solver.mkTerm(APPLY_UF, p, zero);
+    Term p_f_y = d_solver.mkTerm(APPLY_UF, p, f_y);
+    // Assertions
+    Term assertions = d_solver.mkTerm(AND,
+        new Term[] {
+            d_solver.mkTerm(LEQ, zero, f_x), // 0 <= f(x)
+            d_solver.mkTerm(LEQ, zero, f_y), // 0 <= f(y)
+            d_solver.mkTerm(LEQ, sum, one), // f(x) + f(y) <= 1
+            p_0.notTerm(), // not p(0)
+            p_f_y // p(f(y))
+        });
+
+    assertDoesNotThrow(() -> d_solver.checkSatAssuming(d_solver.mkTrue()));
+    d_solver.assertFormula(assertions);
+    assertDoesNotThrow(() -> d_solver.checkSatAssuming(d_solver.mkTerm(DISTINCT, x, y)));
+    assertDoesNotThrow(()
+                           -> d_solver.checkSatAssuming(
+                               new Term[] {d_solver.mkFalse(), d_solver.mkTerm(DISTINCT, x, y)}));
+    assertThrows(CVC5ApiException.class, () -> d_solver.checkSatAssuming(n));
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.checkSatAssuming(new Term[] {n, d_solver.mkTerm(DISTINCT, x, y)}));
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.checkSatAssuming(d_solver.mkTrue()));
+  }
+
+  @Test void setLogic() throws CVC5ApiException
   {
     assertDoesNotThrow(() -> d_solver.setLogic("AUFLIRA"));
-    assertThrows(CVC5ApiException.class, () -> d_solver.setLogic("AF_BV"));    
+    assertThrows(CVC5ApiException.class, () -> d_solver.setLogic("AF_BV"));
+    d_solver.assertFormula(d_solver.mkTrue());
+    assertThrows(CVC5ApiException.class, () -> d_solver.setLogic("AUFLIRA"));
+  }
+
+  @Test void setOption() throws CVC5ApiException
+  {
+    assertDoesNotThrow(() -> d_solver.setOption("bv-sat-solver", "minisat"));
+    assertThrows(CVC5ApiException.class, () -> d_solver.setOption("bv-sat-solver", "1"));
+    d_solver.assertFormula(d_solver.mkTrue());
+    assertThrows(CVC5ApiException.class, () -> d_solver.setOption("bv-sat-solver", "minisat"));
+  }
+
+  @Test void resetAssertions() throws CVC5ApiException
+  {
+    d_solver.setOption("incremental", "true");
+
+    Sort bvSort = d_solver.mkBitVectorSort(4);
+    Term one = d_solver.mkBitVector(4, 1);
+    Term x = d_solver.mkConst(bvSort, "x");
+    Term ule = d_solver.mkTerm(BITVECTOR_ULE, x, one);
+    Term srem = d_solver.mkTerm(BITVECTOR_SREM, one, x);
+    d_solver.push(4);
+    Term slt = d_solver.mkTerm(BITVECTOR_SLT, srem, one);
+    d_solver.resetAssertions();
+    d_solver.checkSatAssuming(new Term[] {slt, ule});
+  }
+
+  @Test void mkSygusVar() throws CVC5ApiException
+  {
+    Sort boolSort = d_solver.getBooleanSort();
+    Sort intSort = d_solver.getIntegerSort();
+    Sort funSort = d_solver.mkFunctionSort(intSort, boolSort);
+
+    assertDoesNotThrow(() -> d_solver.mkSygusVar(boolSort));
+    assertDoesNotThrow(() -> d_solver.mkSygusVar(funSort));
+    assertDoesNotThrow(() -> d_solver.mkSygusVar(boolSort, ("b")));
+    assertDoesNotThrow(() -> d_solver.mkSygusVar(funSort, ""));
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkSygusVar(d_solver.getNullSort()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.mkSygusVar(d_solver.getNullSort(), "a"));
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.mkSygusVar(boolSort));
+  }
+
+  @Test void mkSygusGrammar() throws CVC5ApiException
+  {
+    Term nullTerm = d_solver.getNullTerm();
+    Term boolTerm = d_solver.mkBoolean(true);
+    Term boolVar = d_solver.mkVar(d_solver.getBooleanSort());
+    Term intVar = d_solver.mkVar(d_solver.getIntegerSort());
+
+    assertDoesNotThrow(() -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {intVar}));
+    assertDoesNotThrow(() -> d_solver.mkSygusGrammar(new Term[] {boolVar}, new Term[] {intVar}));
+
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {}));
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {nullTerm}));
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkSygusGrammar(new Term[] {}, new Term[] {boolTerm}));
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkSygusGrammar(new Term[] {boolTerm}, new Term[] {intVar}));
+
+    Solver slv = new Solver();
+    Term boolVar2 = slv.mkVar(slv.getBooleanSort());
+    Term intVar2 = slv.mkVar(slv.getIntegerSort());
+    assertDoesNotThrow(() -> slv.mkSygusGrammar(new Term[] {boolVar2}, new Term[] {intVar2}));
+
+    assertThrows(CVC5ApiException.class,
+        () -> slv.mkSygusGrammar(new Term[] {boolVar}, new Term[] {intVar2}));
+    assertThrows(CVC5ApiException.class,
+        () -> slv.mkSygusGrammar(new Term[] {boolVar2}, new Term[] {intVar}));
+  }
+
+  @Test void synthFun() throws CVC5ApiException
+  {
+    Sort nullSort = d_solver.getNullSort();
+    Sort bool = d_solver.getBooleanSort();
+    Sort integer = d_solver.getIntegerSort();
+
+    Term nullTerm = d_solver.getNullTerm();
+    Term x = d_solver.mkVar(bool);
+
+    Term start1 = d_solver.mkVar(bool);
+    Term start2 = d_solver.mkVar(integer);
+
+    Grammar g1 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start1});
+    g1.addRule(start1, d_solver.mkBoolean(false));
+
+    Grammar g2 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start2});
+    g2.addRule(start2, d_solver.mkInteger(0));
+
+    assertDoesNotThrow(() -> d_solver.synthFun("", new Term[] {}, bool));
+    assertDoesNotThrow(() -> d_solver.synthFun("f1", new Term[] {x}, bool));
+    assertDoesNotThrow(() -> d_solver.synthFun("f2", new Term[] {x}, bool, g1));
+
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.synthFun("f3", new Term[] {nullTerm}, bool));
+    assertThrows(CVC5ApiException.class, () -> d_solver.synthFun("f4", new Term[] {}, nullSort));
+    assertThrows(CVC5ApiException.class, () -> d_solver.synthFun("f6", new Term[] {x}, bool, g2));
+
+    Solver slv = new Solver();
+    Term x2 = slv.mkVar(slv.getBooleanSort());
+    assertDoesNotThrow(() -> slv.synthFun("f1", new Term[] {x2}, slv.getBooleanSort()));
+
+    assertThrows(
+        CVC5ApiException.class, () -> slv.synthFun("", new Term[] {}, d_solver.getBooleanSort()));
+    assertThrows(CVC5ApiException.class,
+        () -> slv.synthFun("f1", new Term[] {x}, d_solver.getBooleanSort()));
+  }
+
+  @Test void synthInv() throws CVC5ApiException
+  {
+    Sort bool = d_solver.getBooleanSort();
+    Sort integer = d_solver.getIntegerSort();
+
+    Term nullTerm = d_solver.getNullTerm();
+    Term x = d_solver.mkVar(bool);
+
+    Term start1 = d_solver.mkVar(bool);
+    Term start2 = d_solver.mkVar(integer);
+
+    Grammar g1 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start1});
+    g1.addRule(start1, d_solver.mkBoolean(false));
+
+    Grammar g2 = d_solver.mkSygusGrammar(new Term[] {x}, new Term[] {start2});
+    g2.addRule(start2, d_solver.mkInteger(0));
+
+    assertDoesNotThrow(() -> d_solver.synthInv("", new Term[] {}));
+    assertDoesNotThrow(() -> d_solver.synthInv("i1", new Term[] {x}));
+    assertDoesNotThrow(() -> d_solver.synthInv("i2", new Term[] {x}, g1));
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.synthInv("i3", new Term[] {nullTerm}));
+    assertThrows(CVC5ApiException.class, () -> d_solver.synthInv("i4", new Term[] {x}, g2));
+  }
+
+  @Test void addSygusConstraint() throws CVC5ApiException
+  {
+    Term nullTerm = d_solver.getNullTerm();
+    Term boolTerm = d_solver.mkBoolean(true);
+    Term intTerm = d_solver.mkInteger(1);
+
+    assertDoesNotThrow(() -> d_solver.addSygusConstraint(boolTerm));
+    assertThrows(CVC5ApiException.class, () -> d_solver.addSygusConstraint(nullTerm));
+    assertThrows(CVC5ApiException.class, () -> d_solver.addSygusConstraint(intTerm));
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.addSygusConstraint(boolTerm));
+  }
+
+  @Test void addSygusInvConstraint() throws CVC5ApiException
+  {
+    Sort bool = d_solver.getBooleanSort();
+    Sort real = d_solver.getRealSort();
+
+    Term nullTerm = d_solver.getNullTerm();
+    Term intTerm = d_solver.mkInteger(1);
+
+    Term inv = d_solver.declareFun("inv", new Sort[] {real}, bool);
+    Term pre = d_solver.declareFun("pre", new Sort[] {real}, bool);
+    Term trans = d_solver.declareFun("trans", new Sort[] {real, real}, bool);
+    Term post = d_solver.declareFun("post", new Sort[] {real}, bool);
+
+    Term inv1 = d_solver.declareFun("inv1", new Sort[] {real}, real);
+
+    Term trans1 = d_solver.declareFun("trans1", new Sort[] {bool, real}, bool);
+    Term trans2 = d_solver.declareFun("trans2", new Sort[] {real, bool}, bool);
+    Term trans3 = d_solver.declareFun("trans3", new Sort[] {real, real}, real);
+
+    assertDoesNotThrow(() -> d_solver.addSygusInvConstraint(inv, pre, trans, post));
+
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(nullTerm, pre, trans, post));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, nullTerm, trans, post));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, pre, nullTerm, post));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, pre, trans, nullTerm));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(intTerm, pre, trans, post));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv1, pre, trans, post));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, trans, trans, post));
+    assertThrows(CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, pre, pre, post));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, pre, trans1, post));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, pre, trans2, post));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, pre, trans3, post));
+    assertThrows(
+        CVC5ApiException.class, () -> d_solver.addSygusInvConstraint(inv, pre, trans, trans));
+
+    Solver slv = new Solver();
+    Sort boolean2 = slv.getBooleanSort();
+    Sort real2 = slv.getRealSort();
+    Term inv22 = slv.declareFun("inv", new Sort[] {real2}, boolean2);
+    Term pre22 = slv.declareFun("pre", new Sort[] {real2}, boolean2);
+    Term trans22 = slv.declareFun("trans", new Sort[] {real2, real2}, boolean2);
+    Term post22 = slv.declareFun("post", new Sort[] {real2}, boolean2);
+    assertDoesNotThrow(() -> slv.addSygusInvConstraint(inv22, pre22, trans22, post22));
+
+    assertThrows(
+        CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv, pre22, trans22, post22));
+    assertThrows(
+        CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv22, pre, trans22, post22));
+    assertThrows(
+        CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv22, pre22, trans, post22));
+    assertThrows(
+        CVC5ApiException.class, () -> slv.addSygusInvConstraint(inv22, pre22, trans22, post));
+  }
+
+  @Test void getSynthSolution() throws CVC5ApiException
+  {
+    d_solver.setOption("lang", "sygus2");
+    d_solver.setOption("incremental", "false");
+
+    Term nullTerm = d_solver.getNullTerm();
+    Term x = d_solver.mkBoolean(false);
+    Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolution(f));
+
+    d_solver.checkSynth();
+
+    assertDoesNotThrow(() -> d_solver.getSynthSolution(f));
+    assertDoesNotThrow(() -> d_solver.getSynthSolution(f));
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolution(nullTerm));
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolution(x));
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.getSynthSolution(f));
+  }
+
+  @Test void getSynthSolutions() throws CVC5ApiException
+  {
+    d_solver.setOption("lang", "sygus2");
+    d_solver.setOption("incremental", "false");
+
+    Term nullTerm = d_solver.getNullTerm();
+    Term x = d_solver.mkBoolean(false);
+    Term f = d_solver.synthFun("f", new Term[] {}, d_solver.getBooleanSort());
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolutions(new Term[] {}));
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolutions(new Term[] {f}));
+
+    d_solver.checkSynth();
+
+    assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f}));
+    assertDoesNotThrow(() -> d_solver.getSynthSolutions(new Term[] {f, f}));
+
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolutions(new Term[] {}));
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolutions(new Term[] {nullTerm}));
+    assertThrows(CVC5ApiException.class, () -> d_solver.getSynthSolutions(new Term[] {x}));
+
+    Solver slv = new Solver();
+    assertThrows(CVC5ApiException.class, () -> slv.getSynthSolutions(new Term[] {x}));
+  }
+
+  @Test void tupleProject() throws CVC5ApiException
+  {
+    Sort[] sorts = new Sort[] {d_solver.getBooleanSort(),
+        d_solver.getIntegerSort(),
+        d_solver.getStringSort(),
+        d_solver.mkSetSort(d_solver.getStringSort())};
+    Term[] elements = new Term[] {d_solver.mkBoolean(true),
+        d_solver.mkInteger(3),
+        d_solver.mkString("C"),
+        d_solver.mkTerm(SINGLETON, d_solver.mkString("Z"))};
+
+    Term tuple = d_solver.mkTuple(sorts, elements);
+
+    int[] indices1 = new int[] {};
+    int[] indices2 = new int[] {0};
+    int[] indices3 = new int[] {0, 1};
+    int[] indices4 = new int[] {0, 0, 2, 2, 3, 3, 0};
+    int[] indices5 = new int[] {4};
+    int[] indices6 = new int[] {0, 4};
+
+    assertDoesNotThrow(() -> d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices1), tuple));
+    assertDoesNotThrow(() -> d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices2), tuple));
+    assertDoesNotThrow(() -> d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices3), tuple));
+    assertDoesNotThrow(() -> d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices4), tuple));
+
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices5), tuple));
+    assertThrows(CVC5ApiException.class,
+        () -> d_solver.mkTerm(d_solver.mkOp(TUPLE_PROJECT, indices6), tuple));
+
+    int[] indices = new int[] {0, 3, 2, 0, 1, 2};
+
+    Op op = d_solver.mkOp(TUPLE_PROJECT, indices);
+    Term projection = d_solver.mkTerm(op, tuple);
+
+    Datatype datatype = tuple.getSort().getDatatype();
+    DatatypeConstructor constructor = datatype.getConstructor(0);
+
+    for (int i = 0; i < indices.length; i++)
+    {
+      Term selectorTerm = constructor.getSelector(indices[i]).getSelectorTerm();
+      Term selectedTerm = d_solver.mkTerm(APPLY_SELECTOR, selectorTerm, tuple);
+      Term simplifiedTerm = d_solver.simplify(selectedTerm);
+      assertEquals(elements[indices[i]], simplifiedTerm);
+    }
+
+    assertEquals("((_ tuple_project 0 3 2 0 1 2) (mkTuple true 3 \"C\" (singleton "
+            + "\"Z\")))",
+        projection.toString());
   }
-}
+}
\ No newline at end of file
diff --git a/test/unit/api/java/cvc5/SortTest.java b/test/unit/api/java/cvc5/SortTest.java
index a937e4dfc..f2f9edaed 100644
--- a/test/unit/api/java/cvc5/SortTest.java
+++ b/test/unit/api/java/cvc5/SortTest.java
@@ -64,7 +64,7 @@ class SortTest
   {
     assertDoesNotThrow(() -> d_solver.getIntegerSort() == d_solver.getNullSort());
     assertDoesNotThrow(() -> d_solver.getIntegerSort() != d_solver.getNullSort());
-    assertDoesNotThrow(() -> d_solver.getIntegerSort().compareTo(d_solver.getNullSort()));    
+    assertDoesNotThrow(() -> d_solver.getIntegerSort().compareTo(d_solver.getNullSort()));
   }
 
   @Test void isBoolean()
@@ -101,11 +101,8 @@ class SortTest
 
   @Test void isRoundingMode() throws CVC5ApiException
   {
-    if (d_solver.supportsFloatingPoint())
-    {
-      assertTrue(d_solver.getRoundingModeSort().isRoundingMode());
-      assertDoesNotThrow(() -> d_solver.getNullSort().isRoundingMode());
-    }
+    assertTrue(d_solver.getRoundingModeSort().isRoundingMode());
+    assertDoesNotThrow(() -> d_solver.getNullSort().isRoundingMode());
   }
 
   @Test void isBitVector() throws CVC5ApiException
@@ -116,11 +113,8 @@ class SortTest
 
   @Test void isFloatingPoint() throws CVC5ApiException
   {
-    if (d_solver.supportsFloatingPoint())
-    {
-      assertTrue(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint());
-      assertDoesNotThrow(() -> d_solver.getNullSort().isFloatingPoint());
-    }
+    assertTrue(d_solver.mkFloatingPointSort(8, 24).isFloatingPoint());
+    assertDoesNotThrow(() -> d_solver.getNullSort().isFloatingPoint());
   }
 
   @Test void isDatatype() throws CVC5ApiException
@@ -474,24 +468,18 @@ class SortTest
 
   @Test void getFPExponentSize() throws CVC5ApiException
   {
-    if (d_solver.supportsFloatingPoint())
-    {
-      Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
-      assertDoesNotThrow(() -> fpSort.getFPExponentSize());
-      Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-      assertThrows(CVC5ApiException.class, () -> setSort.getFPExponentSize());
-    }
+    Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
+    assertDoesNotThrow(() -> fpSort.getFPExponentSize());
+    Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+    assertThrows(CVC5ApiException.class, () -> setSort.getFPExponentSize());
   }
 
   @Test void getFPSignificandSize() throws CVC5ApiException
   {
-    if (d_solver.supportsFloatingPoint())
-    {
-      Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
-      assertDoesNotThrow(() -> fpSort.getFPSignificandSize());
-      Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
-      assertThrows(CVC5ApiException.class, () -> setSort.getFPSignificandSize());
-    }
+    Sort fpSort = d_solver.mkFloatingPointSort(4, 8);
+    assertDoesNotThrow(() -> fpSort.getFPSignificandSize());
+    Sort setSort = d_solver.mkSetSort(d_solver.getIntegerSort());
+    assertThrows(CVC5ApiException.class, () -> setSort.getFPSignificandSize());
   }
 
   @Test void getDatatypeParamSorts() throws CVC5ApiException
diff --git a/test/unit/api/java/cvc5/TermTest.java b/test/unit/api/java/cvc5/TermTest.java
index d5491e0e7..508e264e3 100644
--- a/test/unit/api/java/cvc5/TermTest.java
+++ b/test/unit/api/java/cvc5/TermTest.java
@@ -27,16 +27,17 @@ import org.junit.jupiter.api.AfterEach;
 import org.junit.jupiter.api.BeforeEach;
 import org.junit.jupiter.api.Test;
 
-class TermTest {
+class TermTest
+{
   private Solver d_solver;
 
-  @BeforeEach
-  void setUp() {
+  @BeforeEach void setUp()
+  {
     d_solver = new Solver();
   }
 
-  @Test
-  void eq() {
+  @Test void eq()
+  {
     Sort uSort = d_solver.mkUninterpretedSort("u");
     Term x = d_solver.mkVar(uSort, "x");
     Term y = d_solver.mkVar(uSort, "y");
@@ -50,8 +51,8 @@ class TermTest {
     assertTrue(x != z);
   }
 
-  @Test
-  void getId() {
+  @Test void getId()
+  {
     Term n = d_solver.getNullTerm();
     assertThrows(CVC5ApiException.class, () -> n.getId());
     Term x = d_solver.mkVar(d_solver.getIntegerSort(), "x");
@@ -63,8 +64,8 @@ class TermTest {
     assertNotEquals(x.getId(), z.getId());
   }
 
-  @Test
-  void getKind() throws CVC5ApiException {
+  @Test void getKind() throws CVC5ApiException
+  {
     Sort uSort = d_solver.mkUninterpretedSort("u");
     Sort intSort = d_solver.getIntegerSort();
     Sort boolSort = d_solver.getBooleanSort();
@@ -105,8 +106,8 @@ class TermTest {
     assertEquals(ss.getKind(), SEQ_CONCAT);
   }
 
-  @Test
-  void getSort() throws CVC5ApiException {
+  @Test void getSort() throws CVC5ApiException
+  {
     Sort bvSort = d_solver.mkBitVectorSort(8);
     Sort intSort = d_solver.getIntegerSort();
     Sort boolSort = d_solver.getBooleanSort();
@@ -150,8 +151,8 @@ class TermTest {
     assertEquals(p_f_y.getSort(), boolSort);
   }
 
-  @Test
-  void getOp() throws CVC5ApiException {
+  @Test void getOp() throws CVC5ApiException
+  {
     Sort intsort = d_solver.getIntegerSort();
     Sort bvsort = d_solver.mkBitVectorSort(8);
     Sort arrsort = d_solver.mkArraySort(bvsort, intsort);
@@ -184,7 +185,8 @@ class TermTest {
     List<Term> children = new ArrayList();
 
     Iterator<Term> iterator = fx.iterator();
-    for (Term t : fx) {
+    for (Term t : fx)
+    {
       children.add(t);
     }
 
@@ -201,8 +203,7 @@ class TermTest {
     listDecl.addConstructor(cons);
     listDecl.addConstructor(nil);
     Sort listSort = d_solver.mkDatatypeSort(listDecl);
-    Sort intListSort =
-        listSort.instantiate(new Sort[] {d_solver.getIntegerSort()});
+    Sort intListSort = listSort.instantiate(new Sort[] {d_solver.getIntegerSort()});
     Term c = d_solver.mkConst(intListSort, "c");
     Datatype list = listSort.getDatatype();
     // list datatype constructor and selector operator terms
@@ -210,24 +211,23 @@ class TermTest {
     Term nilOpTerm = list.getConstructorTerm("nil");
   }
 
-  @Test
-  void isNull() throws CVC5ApiException {
+  @Test void isNull() throws CVC5ApiException
+  {
     Term x = d_solver.getNullTerm();
     assertTrue(x.isNull());
     x = d_solver.mkVar(d_solver.mkBitVectorSort(4), "x");
     assertFalse(x.isNull());
   }
 
-  @Test
-  void notTerm() throws CVC5ApiException {
+  @Test void notTerm() throws CVC5ApiException
+  {
     Sort bvSort = d_solver.mkBitVectorSort(8);
     Sort intSort = d_solver.getIntegerSort();
     Sort boolSort = d_solver.getBooleanSort();
     Sort funSort1 = d_solver.mkFunctionSort(bvSort, intSort);
     Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.getNullTerm().notTerm());
+    assertThrows(CVC5ApiException.class, () -> d_solver.getNullTerm().notTerm());
     Term b = d_solver.mkTrue();
     assertDoesNotThrow(() -> b.notTerm());
     Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
@@ -248,8 +248,8 @@ class TermTest {
     assertDoesNotThrow(() -> p_f_x.notTerm());
   }
 
-  @Test
-  void andTerm() throws CVC5ApiException {
+  @Test void andTerm() throws CVC5ApiException
+  {
     Sort bvSort = d_solver.mkBitVectorSort(8);
     Sort intSort = d_solver.getIntegerSort();
     Sort boolSort = d_solver.getBooleanSort();
@@ -257,10 +257,8 @@ class TermTest {
     Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
     Term b = d_solver.mkTrue();
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.getNullTerm().andTerm(b));
-    assertThrows(
-        CVC5ApiException.class, () -> b.andTerm(d_solver.getNullTerm()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.getNullTerm().andTerm(b));
+    assertThrows(CVC5ApiException.class, () -> b.andTerm(d_solver.getNullTerm()));
     assertDoesNotThrow(() -> b.andTerm(b));
     Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
     assertThrows(CVC5ApiException.class, () -> x.andTerm(b));
@@ -316,8 +314,8 @@ class TermTest {
     assertDoesNotThrow(() -> p_f_x.andTerm(p_f_x));
   }
 
-  @Test
-  void orTerm() throws CVC5ApiException {
+  @Test void orTerm() throws CVC5ApiException
+  {
     Sort bvSort = d_solver.mkBitVectorSort(8);
     Sort intSort = d_solver.getIntegerSort();
     Sort boolSort = d_solver.getBooleanSort();
@@ -325,10 +323,8 @@ class TermTest {
     Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
     Term b = d_solver.mkTrue();
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.getNullTerm().orTerm(b));
-    assertThrows(
-        CVC5ApiException.class, () -> b.orTerm(d_solver.getNullTerm()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.getNullTerm().orTerm(b));
+    assertThrows(CVC5ApiException.class, () -> b.orTerm(d_solver.getNullTerm()));
     assertDoesNotThrow(() -> b.orTerm(b));
     Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
     assertThrows(CVC5ApiException.class, () -> x.orTerm(b));
@@ -384,8 +380,8 @@ class TermTest {
     assertDoesNotThrow(() -> p_f_x.orTerm(p_f_x));
   }
 
-  @Test
-  void xorTerm() throws CVC5ApiException {
+  @Test void xorTerm() throws CVC5ApiException
+  {
     Sort bvSort = d_solver.mkBitVectorSort(8);
     Sort intSort = d_solver.getIntegerSort();
     Sort boolSort = d_solver.getBooleanSort();
@@ -393,10 +389,8 @@ class TermTest {
     Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
     Term b = d_solver.mkTrue();
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.getNullTerm().xorTerm(b));
-    assertThrows(
-        CVC5ApiException.class, () -> b.xorTerm(d_solver.getNullTerm()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.getNullTerm().xorTerm(b));
+    assertThrows(CVC5ApiException.class, () -> b.xorTerm(d_solver.getNullTerm()));
     assertDoesNotThrow(() -> b.xorTerm(b));
     Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
     assertThrows(CVC5ApiException.class, () -> x.xorTerm(b));
@@ -452,8 +446,8 @@ class TermTest {
     assertDoesNotThrow(() -> p_f_x.xorTerm(p_f_x));
   }
 
-  @Test
-  void eqTerm() throws CVC5ApiException {
+  @Test void eqTerm() throws CVC5ApiException
+  {
     Sort bvSort = d_solver.mkBitVectorSort(8);
     Sort intSort = d_solver.getIntegerSort();
     Sort boolSort = d_solver.getBooleanSort();
@@ -461,10 +455,8 @@ class TermTest {
     Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
     Term b = d_solver.mkTrue();
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.getNullTerm().eqTerm(b));
-    assertThrows(
-        CVC5ApiException.class, () -> b.eqTerm(d_solver.getNullTerm()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.getNullTerm().eqTerm(b));
+    assertThrows(CVC5ApiException.class, () -> b.eqTerm(d_solver.getNullTerm()));
     assertDoesNotThrow(() -> b.eqTerm(b));
     Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
     assertThrows(CVC5ApiException.class, () -> x.eqTerm(b));
@@ -520,8 +512,8 @@ class TermTest {
     assertDoesNotThrow(() -> p_f_x.eqTerm(p_f_x));
   }
 
-  @Test
-  void impTerm() throws CVC5ApiException {
+  @Test void impTerm() throws CVC5ApiException
+  {
     Sort bvSort = d_solver.mkBitVectorSort(8);
     Sort intSort = d_solver.getIntegerSort();
     Sort boolSort = d_solver.getBooleanSort();
@@ -529,10 +521,8 @@ class TermTest {
     Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
     Term b = d_solver.mkTrue();
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.getNullTerm().impTerm(b));
-    assertThrows(
-        CVC5ApiException.class, () -> b.impTerm(d_solver.getNullTerm()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.getNullTerm().impTerm(b));
+    assertThrows(CVC5ApiException.class, () -> b.impTerm(d_solver.getNullTerm()));
     assertDoesNotThrow(() -> b.impTerm(b));
     Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
     assertThrows(CVC5ApiException.class, () -> x.impTerm(b));
@@ -588,8 +578,8 @@ class TermTest {
     assertDoesNotThrow(() -> p_f_x.impTerm(p_f_x));
   }
 
-  @Test
-  void iteTerm() throws CVC5ApiException {
+  @Test void iteTerm() throws CVC5ApiException
+  {
     Sort bvSort = d_solver.mkBitVectorSort(8);
     Sort intSort = d_solver.getIntegerSort();
     Sort boolSort = d_solver.getBooleanSort();
@@ -597,12 +587,9 @@ class TermTest {
     Sort funSort2 = d_solver.mkFunctionSort(intSort, boolSort);
 
     Term b = d_solver.mkTrue();
-    assertThrows(
-        CVC5ApiException.class, () -> d_solver.getNullTerm().iteTerm(b, b));
-    assertThrows(
-        CVC5ApiException.class, () -> b.iteTerm(d_solver.getNullTerm(), b));
-    assertThrows(
-        CVC5ApiException.class, () -> b.iteTerm(b, d_solver.getNullTerm()));
+    assertThrows(CVC5ApiException.class, () -> d_solver.getNullTerm().iteTerm(b, b));
+    assertThrows(CVC5ApiException.class, () -> b.iteTerm(d_solver.getNullTerm(), b));
+    assertThrows(CVC5ApiException.class, () -> b.iteTerm(b, d_solver.getNullTerm()));
     assertDoesNotThrow(() -> b.iteTerm(b, b));
     Term x = d_solver.mkVar(d_solver.mkBitVectorSort(8), "x");
     assertDoesNotThrow(() -> b.iteTerm(x, x));
@@ -635,30 +622,27 @@ class TermTest {
     assertThrows(CVC5ApiException.class, () -> p_f_x.iteTerm(x, b));
   }
 
-  @Test
-  void termAssignment() {
+  @Test void termAssignment()
+  {
     Term t1 = d_solver.mkInteger(1);
     Term t2 = t1;
     t2 = d_solver.mkInteger(2);
     assertEquals(t1, d_solver.mkInteger(1));
   }
 
-  @Test
-  void termCompare() {
+  @Test void termCompare()
+  {
     Term t1 = d_solver.mkInteger(1);
-    Term t2 =
-        d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
-    Term t3 =
-        d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
+    Term t2 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
+    Term t3 = d_solver.mkTerm(PLUS, d_solver.mkInteger(2), d_solver.mkInteger(2));
     assertTrue(t2.compareTo(t3) >= 0);
     assertTrue(t2.compareTo(t3) <= 0);
     assertTrue((t1.compareTo(t2) > 0) != (t1.compareTo(t2) < 0));
-    assertTrue(
-        (t1.compareTo(t2) > 0 || t1.equals(t2)) == (t1.compareTo(t2) >= 0));
+    assertTrue((t1.compareTo(t2) > 0 || t1.equals(t2)) == (t1.compareTo(t2) >= 0));
   }
 
-  @Test
-  void termChildren() throws CVC5ApiException {
+  @Test void termChildren() throws CVC5ApiException
+  {
     // simple term 2+3
     Term two = d_solver.mkInteger(2);
     Term t1 = d_solver.mkTerm(PLUS, two, d_solver.mkInteger(3));
@@ -679,8 +663,8 @@ class TermTest {
     assertThrows(CVC5ApiException.class, () -> tnull.getChild(0));
   }
 
-  @Test
-  void getInteger() throws CVC5ApiException {
+  @Test void getInteger() throws CVC5ApiException
+  {
     Term int1 = d_solver.mkInteger("-18446744073709551616");
     Term int2 = d_solver.mkInteger("-18446744073709551615");
     Term int3 = d_solver.mkInteger("-4294967296");
@@ -727,7 +711,6 @@ class TermTest {
     assertEquals(int7.getLong(), 10);
     assertEquals(int7.getInteger(), "10");
     assertTrue(!int8.isInt() && int8.isLong() && int8.isInteger());
-    assertEquals(Integer.toUnsignedLong(int8.getInt()), 4294967295L);
     assertEquals(int8.getLong(), 4294967295L);
     assertEquals(int8.getInteger(), "4294967295");
     assertTrue(!int9.isInt() && int9.isLong() && int9.isInteger());
@@ -735,23 +718,20 @@ class TermTest {
     assertEquals(int9.getInteger(), "4294967296");
     assertTrue(!int10.isInt() && !int10.isLong() && int10.isInteger());
 
-    assertEquals(Long.compareUnsigned(int10.getLong(),
-                     new BigInteger("18446744073709551615").longValue()),
-        0);
     assertEquals(int10.getInteger(), "18446744073709551615");
     assertTrue(!int11.isInt() && !int11.isLong() && int11.isInteger());
     assertEquals(int11.getInteger(), "18446744073709551616");
   }
 
-  @Test
-  void getString() {
+  @Test void getString()
+  {
     Term s1 = d_solver.mkString("abcde");
     assertTrue(s1.isString());
     assertEquals(s1.getString(), "abcde");
   }
 
-  @Test
-  void substitute() {
+  @Test void substitute()
+  {
     Term x = d_solver.mkConst(d_solver.getIntegerSort(), "x");
     Term one = d_solver.mkInteger(1);
     Term ttrue = d_solver.mkTrue();
@@ -801,8 +781,8 @@ class TermTest {
     assertThrows(CVC5ApiException.class, () -> xpx.substitute(es, rs));
   }
 
-  @Test
-  void constArray() throws CVC5ApiException {
+  @Test void constArray() throws CVC5ApiException
+  {
     Sort intsort = d_solver.getIntegerSort();
     Sort arrsort = d_solver.mkArraySort(intsort, intsort);
     Term a = d_solver.mkConst(arrsort, "a");
@@ -813,19 +793,15 @@ class TermTest {
     assertEquals(constarr.getConstArrayBase(), one);
     assertThrows(CVC5ApiException.class, () -> a.getConstArrayBase());
 
-    arrsort =
-        d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort());
+    arrsort = d_solver.mkArraySort(d_solver.getRealSort(), d_solver.getRealSort());
     Term zero_array = d_solver.mkConstArray(arrsort, d_solver.mkReal(0));
-    Term stores = d_solver.mkTerm(
-        STORE, zero_array, d_solver.mkReal(1), d_solver.mkReal(2));
-    stores =
-        d_solver.mkTerm(STORE, stores, d_solver.mkReal(2), d_solver.mkReal(3));
-    stores =
-        d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5));
+    Term stores = d_solver.mkTerm(STORE, zero_array, d_solver.mkReal(1), d_solver.mkReal(2));
+    stores = d_solver.mkTerm(STORE, stores, d_solver.mkReal(2), d_solver.mkReal(3));
+    stores = d_solver.mkTerm(STORE, stores, d_solver.mkReal(4), d_solver.mkReal(5));
   }
 
-  @Test
-  void constSequenceElements() throws CVC5ApiException {
+  @Test void constSequenceElements() throws CVC5ApiException
+  {
     Sort realsort = d_solver.getRealSort();
     Sort seqsort = d_solver.mkSequenceSort(realsort);
     Term s = d_solver.mkEmptySequence(seqsort);
@@ -841,8 +817,8 @@ class TermTest {
     assertThrows(CVC5ApiException.class, () -> su.getConstSequenceElements());
   }
 
-  @Test
-  void termScopedToString() {
+  @Test void termScopedToString()
+  {
     Sort intsort = d_solver.getIntegerSort();
     Term x = d_solver.mkConst(intsort, "x");
     assertEquals(x.toString(), "x");