Skip to content

Commit

Permalink
Fix USymbolicArrayCopyAdapter composition (#54)
Browse files Browse the repository at this point in the history
  • Loading branch information
sergeypospelov authored Aug 31, 2023
1 parent 5e44022 commit f41c97a
Showing 1 changed file with 2 additions and 2 deletions.
Original file line number Diff line number Diff line change
Expand Up @@ -55,8 +55,8 @@ abstract class USymbolicArrayCopyAdapter<SrcKey, DstKey>(
keyInfo.cmpConcreteLe(dstFrom, key) && keyInfo.cmpConcreteLe(key, dstTo)

override fun includesSymbolically(key: DstKey, composer: UComposer<*>?): UBoolExpr {
val leftIsLefter = keyInfo.cmpSymbolicLe(ctx, dstFrom, key)
val rightIsRighter = keyInfo.cmpSymbolicLe(ctx, key, dstTo)
val leftIsLefter = keyInfo.cmpSymbolicLe(ctx, keyInfo.mapKey(dstFrom, composer), key)
val rightIsRighter = keyInfo.cmpSymbolicLe(ctx, key, keyInfo.mapKey(dstTo, composer))
val ctx = leftIsLefter.ctx

return ctx.mkAnd(leftIsLefter, rightIsRighter)
Expand Down

0 comments on commit f41c97a

Please sign in to comment.