Slow while jvm test

UnitTestBot · Jul 25, 2023 · 5ec0a1e · 5ec0a1e
1 parent 6fdaa1f
commit 5ec0a1e
Show file tree

Hide file tree

Showing 2 changed files with 32 additions and 1 deletion.
diff --git a/usvm-jvm/src/samples/java/org/usvm/samples/loops/While.java b/usvm-jvm/src/samples/java/org/usvm/samples/loops/While.java
@@ -48,4 +48,17 @@ public int while1000(int x, int y, int z) {
 
         return 2;
     }
+
+    public int while1000slowConstraints(int x, int y, int z) {
+        int t = y;
+        while (y < 1_000) {
+            y++;
+        }
+
+        if (x == y && (t + 1_000 == y)) {
+            return 1;
+        }
+
+        return 2;
+    }
 }
diff --git a/usvm-jvm/src/test/kotlin/org/usvm/samples/loops/TestWhile.kt b/usvm-jvm/src/test/kotlin/org/usvm/samples/loops/TestWhile.kt
@@ -1,12 +1,20 @@
 package org.usvm.samples.loops
 
-import org.junit.jupiter.api.RepeatedTest
 import org.junit.jupiter.api.Test
+import org.usvm.UMachineOptions
 import org.usvm.samples.JavaMethodTestRunner
 import org.usvm.test.util.checkers.eq
 import org.usvm.test.util.checkers.ignoreNumberOfAnalysisResults
 
 class TestWhile : JavaMethodTestRunner() {
+
+    // Increased limits for loop tests
+    override var options: UMachineOptions = super.options.copy(
+        stepLimit = 100_000UL,
+        timeoutMs = 100_000,
+        stepsFromLastCovered = 100_000
+    )
+
     @Test
     fun `Test singleLoop`() {
         checkDiscoveredProperties(
@@ -50,4 +58,14 @@ class TestWhile : JavaMethodTestRunner() {
             { _, _, _, _, r -> r == 2 },
         )
     }
+
+    @Test
+    fun `Test while1000 slow constraints`() {
+        checkDiscoveredProperties(
+            While::while1000slowConstraints,
+            ignoreNumberOfAnalysisResults,
+            { _, _, _, _, r -> r == 1 },
+            { _, _, _, _, r -> r == 2 },
+        )
+    }
 }