From a28db70f0f9c2e4b2111f7cd1a63f024ed03121c Mon Sep 17 00:00:00 2001
From: Levente Bajczi <bajczilevi@gmail.com>
Date: Tue, 9 Jul 2024 00:36:58 +0200
Subject: [PATCH] fixed tests for mac and win

---
 .../solver/smtlib/SmtLibHornSolverTest.kt     | 12 ++++++++----
 .../hu/bme/mit/theta/xcfa2chc/TestChcUtils.kt | 19 +++++++++----------
 2 files changed, 17 insertions(+), 14 deletions(-)

diff --git a/subprojects/solver/solver-smtlib/src/test/java/hu/bme/mit/theta/solver/smtlib/SmtLibHornSolverTest.kt b/subprojects/solver/solver-smtlib/src/test/java/hu/bme/mit/theta/solver/smtlib/SmtLibHornSolverTest.kt
index 73d869a91f..47f3e05a1d 100644
--- a/subprojects/solver/solver-smtlib/src/test/java/hu/bme/mit/theta/solver/smtlib/SmtLibHornSolverTest.kt
+++ b/subprojects/solver/solver-smtlib/src/test/java/hu/bme/mit/theta/solver/smtlib/SmtLibHornSolverTest.kt
@@ -30,6 +30,7 @@ import hu.bme.mit.theta.core.type.inttype.IntExprs.Int
 import hu.bme.mit.theta.core.type.inttype.IntType
 import hu.bme.mit.theta.solver.SolverFactory
 import hu.bme.mit.theta.solver.smtlib.solver.installer.SmtLibSolverInstallerException
+import org.junit.Assume
 import org.junit.jupiter.api.*
 import org.junit.jupiter.params.ParameterizedTest
 import org.junit.jupiter.params.provider.Arguments
@@ -51,7 +52,7 @@ class SmtLibHornSolverTest {
 
         @JvmStatic
         fun solvers(): List<Arguments> {
-            return solverFactories.map { Arguments.of(it.key, it.value) }
+            return SOLVERS.map { Arguments.of(it) }
         }
 
         @BeforeAll
@@ -94,7 +95,8 @@ class SmtLibHornSolverTest {
 
     @ParameterizedTest(name = "[{index}] {0}")
     @MethodSource("solvers")
-    fun testSolvable(name: Pair<String, String>, solverFactory: SolverFactory) {
+    fun testSolvable(name: Pair<String, String>) {
+        val solverFactory = solverFactories[name]!!
         val solver = solverFactory.createHornSolver()
         solver.use { hornSolver ->
             val p = ParamHolder(Int())
@@ -137,7 +139,8 @@ class SmtLibHornSolverTest {
 
     @ParameterizedTest(name = "[{index}] {0}")
     @MethodSource("solvers")
-    fun testUnsolvable(name: Pair<String, String>, solverFactory: SolverFactory) {
+    fun testUnsolvable(name: Pair<String, String>) {
+        val solverFactory = solverFactories[name]!!
         val solver = solverFactory.createHornSolver()
 
         solver.use { hornSolver ->
@@ -165,7 +168,8 @@ class SmtLibHornSolverTest {
 
     @ParameterizedTest(name = "[{index}] {0}")
     @MethodSource("solvers")
-    fun testNonlinearUnsolvable(name: Pair<String, String>, solverFactory: SolverFactory) {
+    fun testNonlinearUnsolvable(name: Pair<String, String>) {
+        val solverFactory = solverFactories[name]!!
         val solver = solverFactory.createHornSolver()
 
         solver.use { hornSolver ->
diff --git a/subprojects/xcfa/xcfa2chc/src/test/java/hu/bme/mit/theta/xcfa2chc/TestChcUtils.kt b/subprojects/xcfa/xcfa2chc/src/test/java/hu/bme/mit/theta/xcfa2chc/TestChcUtils.kt
index 01a0f2003a..d248d52529 100644
--- a/subprojects/xcfa/xcfa2chc/src/test/java/hu/bme/mit/theta/xcfa2chc/TestChcUtils.kt
+++ b/subprojects/xcfa/xcfa2chc/src/test/java/hu/bme/mit/theta/xcfa2chc/TestChcUtils.kt
@@ -34,7 +34,9 @@ import hu.bme.mit.theta.solver.SolverFactory
 import hu.bme.mit.theta.solver.SolverStatus
 import hu.bme.mit.theta.solver.smtlib.SmtLibSolverManager
 import hu.bme.mit.theta.solver.smtlib.solver.installer.SmtLibSolverInstallerException
-import org.junit.jupiter.api.*
+import org.junit.jupiter.api.AfterAll
+import org.junit.jupiter.api.Assertions
+import org.junit.jupiter.api.BeforeAll
 import org.junit.jupiter.params.ParameterizedTest
 import org.junit.jupiter.params.provider.Arguments
 import org.junit.jupiter.params.provider.MethodSource
@@ -56,8 +58,8 @@ class TestChcUtils {
         )
 
         @JvmStatic
-        fun solvers(): List<Arguments> {
-            return solverFactories.map { Arguments.of(it.key, it.value) }
+        fun solvers(): List<Arguments?> {
+            return SOLVERS.map { Arguments.of(it) }
         }
 
         @BeforeAll
@@ -93,14 +95,10 @@ class TestChcUtils {
         }
     }
 
-    @BeforeEach
-    fun before() {
-        Assumptions.assumeTrue(OsHelper.getOs() == OsHelper.OperatingSystem.LINUX)
-    }
-
     @ParameterizedTest(name = "[{index}] {0}")
     @MethodSource("solvers")
-    fun testPetersonManualCounting(name: Pair<String, String>, solverFactory: SolverFactory) {
+    fun testPetersonManualCounting(name: Pair<String, String>) {
+        val solverFactory = solverFactories[name]!!
         val i2i = ArrayType.of(Int(), Int())
 
         val pI = ParamHolder(Int())
@@ -400,7 +398,8 @@ class TestChcUtils {
 
     @ParameterizedTest(name = "[{index}] {0}")
     @MethodSource("solvers")
-    fun testPetersonNoCounting(name: Pair<String, String>, solverFactory: SolverFactory) {
+    fun testPetersonNoCounting(name: Pair<String, String>) {
+        val solverFactory = solverFactories[name]!!
         val i2i = ArrayType.of(Int(), Int())
 
         val pI = ParamHolder(Int())