port_send_msg verification hangs in cex mode with handle_type_is_ptr=on

[priyasiddharth]

Sea-Dsa type aware!
Omnipotent char: omni_i8*
Info: pointer size: 8, word size: 8
Info: Trackable memory is not present
Warning: Skipping global variable marked by llvm.metadata section: @llvm.used
Functions:
NONE
Globals:
0x00000008048000 @.str
0x00000008048010 @g_on_connect_handle
!3 Alloca of 32 bytes: %_0 = alloca [32 x i8], align 16, !sea.dsa.allocsite !328
!3 Alloca of 16 bytes: %_1 = alloca %struct.iovec, align 8, !sea.dsa.allocsite !367
!3 Alloca of 32 bytes: %_2 = alloca %struct.ipc_msg, align 8, !sea.dsa.allocsite !328
!3 Alloca of 24 bytes: %_3 = alloca %struct.uevent, align 8, !sea.dsa.allocsite !370
!3 Alloca of 16 bytes: %_4 = alloca %struct.uuid, align 4, !sea.dsa.allocsite !367
!3 Alloca of 24 bytes: %_5 = alloca %struct.uevent, align 8, !sea.dsa.allocsite !370
!3 Alloca of 16 bytes: %_6 = alloca %struct.ipc_msg_info, align 8, !sea.dsa.allocsite !367
!3 Alloca of 64 bytes: %_7 = alloca [64 x i8], align 16, !sea.dsa.allocsite !375
!3 Alloca of 16 bytes: %_8 = alloca %struct.iovec, align 8, !sea.dsa.allocsite !367
!3 Alloca of 32 bytes: %_9 = alloca %struct.ipc_msg, align 8, !sea.dsa.allocsite !328
!3 Alloca of 40 bytes: %malloc.i8 = alloca %struct._handleState, align 16, !sea.dsa.allocsite !379
!3 Alloca of 40 bytes: %malloc35.i9 = alloca %struct._handleState, align 16, !sea.dsa.allocsite !379
!3 Alloca of 40 bytes: %malloc36.i10 = alloca %struct._handleState, align 16, !sea.dsa.allocsite !379
^CTraceback (most recent call last):
File "/home/siddharth/seahorn/seahorn/build-dbg/run/bin/sea", line 73, in

[priyasiddharth]

On some runs this does not time out (but takes a long time)

https://github.com/seahorn/verifyTrusty/runs/7749844616?check_suite_focus=true