Merge remote-tracking branch 'origin/master' into 406-exception-when-z3-is-interrupted-during-modelevaluate

Author: kfriedberger

lib/ivy.xml

@@ -84,14 +84,14 @@ SPDX-License-Identifier: Apache-2.0
 
     <dependencies>
         <!-- SoSy-Lab Common Library -->
-        <dependency org="org.sosy_lab" name="common" rev="0.3000-585-g7a5f95c1" conf="core->runtime; contrib->sources"/>
+        <dependency org="org.sosy_lab" name="common" rev="0.3000-609-g90a352c" conf="core->runtime; contrib->sources"/>
 
         <!-- Google Core Libraries for Java
              Contains a lot of helpful data structures. -->
-        <dependency org="com.google.guava" name="guava" rev="33.2.1-jre" conf="core->default; contrib->sources"/>
+        <dependency org="com.google.guava" name="guava" rev="33.3.1-jre" conf="core->default; contrib->sources"/>
 
         <!--  Guava-testlib contains many useful testing utilities -->
-        <dependency org="com.google.guava" name="guava-testlib" rev="33.2.1-jre" conf="test->default; contrib->sources"/>
+        <dependency org="com.google.guava" name="guava-testlib" rev="33.3.1-jre" conf="test->default; contrib->sources"/>
 
         <!-- Dependency on Ivy itself so that we can ugprade it easily.
              Change version number in build/build-ivy.xml for upgrading. -->
@@ -102,7 +102,7 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="com.google.auto.value" name="auto-value-annotations" rev="1.11.0" conf="build->default; contrib->sources"/>
 
         <!-- Annotations we use for @Nullable etc. -->
-        <dependency org="org.checkerframework" name="checker-qual" rev="3.44.0" conf="core->default; contrib->sources"/>
+        <dependency org="org.checkerframework" name="checker-qual" rev="3.48.1" conf="core->default; contrib->sources"/>
 
         <!-- JUnit
              Testing framework. -->
@@ -119,8 +119,8 @@ SPDX-License-Identifier: Apache-2.0
 
         <!-- Truth
              Library for writing literal assertions. -->
-        <dependency org="com.google.truth" name="truth" rev="1.4.2" conf="test->default; contrib->sources"/>
-        <dependency org="com.google.truth.extensions" name="truth-java8-extension" rev="1.4.2" conf="test->default; contrib->sources"/>
+        <dependency org="com.google.truth" name="truth" rev="1.4.4" conf="test->default; contrib->sources"/>
+        <dependency org="com.google.truth.extensions" name="truth-java8-extension" rev="1.4.4" conf="test->default; contrib->sources"/>
 
         <!-- Google error-prone
              Compiler adaptor with some useful checks for common errors. -->
@@ -129,11 +129,11 @@ SPDX-License-Identifier: Apache-2.0
 
         <!-- Eclipse JDT Compiler
              For additional compiler warnings. -->
-        <dependency org="org.eclipse.jdt.core.compiler" name="ecj" rev="4.29" conf="build->default"/>
+        <dependency org="org.eclipse.jdt.core.compiler" name="ecj" rev="4.32-sosy0" conf="build->default"/>
 
         <!-- google-java-format
              A source-code formatter for Java -->
-        <dependency org="com.google.googlejavaformat" name="google-java-format" rev="1.22.0" conf="format-source->default"/>
+        <dependency org="com.google.googlejavaformat" name="google-java-format" rev="1.24.0" conf="format-source->default"/>
 
         <!-- SpotBugs -->
         <dependency org="com.github.spotbugs" name="spotbugs-ant" rev="4.8.6" conf="spotbugs->default"/>
@@ -143,7 +143,7 @@ SPDX-License-Identifier: Apache-2.0
 
         <!-- Checkstyle -->
         <dependency org="com.github.sevntu-checkstyle" name="sevntu-checks" rev="1.44.1" conf="checkstyle->default"/>
-        <dependency org="com.puppycrawl.tools" name="checkstyle" rev="10.17.0" conf="checkstyle->default"/>
+        <dependency org="com.puppycrawl.tools" name="checkstyle" rev="10.19.0" conf="checkstyle->default"/>
 
         <!-- SmtInterpol -->
         <dependency org="de.uni-freiburg.informatik.ultimate" name="smtinterpol" rev="2.5-1242-g5c50fb6d" conf="runtime-smtinterpol->master; contrib->sources"/>
@@ -160,14 +160,14 @@ SPDX-License-Identifier: Apache-2.0
         <dependency org="edu.tum.cs" name="java-cup" rev="11b-20160615" conf="runtime-princess->runtime"/>
 
         <!-- Solver Binaries -->
-        <dependency org="org.sosy_lab" name="javasmt-solver-mathsat" rev="5.6.10" conf="runtime-mathsat->solver-mathsat" />
-        <dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.12.5" conf="runtime-z3->solver-z3; contrib->sources,javadoc" />
+        <dependency org="org.sosy_lab" name="javasmt-solver-mathsat" rev="5.6.11-glibc2.27" conf="runtime-mathsat->solver-mathsat" />
+        <dependency org="org.sosy_lab" name="javasmt-solver-z3" rev="4.13.0" conf="runtime-z3->solver-z3; contrib->sources,javadoc" />
         <dependency org="org.sosy_lab" name="javasmt-solver-opensmt" rev="2.6.0-g2f72cc0e" conf="runtime-opensmt->solver-opensmt; contrib->sources,javadoc" />
         <dependency org="org.sosy_lab" name="javasmt-solver-optimathsat" rev="1.7.1-sosy0" conf="runtime-optimathsat->solver-optimathsat" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc4" rev="1.8-prerelease-2020-06-24-g7825d8f28" conf="runtime-cvc4->solver-cvc4" />
         <dependency org="org.sosy_lab" name="javasmt-solver-cvc5" rev="1.0.5-g4cb2ab9eb" conf="runtime-cvc5->solver-cvc5" />
         <dependency org="org.sosy_lab" name="javasmt-solver-boolector" rev="3.2.2-g1a89c229" conf="runtime-boolector->solver-boolector" />
-        <dependency org="org.sosy_lab" name="javasmt-solver-bitwuzla" rev="0.6.0-gab3db0e6" conf="runtime-bitwuzla->solver-bitwuzla; contrib->sources,javadoc"/>
+        <dependency org="org.sosy_lab" name="javasmt-solver-bitwuzla" rev="0.6.0-g2b3d69a7" conf="runtime-bitwuzla->solver-bitwuzla; contrib->sources,javadoc"/>
 
         <!-- additional JavaSMT components with Solver Binaries -->
         <dependency org="org.sosy_lab" name="javasmt-yices2" rev="4.1.1-734-g3732f7e08" conf="runtime-yices2->runtime; contrib->sources" />

src/org/sosy_lab/java_smt/basicimpl/AbstractSolverContext.java

@@ -35,6 +35,7 @@ public final FormulaManager getFormulaManager() {
     return fmgr;
   }
 
+  @SuppressWarnings("resource")
   @Override
   public final ProverEnvironment newProverEnvironment(ProverOptions... options) {
     ProverEnvironment out = newProverEnvironment0(toSet(options));

src/org/sosy_lab/java_smt/example/FormulaClassifier.java

@@ -294,7 +294,7 @@ public Integer visitFunction(
             nonLinearArithmetic = true;
             return allArgLevel + 1;
           }
-          // $FALL-THROUGH$
+        // $FALL-THROUGH$
         default:
           if (pFunctionDeclaration.getType().isBooleanType()) {
             if (EnumSet.of(

src/org/sosy_lab/java_smt/solvers/smtinterpol/SmtInterpolAbstractProver.java

@@ -217,7 +217,8 @@ public ImmutableMap<String, String> getStatistics() {
   public void close() {
     if (!closed) {
       annotatedTerms.clear();
-      env.pop(size());
+      env.resetAssertions();
+      env.exit();
     }
     super.close();
   }

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

@@ -10,7 +10,6 @@
 
 import static com.google.common.truth.Truth.assertThat;
 import static com.google.common.truth.Truth.assertWithMessage;
-import static com.google.common.truth.Truth.assert_;
 import static com.google.common.truth.TruthJUnit.assume;
 import static org.junit.Assert.assertThrows;
 import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
@@ -534,11 +533,9 @@ public void bvInRange() throws SolverException, InterruptedException {
   @SuppressWarnings("CheckReturnValue")
   public void bvOutOfRange() {
     for (int[] sizeAndValue : new int[][] {{4, 32}, {4, -9}, {8, 300}, {8, -160}}) {
-      try {
-        bvmgr.makeBitvector(sizeAndValue[0], sizeAndValue[1]);
-        assert_().fail();
-      } catch (IllegalArgumentException expected) {
-      }
+      assertThrows(
+          IllegalArgumentException.class,
+          () -> bvmgr.makeBitvector(sizeAndValue[0], sizeAndValue[1]));
     }
 
     for (int size : new int[] {4, 6, 8, 10, 16, 32}) {
@@ -547,16 +544,9 @@ public void bvOutOfRange() {
       bvmgr.makeBitvector(size, -(1L << (size - 1)));
 
       // forbitten values
-      try {
-        bvmgr.makeBitvector(size, 1L << size);
-        assert_().fail();
-      } catch (IllegalArgumentException expected) {
-      }
-      try {
-        bvmgr.makeBitvector(size, -(1L << (size - 1)) - 1);
-        assert_().fail();
-      } catch (IllegalArgumentException expected) {
-      }
+      assertThrows(IllegalArgumentException.class, () -> bvmgr.makeBitvector(size, 1L << size));
+      assertThrows(
+          IllegalArgumentException.class, () -> bvmgr.makeBitvector(size, -(1L << (size - 1)) - 1));
     }
 
     for (int size : new int[] {36, 40, 64, 65, 100, 128, 200, 250, 1000, 10000}) {
@@ -572,17 +562,14 @@ public void bvOutOfRange() {
       bvmgr.makeBitvector(size, BigInteger.ONE.shiftLeft(size - 1).negate());
 
       // forbitten values
-      try {
-        bvmgr.makeBitvector(size, BigInteger.ONE.shiftLeft(size));
-        assert_().fail();
-      } catch (IllegalArgumentException expected) {
-      }
-      try {
-        bvmgr.makeBitvector(
-            size, BigInteger.ONE.shiftLeft(size - 1).negate().subtract(BigInteger.ONE));
-        assert_().fail();
-      } catch (IllegalArgumentException expected) {
-      }
+      assertThrows(
+          IllegalArgumentException.class,
+          () -> bvmgr.makeBitvector(size, BigInteger.ONE.shiftLeft(size)));
+      assertThrows(
+          IllegalArgumentException.class,
+          () ->
+              bvmgr.makeBitvector(
+                  size, BigInteger.ONE.shiftLeft(size - 1).negate().subtract(BigInteger.ONE)));
     }
   }
 

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

@@ -10,8 +10,8 @@
 
 import static com.google.common.truth.Truth.assertThat;
 import static com.google.common.truth.Truth.assertWithMessage;
-import static com.google.common.truth.Truth.assert_;
 import static com.google.common.truth.TruthJUnit.assume;
+import static org.junit.Assert.assertThrows;
 import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
 
 import com.google.common.collect.ImmutableList;
@@ -47,7 +47,7 @@ public class FloatingPointFormulaManagerTest
   // numbers are small enough to be precise with single precision
   private static final int[] SINGLE_PREC_INTS = new int[] {0, 1, 2, 5, 10, 20, 50, 100, 200, 500};
 
-  private static final int NUM_RANDOM_TESTS = 100;
+  private static final int NUM_RANDOM_TESTS = 50;
 
   private FloatingPointType singlePrecType;
   private FloatingPointType doublePrecType;
@@ -867,8 +867,8 @@ private List<Float> getListOfFloats() {
       flts.add(-0.0f); // MathSat5 fails for NEGATIVE_ZERO
     }
 
-    for (int i = 1; i < 20; i++) {
-      for (int j = 1; j < 20; j++) {
+    for (int i = 1; i < 10; i++) {
+      for (int j = 1; j < 10; j++) {
         flts.add((float) (i * Math.pow(10, j)));
         flts.add((float) (-i * Math.pow(10, j)));
       }
@@ -904,8 +904,8 @@ private List<Double> getListOfDoubles() {
       dbls.add(-0.0); // MathSat5 fails for NEGATIVE_ZERO
     }
 
-    for (int i = 1; i < 20; i++) {
-      for (int j = 1; j < 20; j++) {
+    for (int i = 1; i < 10; i++) {
+      for (int j = 1; j < 10; j++) {
         dbls.add(i * Math.pow(10, j));
         dbls.add(-i * Math.pow(10, j));
       }
@@ -1024,11 +1024,9 @@ public void fpInterpolation() throws SolverException, InterruptedException {
     }
   }
 
-  @SuppressWarnings("CheckReturnValue")
-  @Test(expected = Exception.class)
+  @Test
   public void failOnInvalidString() {
-    fpmgr.makeNumber("a", singlePrecType);
-    assert_().fail();
+    assertThrows(Exception.class, () -> fpmgr.makeNumber("a", singlePrecType));
   }
 
   @Test

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

@@ -11,7 +11,6 @@
 import static com.google.common.collect.Iterables.getLast;
 import static com.google.common.truth.Truth.assertThat;
 import static com.google.common.truth.Truth.assertWithMessage;
-import static com.google.common.truth.Truth.assert_;
 import static com.google.common.truth.TruthJUnit.assume;
 import static org.junit.Assert.assertThrows;
 import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
@@ -362,8 +361,7 @@ public <T> void sequentialInterpolationIsNotRepeatedIndividualInterpolation()
     }
   }
 
-  @Test(expected = IllegalArgumentException.class)
-  @SuppressWarnings("CheckReturnValue")
+  @Test
   public <T> void sequentialInterpolationWithoutPartition()
       throws SolverException, InterruptedException {
     requireIntegers();
@@ -373,8 +371,8 @@ public <T> void sequentialInterpolationWithoutPartition()
     assertThat(stack).isUnsatisfiable();
 
     // empty list of partition
-    stack.getSeqInterpolants(ImmutableList.of());
-    assert_().fail();
+    assertThrows(
+        IllegalArgumentException.class, () -> stack.getSeqInterpolants(ImmutableList.of()));
   }
 
   @Test
@@ -973,8 +971,7 @@ public <T> void treeInterpolationMalFormed6() throws SolverException, Interrupte
     stack.getTreeInterpolants0(ImmutableList.of(TA, TA, TA), new int[] {0, 2, 0});
   }
 
-  @Test(expected = IllegalArgumentException.class)
-  @SuppressWarnings("CheckReturnValue")
+  @Test
   public <T> void treeInterpolationWithoutPartition() throws SolverException, InterruptedException {
     requireTreeItp();
 
@@ -984,8 +981,9 @@ public <T> void treeInterpolationWithoutPartition() throws SolverException, Inte
     assertThat(stack).isUnsatisfiable();
 
     // empty list of partition
-    stack.getTreeInterpolants(ImmutableList.of(), new int[] {});
-    assert_().fail();
+    assertThrows(
+        IllegalArgumentException.class,
+        () -> stack.getTreeInterpolants(ImmutableList.of(), new int[] {}));
   }
 
   @Test

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

@@ -51,7 +51,7 @@ public class ModelEvaluationTest extends SolverBasedTest0.ParameterizedSolverBas
 
   @Override
   protected ConfigurationBuilder createTestConfigBuilder() {
-    problemSize = solverToUse() == Solvers.PRINCESS ? 10 : 100; // Princess is too slow.
+    problemSize = solverToUse() == Solvers.PRINCESS ? 10 : 50; // Princess is too slow.
     ConfigurationBuilder builder = super.createTestConfigBuilder();
     if (solverToUse() == Solvers.MATHSAT5) {
       builder.setOption("solver.mathsat5.furtherOptions", "model_generation=true");

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

@@ -12,6 +12,7 @@
 import static com.google.common.truth.Truth.assertWithMessage;
 import static com.google.common.truth.Truth.assert_;
 import static com.google.common.truth.TruthJUnit.assume;
+import static org.junit.Assert.assertThrows;
 import static org.sosy_lab.java_smt.api.FormulaType.IntegerType;
 import static org.sosy_lab.java_smt.test.ProverEnvironmentSubject.assertThat;
 
@@ -184,7 +185,7 @@ public void testGetRationals() throws SolverException, InterruptedException {
   /** Test that different names are no problem for Bools in the model. */
   @Test
   public void testGetBooleans() throws SolverException, InterruptedException {
-    // Some names are specificly chosen to test the Boolector model
+    // Some names are specifically chosen to test the Boolector model
     for (String name : VARIABLE_NAMES) {
       testModelGetters(bmgr.makeVariable(name), bmgr.makeBoolean(true), true, name);
     }
@@ -1207,12 +1208,12 @@ public void testGetArrays4() throws SolverException, InterruptedException {
         ImmutableList.of(BigInteger.valueOf(5)));
   }
 
-  @Test(expected = IllegalArgumentException.class)
-  @SuppressWarnings("CheckReturnValue")
+  @Test
   public void testGetArrays4invalid() throws SolverException, InterruptedException {
     requireParser();
     requireArrays();
     requireArrayModel();
+    requireIntegers();
 
     // create formula for "arr[5]==x && x==123"
     BooleanFormula f =
@@ -1229,7 +1230,9 @@ public void testGetArrays4invalid() throws SolverException, InterruptedException
       assertThat(prover).isSatisfiable();
 
       try (Model m = prover.getModel()) {
-        m.evaluate(amgr.makeArray("arr", ARRAY_TYPE_INT_INT));
+        assertThrows(
+            IllegalArgumentException.class,
+            () -> m.evaluate(amgr.makeArray("arr", ARRAY_TYPE_INT_INT)));
       }
     }
   }
@@ -2306,22 +2309,19 @@ public void modelAfterSolverCloseTest() throws SolverException, InterruptedExcep
     }
   }
 
-  @SuppressWarnings("resource")
-  @Test(expected = IllegalStateException.class)
+  @Test
   public void testGenerateModelsOption() throws SolverException, InterruptedException {
     try (ProverEnvironment prover = context.newProverEnvironment()) { // no option
       assertThat(prover).isSatisfiable();
-      prover.getModel();
-      assert_().fail();
+      assertThrows(IllegalStateException.class, () -> prover.getModel());
     }
   }
 
-  @Test(expected = IllegalStateException.class)
+  @Test
   public void testGenerateModelsOption2() throws SolverException, InterruptedException {
     try (ProverEnvironment prover = context.newProverEnvironment()) { // no option
       assertThat(prover).isSatisfiable();
-      prover.getModelAssignments();
-      assert_().fail();
+      assertThrows(IllegalStateException.class, () -> prover.getModelAssignments());
     }
   }
 

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

@@ -52,7 +52,7 @@ public class NonLinearArithmeticTest<T extends NumeralFormula> extends SolverBas
   @Parameters(name = "{0} {1} {2}")
   public static Iterable<Object[]> getAllSolversAndTheories() {
     return Lists.cartesianProduct(
-            Arrays.asList(Solvers.values()),
+            Arrays.asList(ParameterizedSolverBasedTest0.getAllSolvers()),
             ImmutableList.of(FormulaType.IntegerType, FormulaType.RationalType),
             Arrays.asList(NonLinearArithmetic.values()))
         .stream()