Allow forks with the same path in random path selector (#50)

UnitTestBot · Aug 17, 2023 · 65eeeba · 65eeeba
1 parent fc7e03b
commit 65eeeba
Showing 1 changed file with 4 additions and 1 deletion.
diff --git a/usvm-core/src/main/kotlin/org/usvm/ps/RandomTreePathSelector.kt b/usvm-core/src/main/kotlin/org/usvm/ps/RandomTreePathSelector.kt
@@ -57,7 +57,10 @@ internal class RandomTreePathSelector<State : UState<*, *, *, Statement, *, Stat
             }
 
             // Leaf if reached
-            val nodeFromThisSelector = currentNode.states.singleOrNull { it in states }
+            // Note that we may have several nodes satisfying the predicate here since
+            // they might be created because of type forks or approximation forks.
+            // In such case, they have the same path but different path constraints.
+            val nodeFromThisSelector = currentNode.states.firstOrNull { it in states }
             if (nodeFromThisSelector != null) {
                 peekedState = nodeFromThisSelector
                 break