Remove tests that use formerly illegal variable names and expect and exception

Author: daniel-raffler

src/org/sosy_lab/java_smt/test/EnumerationFormulaManagerTest.java

@@ -159,13 +159,6 @@ public void testIncompatibleEnumeration() {
     assertThrows(IllegalArgumentException.class, () -> emgr.equivalence(blue, circle));
   }
 
-  @Test
-  public void testInvalidName() {
-    assertThrows(IllegalArgumentException.class, () -> emgr.declareEnumeration("true", "X", "Y"));
-    EnumerationFormulaType colorType = emgr.declareEnumeration("ColorE", "Blue", "White");
-    assertThrows(IllegalArgumentException.class, () -> emgr.makeVariable("true", colorType));
-  }
-
   private static class ConstantsVisitor extends DefaultFormulaVisitor<TraversalProcess> {
 
     final Set<String> constants = new HashSet<>();

src/org/sosy_lab/java_smt/test/UFManagerTest.java

@@ -244,22 +244,6 @@ public void testDeclareAndCallUFWithBooleanAndBVTypes() {
     }
   }
 
-  @SuppressWarnings("CheckReturnValue")
-  @Test
-  public void testDeclareAndCallUFWithIntWithUnsupportedName() {
-    requireIntegers();
-    assertThrows(
-        IllegalArgumentException.class,
-        () ->
-            fmgr.declareAndCallUF(
-                "|Func|", FormulaType.IntegerType, ImmutableList.of(imgr.makeNumber(1))));
-    assertThrows(
-        IllegalArgumentException.class,
-        () ->
-            fmgr.declareUF(
-                "|Func|", FormulaType.IntegerType, ImmutableList.of(FormulaType.IntegerType)));
-  }
-
   @Test
   public void testDeclareAndCallUFWithBv() {
     requireBitvectors();
@@ -276,26 +260,6 @@ public void testDeclareAndCallUFWithBv() {
     }
   }
 
-  @Test
-  @SuppressWarnings("CheckReturnValue")
-  public void testDeclareAndCallUFWithBvWithUnsupportedName() {
-    requireBitvectors();
-    assertThrows(
-        IllegalArgumentException.class,
-        () ->
-            fmgr.declareAndCallUF(
-                "|Func|",
-                FormulaType.getBitvectorTypeWithSize(4),
-                ImmutableList.of(bvmgr.makeBitvector(4, 1))));
-    assertThrows(
-        IllegalArgumentException.class,
-        () ->
-            fmgr.declareUF(
-                "|Func|",
-                FormulaType.getBitvectorTypeWithSize(4),
-                ImmutableList.of(FormulaType.getBitvectorTypeWithSize(4))));
-  }
-
   @Test
   public void testDeclareAndCallUFWithTypedArgs() {
     requireBooleanArgument();