1 files changed, 1 insertions, 30 deletions
diff --git a/test/unit/api/java/cvc5/SolverTest.java b/test/unit/api/java/cvc5/SolverTest.java
index d153b8a91..9694510d9 100644
--- a/test/unit/api/java/cvc5/SolverTest.java
+++ b/test/unit/api/java/cvc5/SolverTest.java
@@ -386,35 +386,6 @@ class SolverTest
     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);
@@ -2342,4 +2313,4 @@ class SolverTest
             + "\"Z\")))",
         projection.toString());
   }
-}
-\ No newline at end of file
+}