File tree Expand file tree Collapse file tree
usvm-ts/src/main/kotlin/org/usvm/machine/expr Expand file tree Collapse file tree Original file line number Diff line number Diff line change @@ -294,14 +294,13 @@ private fun TsExprResolver.handleArrayPush(
294294 memory.write(lengthLValue, newLength, guard = trueExpr)
295295
296296 // Write the new element to the end of the array
297- // TODO check sorts compatibility https://github.com/UnitTestBot/usvm/issues/300
298- val newIndexLValue = mkArrayIndexLValue(
299- sort = elementSort,
300- ref = array,
297+ assignToArrayIndex(
298+ scope = scope,
299+ array = array,
301300 index = length,
302- type = arrayType ,
303- )
304- memory.write(newIndexLValue, arg.asExpr(elementSort), guard = trueExpr)
301+ expr = arg ,
302+ arrayType = arrayType,
303+ ) ? : return @calcOnState null
305304
306305 // Return the new length of the array (as per ECMAScript spec for Array.push)
307306 mkBvToFpExpr(
You can’t perform that action at this time.
0 commit comments