From 5f14c3f70dbedf7013c3b137d4138848f75f5051 Mon Sep 17 00:00:00 2001 From: Daniel Raffler Date: Tue, 1 Apr 2025 12:10:03 +0200 Subject: [PATCH] CVC5: Completely disable CVC5 in SolverConcurrencyTest and TimeoutTest due to its concurrency issues --- .../java_smt/test/SolverConcurrencyTest.java | 19 +++++------- .../sosy_lab/java_smt/test/TimeoutTest.java | 31 ++++++++----------- 2 files changed, 20 insertions(+), 30 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java index 50cd3a71cf..f6f1954fb6 100644 --- a/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverConcurrencyTest.java @@ -124,6 +124,11 @@ public void checkThatSolverIsAvailable() throws InvalidConfigurationException { .that(solver) .isNotEqualTo(Solvers.MATHSAT5); } + + assume() + .withMessage("Solver does not support concurrency without concurrent context.") + .that(solver) + .isNotEqualTo(Solvers.CVC5); } private void requireConcurrentMultipleStackSupport() { @@ -298,7 +303,7 @@ public void testFormulaTranslationWithConcurrentContexts() assume() .withMessage("Solver does not support translation of formulas") .that(solver) - .isNoneOf(Solvers.CVC4, Solvers.PRINCESS, Solvers.CVC5); + .isNoneOf(Solvers.CVC4, Solvers.PRINCESS); ConcurrentLinkedQueue contextAndFormulaList = new ConcurrentLinkedQueue<>(); @@ -348,11 +353,6 @@ public void testFormulaTranslationWithConcurrentContexts() public void testIntConcurrencyWithoutConcurrentContext() throws InvalidConfigurationException { requireIntegers(); - assume() - .withMessage("Solver does not support concurrency without concurrent context.") - .that(solver) - .isNotEqualTo(Solvers.CVC5); - ConcurrentLinkedQueue contextList = new ConcurrentLinkedQueue<>(); // Initialize contexts before using them in the threads for (int i = 0; i < NUMBER_OF_THREADS; i++) { @@ -373,11 +373,6 @@ public void testIntConcurrencyWithoutConcurrentContext() throws InvalidConfigura public void testBvConcurrencyWithoutConcurrentContext() throws InvalidConfigurationException { requireBitvectors(); - assume() - .withMessage("Solver does not support concurrency without concurrent context.") - .that(solver) - .isNotEqualTo(Solvers.CVC5); - ConcurrentLinkedQueue contextList = new ConcurrentLinkedQueue<>(); // Initialize contexts before using them in the threads for (int i = 0; i < NUMBER_OF_THREADS; i++) { @@ -545,7 +540,7 @@ public void continuousRunningThreadFormulaTransferTranslateTest() { assume() .withMessage("Solver does not support translation of formulas") .that(solver) - .isNoneOf(Solvers.CVC4, Solvers.CVC5, Solvers.PRINCESS); + .isNoneOf(Solvers.CVC4, Solvers.PRINCESS); // This is fine! We might access this more than once at a time, // but that gives only access to the bucket, which is threadsafe. diff --git a/src/org/sosy_lab/java_smt/test/TimeoutTest.java b/src/org/sosy_lab/java_smt/test/TimeoutTest.java index 3b7e55aa6d..ffcdcb05b3 100644 --- a/src/org/sosy_lab/java_smt/test/TimeoutTest.java +++ b/src/org/sosy_lab/java_smt/test/TimeoutTest.java @@ -8,13 +8,14 @@ package org.sosy_lab.java_smt.test; +import static com.google.common.truth.TruthJUnit.assume; import static org.junit.Assert.assertThrows; -import com.google.common.truth.TruthJUnit; import java.util.ArrayList; import java.util.List; import java.util.Random; import java.util.function.Supplier; +import org.junit.Before; import org.junit.Test; import org.junit.runner.RunWith; import org.junit.runners.Parameterized; @@ -62,13 +63,20 @@ protected Logics logicToUse() { return Logics.QF_LIA; } + @Before + public void setUp() { + // FIXME CVC5 has interruptions, but crashes on Windows, probably due to concurrency issues + // TODO Add interruption for Princess + assume() + .withMessage(solverToUse() + " does not support interruption") + .that(solverToUse()) + .isNoneOf(Solvers.PRINCESS, Solvers.CVC5); + } + @Test @SuppressWarnings("CheckReturnValue") public void testTacticTimeout() { - TruthJUnit.assume() - .withMessage("Only Z3 has native tactics") - .that(solverToUse()) - .isEqualTo(Solvers.Z3); + assume().withMessage("Only Z3 has native tactics").that(solverToUse()).isEqualTo(Solvers.Z3); Fuzzer fuzzer = new Fuzzer(mgr, new Random(0)); String msg = "ShutdownRequest"; BooleanFormula test = fuzzer.fuzz(20, 3); @@ -79,21 +87,12 @@ public void testTacticTimeout() { @Test(timeout = TIMEOUT_MILLISECONDS) public void testProverTimeoutInt() throws InterruptedException { requireIntegers(); - TruthJUnit.assume() - .withMessage(solverToUse() + " does not support interruption") - .that(solverToUse()) - .isNoneOf(Solvers.PRINCESS, Solvers.BOOLECTOR, Solvers.CVC5); testBasicProverTimeoutInt(() -> context.newProverEnvironment()); } @Test(timeout = TIMEOUT_MILLISECONDS) public void testProverTimeoutBv() throws InterruptedException { requireBitvectors(); - TruthJUnit.assume() - .withMessage(solverToUse() + " does not support interruption") - .that(solverToUse()) - .isNoneOf(Solvers.PRINCESS, Solvers.CVC5); - testBasicProverTimeoutBv(() -> context.newProverEnvironment()); } @@ -101,10 +100,6 @@ public void testProverTimeoutBv() throws InterruptedException { public void testInterpolationProverTimeout() throws InterruptedException { requireInterpolation(); requireIntegers(); - TruthJUnit.assume() - .withMessage(solverToUse() + " does not support interruption") - .that(solverToUse()) - .isNoneOf(Solvers.PRINCESS, Solvers.BOOLECTOR, Solvers.CVC5); testBasicProverTimeoutInt(() -> context.newProverEnvironmentWithInterpolation()); }