使用Z3 HORN逻辑时调用ip_dst/ip_src操作返回unknown的问题

我在使用Z3的HORN逻辑解决问题，原本代码运行正常，但在断言中加入ip_dst *变量名*或ip_src *变量名*操作后，Z3返回unknown。其中ip_dst和ip_src是通过以下构造函数声明的：

(declare-datatypes () ((ArrayElement
                        (Ip_src (ip_src (_ BitVec 32)))
                        (Ip_dst (ip_dst (_ BitVec 32)))
)))

我需要在断言中比较(ip_dst 变量)与特定常量的按位AND结果和另一个常量是否相等。尝试过将操作拆分为多个等式、使用移位操作等方法，都没解决问题。希望保留现有变量结构，寻求可行的解决办法。

以下是最小复现示例（MRE）：

(set-logic HORN)
  
(declare-datatypes () ((ArrayElement
                        (Ip_src (ip_src (_ BitVec 32)))
                        (Ip_dst (ip_dst (_ BitVec 32)))
                        )))

(declare-fun status (Int Int (Array Int ArrayElement) ) Bool)


;state 0

(assert (forall ((tabella Int) (priorita Int) (header (Array Int ArrayElement))
                )
                (=>
                    (and
                        (= tabella 0)                   
                        (= (select header 0) (Ip_src #b00001010000010100000101011101111))   ;IP_SRC
                        (= (select header 1) (Ip_dst #b00001010000010100000101000011111))   ;IP_DST 
                    )
                    (status tabella priorita header)
                )
        )
)

;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;;; 

;transitions

(assert (forall ((tabella Int) (priorita Int) (header (Array Int ArrayElement)) 
                (tabellap Int) (prioritap Int) (headerp (Array Int ArrayElement))
                )
                
                (=> 
                    (and
                        (= tabella 0) 

                                (= priorita 1 ) 
                            
                                (= (bvand (ip_src (select header 0)) #b11111111111111111111111100000000) #b00001010000010100000101000000000)
                            
                                (= tabellap -1) 
                        
                                (= (select header 0) (select headerp 0))    
                                (= (select header 1) (select headerp 1))    
                                (= (select header 2) (select headerp 2))    
                                (= (select header 3) (select headerp 3))    
                            
                    
                        (status tabella priorita header )
                    )
                    (status tabellap prioritap headerp )
                )
))

(assert (forall ((tabella Int) (priorita Int) (header (Array Int ArrayElement)) 
                (tabellap Int) (prioritap Int) (headerp (Array Int ArrayElement))
                )
                
                (=> 
                    (and
                        (= tabella 0) ;la regola è applicata se siamo nella tabella 2

                                (= priorita 1 ) 

                                (= (bvand (ip_dst (select header 1)) #b11111111111111111111111100000000) #b00001010000010100000101000000000)
                            
                                (= tabellap -2) 
                        
                                (= (select header 0) (select headerp 0))    
                                (= (select header 1) (select headerp 1))    
                                (= (select header 2) (select headerp 2))    
                                (= (select header 3) (select headerp 3))    
                            
                    
                        (status tabella priorita header )
                    )
                    (status tabellap prioritap headerp )
                )
))
                            

(assert (forall ((tabella Int) (priorita Int) (header (Array Int ArrayElement)) 
                )
        (=>
            (and
                (= tabella -1)
                (status tabella priorita header )
            )
        false
        )
))

(set-option :timeout 0)
(check-sat)
(get-model)

内容的提问来源于stack exchange，提问作者MaTh