2 files changed, 22 insertions, 0 deletions
diff --git a/test/unit/api/java/SolverTest.java b/test/unit/api/java/SolverTest.java
index 161854421..6a08d79c6 100644
--- a/test/unit/api/java/SolverTest.java
+++ b/test/unit/api/java/SolverTest.java
@@ -639,6 +639,13 @@ class SolverTest
     assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpNone()));
   }
 
+  @Test void mkRegexpAll()
+  {
+    Sort strSort = d_solver.getStringSort();
+    Term s = d_solver.mkConst(strSort, "s");
+    assertDoesNotThrow(() -> d_solver.mkTerm(STRING_IN_REGEXP, s, d_solver.mkRegexpAll()));
+  }
+
   @Test void mkRegexpAllchar()
   {
     Sort strSort = d_solver.getStringSort();
diff --git a/test/unit/api/java/TermTest.java b/test/unit/api/java/TermTest.java
index bf0beb024..b7f111428 100644
--- a/test/unit/api/java/TermTest.java
+++ b/test/unit/api/java/TermTest.java
@@ -219,6 +219,21 @@ class TermTest
     Term nilOpTerm = list.getConstructorTerm("nil");
   }
 
+  @Test void hasGetSymbol() throws CVC5ApiException
+  {
+    Term n = d_solver.getNullTerm();
+    Term t = d_solver.mkBoolean(true);
+    Term c = d_solver.mkConst(d_solver.getBooleanSort(), "|\\|");
+
+    assertThrows(CVC5ApiException.class, () -> n.hasSymbol());
+    assertFalse(t.hasSymbol());
+    assertTrue(c.hasSymbol());
+
+    assertThrows(CVC5ApiException.class, () -> n.getSymbol());
+    assertThrows(CVC5ApiException.class, () -> t.getSymbol());
+    assertEquals(c.getSymbol(), "|\\|");
+  }
+
   @Test void isNull() throws CVC5ApiException
   {
     Term x = d_solver.getNullTerm();