Fixed resolving enum values without any constraints

UnitTestBot · Nov 29, 2023 · caaea27 · caaea27
1 parent c3dc9cb
commit caaea27
Showing 1 changed file with 7 additions and 2 deletions.
diff --git a/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestStateResolver.kt b/usvm-jvm/src/main/kotlin/org/usvm/api/util/JcTestStateResolver.kt
@@ -278,8 +278,13 @@ abstract class JcTestStateResolver<T>(
         val ordinalLValue = UFieldLValue(ctx.sizeSort, heapRef, ctx.enumOrdinalField)
         val ordinalFieldValue = resolvePrimitiveInt(memory.read(ordinalLValue))
 
-        val enumField = enumAncestor.enumValues?.get(ordinalFieldValue)
-            ?: error("Cant find enum field with index $ordinalFieldValue")
+        val enumValues = enumAncestor.enumValues
+            ?: error("Cant find enum values from enum type $enumAncestor")
+
+        val enumField = enumValues.getOrNull(ordinalFieldValue)
+            // It means we do not have any constraints for this enum value (including correctness constraints),
+            // so we can choose any enum value
+            ?: enumValues.first()
 
         return decoderApi.getField(enumField, decoderApi.createNullConst(ctx.cp.objectType))
     }