Try remove cvc5 limits

UnitTestBot · Oct 18, 2024 · 1d89dad · 1d89dad
1 parent 9a354dc
commit 1d89dad
Showing 1 changed file with 1 addition and 10 deletions.
diff --git a/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/Cvc5BenchmarksBasedTest.kt b/ksmt-test/src/test/kotlin/io/ksmt/test/benchmarks/Cvc5BenchmarksBasedTest.kt
@@ -36,16 +36,7 @@ class Cvc5BenchmarksBasedTest : BenchmarksBasedTest() {
         @JvmStatic
         fun cvc5TestData() = testData()
 
-        /**
-         * Resource limit to prevent solver from consuming huge amounts of native memory.
-         * The value is measured in some abstract resource usage units and chosen to maintain
-         * a balance between resource usage and the number of unknown check-sat results.
-         * */
-        const val RESOURCE_LIMIT = 4000
-
         fun KSolverRunnerManager.createCvc5TestSolver(ctx: KContext) =
-            createSolver(ctx, KCvc5Solver::class).apply {
-                configure { setCvc5Option("rlimit", "$RESOURCE_LIMIT") }
-            }
+            createSolver(ctx, KCvc5Solver::class)
     }
 }