From 44b128e30400c723d4a74c14dd5861d595e933c3 Mon Sep 17 00:00:00 2001 From: Sergey Pospelov Date: Mon, 4 Sep 2023 11:31:46 +0300 Subject: [PATCH] Fix lower bound for length --- .../kotlin/org/usvm/api/collection/ObjectMapCollectionApi.kt | 2 +- 1 file changed, 1 insertion(+), 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 index b35e81abd9..af2ca545de 100644 --- 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) } }