Fix lower bound for length

UnitTestBot · Sep 4, 2023 · 44b128e · 44b128e
1 parent aced3ce
commit 44b128e
Showing 1 changed file with 1 addition and 1 deletion.
diff --git a/usvm-core/src/main/kotlin/org/usvm/api/collection/ObjectMapCollectionApi.kt b/usvm-core/src/main/kotlin/org/usvm/api/collection/ObjectMapCollectionApi.kt
@@ -116,7 +116,7 @@ object ObjectMapCollectionApi {
         val sizeLowerBound = mkIte(mkBvSignedGreaterExpr(srcMapSize, dstMapSize), srcMapSize, dstMapSize)
         val sizeUpperBound = mkBvAddExpr(srcMapSize, dstMapSize)
         pathConstraints += mkBvSignedGreaterOrEqualExpr(mergedMapSize, sizeLowerBound)
-        pathConstraints += mkBvSignedGreaterOrEqualExpr(mergedMapSize, sizeUpperBound)
+        pathConstraints += mkBvSignedLessOrEqualExpr(mergedMapSize, sizeUpperBound)
         memory.write(UMapLengthLValue(dstRef, mapType), mergedMapSize, guard = trueExpr)
     }
 }