Z3 returns unknown with HORN logic if I use a specific operation

Question

I am using HORN logic in order to solve a problem with Z3. The code works until I put in one assert the following operation: ip_dst *namevar* or ip_src *namevar* where ip_dst and ip_src are defined as follows:

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

And I don't know to solve the problem.

In the assert statement, I need to compare the bitwise AND of (ip_dst namevar) and a specific constant with another constant.

The full code is as follows:

(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) Int Int (Array Int (Array Int MatrixElement))) Bool)

... ...

(assert (forall ((tabella Int) (priorita Int) (header (Array Int ArrayElement)) (riga_instradamento Int)
(nrighe Int) (tab_instradamento (Array Int (Array Int MatrixElement)))
(tabellap Int) (prioritap Int) (headerp (Array Int ArrayElement)) 
(riga_instradamentop Int)(nrighep Int) (tab_instradamentop (Array Int (Array Int MatrixElement))))

  (=>


   (and


    (= tabella 2)

    (= priorita (* 1 (+ 1 nrighe) ))

    (= (bvand (ip_dst (select header 1)) #b11111111111111111111111100000000) #b00001010000010100000101000000000)

             ....other conditions....

    (status tabella priorita header riga_instradamento nrighe tab_instradamento)

   
    )
    (status tabellap prioritap headerp riga_instradamentop nrighep tab_instradamentop)
   )

  ))
                        

....

(check-sat)

I thought about declaring the variable "header" in a different way. I considered substituting it with two variables of the appropriate type (_ BitVec 32), but I would like to keep the variables as they are. Is there a different way to do the same thing? Thanks.

I tried to split the operation into three equalities, as follows:

(= var (select header 3))

(= var1 (ip_dst var))

(= (bvand var1 #b....) #b....)

However, the error message still highlighted the ip_dst *namevar* operation as the problem, and the result remained the same. I also tried using bitwise shifting operations, but this did not work either.

Here an 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)