simplify tests and avoid some unneeded construction of lists.

Author: kfriedberger

src/org/sosy_lab/java_smt/solvers/cvc4/CVC4NativeAPITest.java

@@ -11,7 +11,6 @@
 import static com.google.common.truth.Truth.assertThat;
 import static org.junit.Assert.assertThrows;
 
-import com.google.common.collect.ImmutableList;
 import edu.stanford.CVC4.ArrayType;
 import edu.stanford.CVC4.BitVector;
 import edu.stanford.CVC4.BitVectorType;
@@ -766,7 +765,7 @@ public void checkUnsatCore() {
 
     // UnsatCores are iterable
     for (Expr e : unsatCore) {
-      assertThat(e.toString()).isIn(ImmutableList.of("(not (or a b))", "(and a b)"));
+      assertThat(e.toString()).isAnyOf("(not (or a b))", "(and a b)");
     }
   }
 

src/org/sosy_lab/java_smt/solvers/cvc5/CVC5NativeAPITest.java

@@ -12,7 +12,6 @@
 import static org.junit.Assert.assertThrows;
 
 import com.google.common.base.Preconditions;
-import com.google.common.collect.ImmutableList;
 import io.github.cvc5.CVC5ApiException;
 import io.github.cvc5.Kind;
 import io.github.cvc5.Op;
@@ -1031,7 +1030,7 @@ public void checkUnsatCore() {
 
     // UnsatCores are iterable
     for (Term e : unsatCore) {
-      assertThat(e.toString()).isIn(ImmutableList.of("(not (or a b))", "(and a b)"));
+      assertThat(e.toString()).isAnyOf("(not (or a b))", "(and a b)");
     }
   }
 

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

@@ -856,7 +856,7 @@ public void testPartialModelsUF() throws SolverException, InterruptedException {
     assume()
         .withMessage("As of now, only Z3 supports partial model evaluation")
         .that(solver)
-        .isIn(ImmutableList.of(Solvers.Z3));
+        .isEqualTo(Solvers.Z3);
     try (ProverEnvironment prover = context.newProverEnvironment(ProverOptions.GENERATE_MODELS)) {
       IntegerFormula x = imgr.makeVariable("x");
       IntegerFormula f = fmgr.declareAndCallUF("f", IntegerType, x);