title: Is there a way to specify the domain of a variable when defining it using an array?
body: <p>My program reads the constraints from a smt2 file, and all the variables are defined as an array. For example</p>
  
  <pre><code>(declare-fun x () (Array (_ BitVec 32) (_ BitVec 8) ) )
  (declare-fun y () (Array (_ BitVec 32) (_ BitVec 8) ) )
  (assert (bvslt  (concat  (select  x (_ bv3 32) ) (concat  (select  x (_ bv2 32) ) (concat  (select  x (_ bv1 32) ) (select  x (_ bv0 32) ) ) ) ) (concat  (select  y (_ bv3 32) ) (concat  (select  y (_ bv2 32) ) (concat  (select  y (_ bv1 32) ) (select  y (_ bv0 32) ) ) ) ) ) )
  (check-sat)
  (exit)
  </code></pre>
  
  <p>Some other constraints are omitted. Sometimes the solver gives a value of x as:</p>
  
  <pre><code>(store (store (store ((as const (Array (_ BitVec 32) (_ BitVec 8))) #xfe)
                       #x00000002
                       #x00)
                #x00000001
                #xff)
         #x00000003
         #x80)
  </code></pre>
  
  <p>According to the definition, each element of the array is a hex value, so the value should be 0x8000fffe. This value is beyond the upper bounds of integer in C++. When I covert it back to int, it is a negative value. So I guess Z3 treats all variables defined by an array as unsigned int. 
  For example, if the constraint is x > y, the solver may give
  x = 0x8000fffe
  and 
  y = 0x00000001. The values satisfy the constraint in unsigned comparison, but when conducting a signed comparison, x is negative and y is positive so it is wrong. I am wondering if there is a way to tell the solver that the numbers are signed when defining them as an array?   </p>
  
  <p>Added 22:26:43 09/14/2019
  I got two smt2 files, one is</p>
  
  <pre><code>(set-logic QF_AUFBV )
  (declare-fun x () (Array (_ BitVec 32) (_ BitVec 8) ) )
  (declare-fun y () (Array (_ BitVec 32) (_ BitVec 8) ) )
  (assert (bvslt  (concat  (select  x (_ bv3 32) ) (concat  (select  x (_ bv2 32) ) (concat  (select  x (_ bv1 32) ) (select  x (_ bv0 32) ) ) ) ) (concat  (select  y (_ bv3 32) ) (concat  (select  y (_ bv2 32) ) (concat  (select  y (_ bv1 32) ) (select  y (_ bv0 32) ) ) ) ) ) )
  (check-sat)
  (exit)
  </code></pre>
  
  <p>The constraint is simply x &lt; y.
  The other one is</p>
  
  <pre><code>(set-logic QF_AUFBV )
  (declare-fun x () (Array (_ BitVec 32) (_ BitVec 8) ) )
  (declare-fun y () (Array (_ BitVec 32) (_ BitVec 8) ) )
  (assert (let ( (?B1 (concat  (select  y (_ bv3 32) ) (concat  (select  y (_ bv2 32) ) (concat  (select  y (_ bv1 32) ) (select  y (_ bv0 32) ) ) ) ) ) (?B2 (concat  (select  x (_ bv3 32) ) (concat  (select  x (_ bv2 32) ) (concat  (select  x (_ bv1 32) ) (select  x (_ bv0 32) ) ) ) ) ) ) (let ( (?B3 (bvsub  ?B1 ?B2 ) ) ) (and  (and  (and  (and  (and  (=  false (=  (_ bv0 32) ?B2 ) ) (=  false (=  (_ bv0 32) ?B1 ) ) ) (=  false (bvslt  ?B1 ?B2 ) ) ) (=  false (=  (_ bv0 32) ?B3 ) ) ) (=  false (bvslt  ?B3 ?B2 ) ) ) (=  (_ bv0 32) (bvsub  ?B3 ?B2 ) ) ) ) ) )
  (check-sat)
  (exit)
  </code></pre>
  
  <p>which is </p>
  
  <pre><code> [(! (0 == x)), 
     (! (0 == y)), 
     (! ( y &lt; x)),
     (! (0 ==( y - x))), 
     (! (( y - x) &lt; x)), 
     (0 ==(( y - x) - x)) ]
  </code></pre>
  
  <p>These smt2 files are generated by Klee.The solver gives</p>
  
  <pre><code>x = (store (store (store ((as const (Array (_ BitVec 32) (_ BitVec 8))) #xfe)
                       #x00000002
                       #x00)
                #x00000001
                #xff)
         #x00000003
         #x80)
  y = before minimize: (store (store (store ((as const (Array (_ BitVec 32) (_ BitVec 8))) #xfc)
                       #x00000002
                       #x01)
                #x00000001
                #xff)
         #x00000003
         #x00)
  </code></pre>
  
  <p>so x=0x8000fffe, and y=0x0001fffc. Converted to decimal, we have x=2147549180, and y=131068. So y-x-x is-4294967296, not decimal 0. The solver thinks it is satisfied bacause 4294967296 is </p>
  
  <pre><code>1 00000000 00000000 00000000 00000000
  </code></pre>
  
  <p>in binary, where the "1" is the 33rd bit, and will be removed. So -4294967296 is considered 0x00 in the memory. This is the reason I asked this question. X and y should be integers, so 0x8000fffe is -0x0000fffe, aka -65534. And y is 131068. And y-x-x is apparently not 0. So in terms of integer, the values don't satisfy the constraints. The expression y - x - x seems to be computed in unsigned rules.</p>