From b658d4133428535f6bcb47dbecf9772217790ade Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 18 May 2025 08:21:24 +0200 Subject: [PATCH 1/2] CVC5: re-enable concurrency test for Windows. --- src/org/sosy_lab/java_smt/test/SolverContextTest.java | 4 ---- 1 file changed, 4 deletions(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverContextTest.java b/src/org/sosy_lab/java_smt/test/SolverContextTest.java index bef2574fb3..8fc0b7b619 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextTest.java @@ -149,10 +149,6 @@ public void testCVC5WithValidOptions() throws InvalidConfigurationException { public void testCVC5WithValidOptionsTimeLimit() throws InvalidConfigurationException, InterruptedException { assume().that(solverToUse()).isEqualTo(Solvers.CVC5); - assume() - .withMessage("CVC5 has an issue with creating and closing a second context on Windows.") - .that(IS_WINDOWS) - .isFalse(); // tlimit-per is time limit in ms of wall clock time per query var configValid = From b63f6437eea41a490740858298bafa0eb90021a7 Mon Sep 17 00:00:00 2001 From: Karlheinz Friedberger Date: Sun, 18 May 2025 08:31:25 +0200 Subject: [PATCH 2/2] cleanup code --- src/org/sosy_lab/java_smt/test/SolverContextTest.java | 1 - 1 file changed, 1 deletion(-) diff --git a/src/org/sosy_lab/java_smt/test/SolverContextTest.java b/src/org/sosy_lab/java_smt/test/SolverContextTest.java index 8fc0b7b619..3619cd6ce4 100644 --- a/src/org/sosy_lab/java_smt/test/SolverContextTest.java +++ b/src/org/sosy_lab/java_smt/test/SolverContextTest.java @@ -11,7 +11,6 @@ import static com.google.common.truth.Truth.assertThat; import static com.google.common.truth.TruthJUnit.assume; import static org.junit.Assert.assertThrows; -import static org.sosy_lab.java_smt.test.SolverContextFactoryTest.IS_WINDOWS; import org.junit.Test; import org.sosy_lab.common.configuration.InvalidConfigurationException;