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

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)