Enable most quantifier tests for CVC4 that were disabled

Author: baierd

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

@@ -134,8 +134,6 @@ private SolverException handleSolverException(SolverException e) throws SolverEx
 
   @Test
   public void testLIAForallArrayConjunctUnsat() throws SolverException, InterruptedException {
-    assume().that(solverUnderTest).isNotEqualTo(Solvers.CVC4);
-
     // (forall x . b[x] = 0) AND (b[123] = 1) is UNSAT
     requireIntegers();
 
@@ -154,8 +152,6 @@ public void testBVForallArrayConjunctUnsat() throws SolverException, Interrupted
     assume().that(solverUnderTest).isNotEqualTo(Solvers.PRINCESS);
     // Boolector quants need to be reworked
     assume().that(solverUnderTest).isNotEqualTo(Solvers.BOOLECTOR);
-    // CVC4 can solve less quants with String support enabled, TODO bug?
-    assume().that(solverUnderTest).isNotEqualTo(Solvers.CVC4);
 
     BooleanFormula f =
         bmgr.and(
@@ -346,8 +342,6 @@ public void testBVExistsArrayConjunct1() throws SolverException, InterruptedExce
 
   @Test
   public void testLIAExistsArrayConjunct2() throws SolverException, InterruptedException {
-    assume().that(solverUnderTest).isNotEqualTo(Solvers.CVC4);
-
     // (exists x . b[x] = 1) AND  (forall x . b[x] = 0) is UNSAT
 
     requireIntegers();
@@ -358,8 +352,6 @@ public void testLIAExistsArrayConjunct2() throws SolverException, InterruptedExc
 
   @Test
   public void testBVExistsArrayConjunct2() throws SolverException, InterruptedException {
-    assume().that(solverUnderTest).isNotEqualTo(Solvers.CVC4);
-
     // (exists x . b[x] = 1) AND (forall x . b[x] = 0) is UNSAT
     requireBitvectors();
     // Princess does not support bitvectors in arrays
@@ -795,8 +787,6 @@ public void checkBVQuantifierElimination() throws InterruptedException, SolverEx
 
   @Test
   public void testExistsRestrictedRange() throws SolverException, InterruptedException {
-    assume().that(solverUnderTest).isNotEqualTo(Solvers.CVC4);
-
     ArrayFormula<IntegerFormula, IntegerFormula> b =
         amgr.makeArray("b", FormulaType.IntegerType, FormulaType.IntegerType);
     BooleanFormula bAtXEq1 = imgr.equal(amgr.select(b, x), imgr.makeNumber(1));
@@ -978,13 +968,6 @@ public void testForallBasicStringArray() throws SolverException, InterruptedExce
     requireStrings();
     requireIntegers();
 
-    // CVC4 returns null or UNKNOWN, however it does not seem to have a problem with
-    // declaring/starting the solving process!
-    assume()
-        .withMessage("Solver %s does not support the complete theory of quantifiers", solverToUse())
-        .that(solverToUse())
-        .isNotEqualTo(Solvers.CVC4);
-
     // forall var (var = select(store(arr, 2, "bla"), 2)
     IntegerFormula two = imgr.makeNumber(2);
     StringFormula string = smgr.makeString("bla");