incorrect unsat answer on VC

[yannickmoy]

Z3 4.10 immediately returns unsat on the VC below, which should be satisfiable (although it's hard to check due to the encoding). Other provers return unknown immediately, and any slight change to the VC also makes Z3 return unknown. For example, removing the first declaration for datatype int__ref (which is unused) causes Z3 to return unknown immediately. Or removing the assertion on line 36 giving the value of (unused) constant two_power_size_minus_one also causes Z3 to return unknown immediately.

I reduced the VC as much as I could, but every new removal seems to make the problem go away.

Can I do something on my side to help diagnose the issue further?

(declare-datatypes ((int__ref 0))
  (((int__refqtmk (int__content Int)))))

(declare-datatypes ((bool__ref 0))
  (((bool__refqtmk (bool__content Bool)))))

;; nth
(declare-fun nth ((_ BitVec 16)
  Int) Bool)

;; asr
(declare-fun asr ((_ BitVec 16)
  Int) (_ BitVec 16))

;; lsl
(declare-fun lsl ((_ BitVec 16)
  Int) (_ BitVec 16))

;; abs
(define-fun abs1 ((x Int)) Int
  (ite (<= 0 x) x (- x)))

;; Abs_le
(assert
  (forall ((x Int) (y Int)) (= (<= (abs1 x) y) (and (<= (- y) x) (<= x y)))))

;; Abs_pos
(assert (forall ((x Int)) (<= 0 (abs1 x))))

;; pow2
(declare-fun pow2 (Int) Int)

(declare-const two_power_size_minus_one Int)

;; two_power_size_minus_one_val
(assert (= two_power_size_minus_one (pow2 (- 16 1))))

;; to_int
(define-fun to_int1 ((x (_ BitVec 16))) Int
  (ite (bvsge x (_ bv0 16)) (bv2nat x) (- (- 65536 (bv2nat x)))))

;; asr_bv_is_asr
(assert
  (forall ((x (_ BitVec 16)) (n (_ BitVec 16)))
    (= (bvashr x n) (asr x (bv2nat n)))))

;; lsl_bv_is_lsl
(assert
  (forall ((x (_ BitVec 16)) (n (_ BitVec 16)))
    (= (bvshl x n) (lsl x (bv2nat n)))))

;; min
(define-fun min ((x Int) (y Int)) Int
  (ite (<= x y) x y))

;; max
(define-fun max ((x Int) (y Int)) Int
  (ite (<= x y) y x))

;; Min_r
(assert (forall ((x Int) (y Int)) (=> (<= y x) (= (min x y) y))))

;; Max_l
(assert (forall ((x Int) (y Int)) (=> (<= y x) (= (max x y) x))))

;; Min_comm
(assert (forall ((x Int) (y Int)) (= (min x y) (min y x))))

;; Max_comm
(assert (forall ((x Int) (y Int)) (= (max x y) (max y x))))

;; Min_assoc
(assert
  (forall ((x Int) (y Int) (z Int)) (= (min (min x y) z) (min x (min y z)))))

;; Max_assoc
(assert
  (forall ((x Int) (y Int) (z Int)) (= (max (max x y) z) (max x (max y z)))))

;; nth
(declare-fun nth1 ((_ BitVec 64)
  Int) Bool)

;; asr
(declare-fun asr1 ((_ BitVec 64)
  Int) (_ BitVec 64))

;; lsl
(declare-fun lsl1 ((_ BitVec 64)
  Int) (_ BitVec 64))

(declare-const two_power_size_minus_one1 Int)

;; two_power_size_minus_one_val
(assert (= two_power_size_minus_one1 (pow2 (- 64 1))))

;; to_int
(define-fun to_int2 ((x (_ BitVec 64))) Int
  (ite (bvsge x (_ bv0 64))
    (bv2nat x)
    (- (- 18446744073709551616 (bv2nat x)))))

;; asr_bv_is_asr
(assert
  (forall ((x (_ BitVec 64)) (n (_ BitVec 64)))
    (= (bvashr x n) (asr1 x (bv2nat n)))))

;; lsl_bv_is_lsl
(assert
  (forall ((x (_ BitVec 64)) (n (_ BitVec 64)))
    (= (bvshl x n) (lsl1 x (bv2nat n)))))

;; nth
(declare-fun nth2 ((_ BitVec 32)
  Int) Bool)

;; asr
(declare-fun asr2 ((_ BitVec 32)
  Int) (_ BitVec 32))

;; lsl
(declare-fun lsl2 ((_ BitVec 32)
  Int) (_ BitVec 32))

(declare-const two_power_size_minus_one2 Int)

;; two_power_size_minus_one_val
(assert (= two_power_size_minus_one2 (pow2 (- 32 1))))

;; to_int
(define-fun to_int3 ((x (_ BitVec 32))) Int
  (ite (bvsge x (_ bv0 32)) (bv2nat x) (- (- 4294967296 (bv2nat x)))))

;; asr_bv_is_asr
(assert
  (forall ((x (_ BitVec 32)) (n (_ BitVec 32)))
    (= (bvashr x n) (asr2 x (bv2nat n)))))

;; lsl_bv_is_lsl
(assert
  (forall ((x (_ BitVec 32)) (n (_ BitVec 32)))
    (= (bvshl x n) (lsl2 x (bv2nat n)))))

(declare-sort channel_id_t 0)

;; channel_id_t'int
(declare-fun channel_id_tqtint (channel_id_t) Int)

;; channel_id_t'axiom
(assert
  (forall ((i channel_id_t))
    (and
      (<= (- 1) (channel_id_tqtint i))
      (<= (channel_id_tqtint i) 2147483647))))

;; in_range
(define-fun in_range ((x Int)) Bool
  (and (<= (- 1) x) (<= x 2147483647)))

(declare-const dummy channel_id_t)

;; to_rep
(define-fun to_rep ((x channel_id_t)) Int
  (channel_id_tqtint x))

;; of_rep
(declare-fun of_rep (Int) channel_id_t)

;; inversion_axiom
(assert
  (forall ((x channel_id_t))
    (! (= (of_rep (to_rep x)) x) :pattern ((to_rep x)) )))

;; range_axiom
(assert
  (forall ((x channel_id_t))
    (! (in_range (to_rep x)) :pattern ((to_rep x)) )))

;; coerce_axiom
(assert
  (forall ((x Int))
    (! (=> (in_range x) (= (to_rep (of_rep x)) x)) :pattern ((to_rep
                                                               (of_rep x))) )))

(declare-sort node_descriptor_t 0)

(declare-const attr__ATTRIBUTE_MODULUS (_ BitVec 32))

(declare-const dummy1 node_descriptor_t)

;; to_rep
(declare-fun to_rep1 (node_descriptor_t) (_ BitVec 32))

;; of_rep
(declare-fun of_rep1 ((_ BitVec 32)) node_descriptor_t)

;; inversion_axiom
(assert
  (forall ((x node_descriptor_t))
    (! (= (of_rep1 (to_rep1 x)) x) :pattern ((to_rep1 x)) )))

;; range_axiom
(assert true)

;; coerce_axiom
(assert
  (forall ((x (_ BitVec 32)))
    (! (= (to_rep1 (of_rep1 x)) x) :pattern ((to_rep1 (of_rep1 x))) )))

(declare-sort process_id_t 0)

;; process_id_t'int
(declare-fun process_id_tqtint (process_id_t) Int)

;; process_id_t'axiom
(assert
  (forall ((i process_id_t))
    (and
      (<= (- 2147483648) (process_id_tqtint i))
      (<= (process_id_tqtint i) 2147483647))))

;; in_range
(define-fun in_range1 ((x Int)) Bool
  (and (<= (- 2147483648) x) (<= x 2147483647)))

(declare-const dummy2 process_id_t)

;; to_rep
(define-fun to_rep2 ((x process_id_t)) Int
  (process_id_tqtint x))

;; of_rep
(declare-fun of_rep2 (Int) process_id_t)

;; inversion_axiom
(assert
  (forall ((x process_id_t))
    (! (= (of_rep2 (to_rep2 x)) x) :pattern ((to_rep2 x)) )))

;; range_axiom
(assert
  (forall ((x process_id_t))
    (! (in_range1 (to_rep2 x)) :pattern ((to_rep2 x)) )))

;; coerce_axiom
(assert
  (forall ((x Int))
    (! (=> (in_range1 x) (= (to_rep2 (of_rep2 x)) x)) :pattern ((to_rep2
                                                                  (of_rep2 x))) )))

(declare-sort thread_id_t 0)

;; thread_id_t'int
(declare-fun thread_id_tqtint (thread_id_t) Int)

;; thread_id_t'axiom
(assert
  (forall ((i thread_id_t))
    (and
      (<= (- 2147483648) (thread_id_tqtint i))
      (<= (thread_id_tqtint i) 2147483647))))

;; in_range
(define-fun in_range2 ((x Int)) Bool
  (and (<= (- 2147483648) x) (<= x 2147483647)))

(declare-const dummy3 thread_id_t)

;; to_rep
(define-fun to_rep3 ((x thread_id_t)) Int
  (thread_id_tqtint x))

;; of_rep
(declare-fun of_rep3 (Int) thread_id_t)

;; inversion_axiom
(assert
  (forall ((x thread_id_t))
    (! (= (of_rep3 (to_rep3 x)) x) :pattern ((to_rep3 x)) )))

;; range_axiom
(assert
  (forall ((x thread_id_t))
    (! (in_range2 (to_rep3 x)) :pattern ((to_rep3 x)) )))

;; coerce_axiom
(assert
  (forall ((x Int))
    (! (=> (in_range2 x) (= (to_rep3 (of_rep3 x)) x)) :pattern ((to_rep3
                                                                  (of_rep3 x))) )))

(declare-sort connection_id_t 0)

;; connection_id_t'int
(declare-fun connection_id_tqtint (connection_id_t) Int)

;; connection_id_t'axiom
(assert
  (forall ((i connection_id_t))
    (and
      (<= (- 1) (connection_id_tqtint i))
      (<= (connection_id_tqtint i) 2147483647))))

;; in_range
(define-fun in_range3 ((x Int)) Bool
  (and (<= (- 1) x) (<= x 2147483647)))

(declare-const dummy4 connection_id_t)

;; to_rep
(define-fun to_rep4 ((x connection_id_t)) Int
  (connection_id_tqtint x))

;; of_rep
(declare-fun of_rep4 (Int) connection_id_t)

;; inversion_axiom
(assert
  (forall ((x connection_id_t))
    (! (= (of_rep4 (to_rep4 x)) x) :pattern ((to_rep4 x)) )))

;; range_axiom
(assert
  (forall ((x connection_id_t))
    (! (in_range3 (to_rep4 x)) :pattern ((to_rep4 x)) )))

;; coerce_axiom
(assert
  (forall ((x Int))
    (! (=> (in_range3 x) (= (to_rep4 (of_rep4 x)) x)) :pattern ((to_rep4
                                                                  (of_rep4 x))) )))

(declare-sort thread_priority_t 0)

;; thread_priority_t'int
(declare-fun thread_priority_tqtint (thread_priority_t) Int)

;; thread_priority_t'axiom
(assert
  (forall ((i thread_priority_t))
    (and
      (<= (- 32768) (thread_priority_tqtint i))
      (<= (thread_priority_tqtint i) 32767))))

;; in_range
(define-fun in_range4 ((x Int)) Bool
  (and (<= (- 32768) x) (<= x 32767)))

(declare-const dummy5 thread_priority_t)

;; to_rep
(define-fun to_rep5 ((x thread_priority_t)) Int
  (thread_priority_tqtint x))

;; of_rep
(declare-fun of_rep5 (Int) thread_priority_t)

;; inversion_axiom
(assert
  (forall ((x thread_priority_t))
    (! (= (of_rep5 (to_rep5 x)) x) :pattern ((to_rep5 x)) )))

;; range_axiom
(assert
  (forall ((x thread_priority_t))
    (! (in_range4 (to_rep5 x)) :pattern ((to_rep5 x)) )))

;; coerce_axiom
(assert
  (forall ((x Int))
    (! (=> (in_range4 x) (= (to_rep5 (of_rep5 x)) x)) :pattern ((to_rep5
                                                                  (of_rep5 x))) )))

(declare-sort connect_flags_t 0)

(declare-const attr__ATTRIBUTE_MODULUS1 (_ BitVec 16))

(declare-const dummy6 connect_flags_t)

;; to_rep
(declare-fun to_rep6 (connect_flags_t) (_ BitVec 16))

;; of_rep
(declare-fun of_rep6 ((_ BitVec 16)) connect_flags_t)

;; inversion_axiom
(assert
  (forall ((x connect_flags_t))
    (! (= (of_rep6 (to_rep6 x)) x) :pattern ((to_rep6 x)) )))

;; range_axiom
(assert true)

;; coerce_axiom
(assert
  (forall ((x (_ BitVec 16)))
    (! (= (to_rep6 (of_rep6 x)) x) :pattern ((to_rep6 (of_rep6 x))) )))

(declare-sort size_t 0)

(declare-const attr__ATTRIBUTE_MODULUS2 (_ BitVec 64))

(declare-const dummy7 size_t)

;; to_rep
(declare-fun to_rep7 (size_t) (_ BitVec 64))

;; of_rep
(declare-fun of_rep7 ((_ BitVec 64)) size_t)

;; inversion_axiom
(assert
  (forall ((x size_t))
    (! (= (of_rep7 (to_rep7 x)) x) :pattern ((to_rep7 x)) )))

;; range_axiom
(assert true)

;; coerce_axiom
(assert
  (forall ((x (_ BitVec 64)))
    (! (= (to_rep7 (of_rep7 x)) x) :pattern ((to_rep7 (of_rep7 x))) )))

(declare-sort reserved_32_t 0)

;; reserved_32_t'int
(declare-fun reserved_32_tqtint (reserved_32_t) Int)

;; reserved_32_t'axiom
(assert
  (forall ((i reserved_32_t))
    (and
      (<= (- 2147483648) (reserved_32_tqtint i))
      (<= (reserved_32_tqtint i) 2147483647))))

;; in_range
(define-fun in_range5 ((x Int)) Bool
  (and (<= (- 2147483648) x) (<= x 2147483647)))

(declare-const dummy8 reserved_32_t)

;; to_rep
(define-fun to_rep8 ((x reserved_32_t)) Int
  (reserved_32_tqtint x))

;; of_rep
(declare-fun of_rep8 (Int) reserved_32_t)

;; inversion_axiom
(assert
  (forall ((x reserved_32_t))
    (! (= (of_rep8 (to_rep8 x)) x) :pattern ((to_rep8 x)) )))

;; range_axiom
(assert
  (forall ((x reserved_32_t))
    (! (in_range5 (to_rep8 x)) :pattern ((to_rep8 x)) )))

;; coerce_axiom
(assert
  (forall ((x Int))
    (! (=> (in_range5 x) (= (to_rep8 (of_rep8 x)) x)) :pattern ((to_rep8
                                                                  (of_rep8 x))) )))

(declare-datatypes ((us_split_fields 0))
  (((us_split_fieldsqtmk
    (rec__ada___qnx__neutrino__msg_info64_t__nd node_descriptor_t)(rec__ada___qnx__neutrino__msg_info64_t__srcnd node_descriptor_t)(rec__ada___qnx__neutrino__msg_info64_t__pid process_id_t)(rec__ada___qnx__neutrino__msg_info64_t__tid thread_id_t)(rec__ada___qnx__neutrino__msg_info64_t__chid channel_id_t)(rec__ada___qnx__neutrino__msg_info64_t__scoid connection_id_t)(rec__ada___qnx__neutrino__msg_info64_t__coid connection_id_t)(rec__ada___qnx__neutrino__msg_info64_t__priority thread_priority_t)(rec__ada___qnx__neutrino__msg_info64_t__flags connect_flags_t)(rec__ada___qnx__neutrino__msg_info64_t__msglen size_t)(rec__ada___qnx__neutrino__msg_info64_t__srcmsglen size_t)(rec__ada___qnx__neutrino__msg_info64_t__dstmsglen size_t)(rec__ada___qnx__neutrino__msg_info64_t__type_id connection_id_t)(rec__ada___qnx__neutrino__msg_info64_t__reserved reserved_32_t)))))

(declare-datatypes ((us_split_fields__ref 0))
  (((us_split_fields__refqtmk (us_split_fields__content us_split_fields)))))

(declare-datatypes ((us_rep 0))
  (((us_repqtmk (us_split_fields1 us_split_fields)))))

(declare-const value__size Int)

(declare-const object__size Int)

(declare-const alignment Int)

;; value__size_axiom
(assert (<= 0 value__size))

;; object__size_axiom
(assert (<= 0 object__size))

;; alignment_axiom
(assert (<= 0 alignment))

(declare-const ada___qnx__neutrino__msg_info64_t__nd__first__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__nd__last__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__nd__position Int)

;; ada___qnx__neutrino__msg_info64_t__nd__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__nd__first__bit))

;; ada___qnx__neutrino__msg_info64_t__nd__last__bit_axiom
(assert
  (< ada___qnx__neutrino__msg_info64_t__nd__first__bit ada___qnx__neutrino__msg_info64_t__nd__last__bit))

;; ada___qnx__neutrino__msg_info64_t__nd__position_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__nd__position))

(declare-const ada___qnx__neutrino__msg_info64_t__srcnd__first__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__srcnd__last__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__srcnd__position Int)

;; ada___qnx__neutrino__msg_info64_t__srcnd__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__srcnd__first__bit))

;; ada___qnx__neutrino__msg_info64_t__srcnd__last__bit_axiom
(assert
  (< ada___qnx__neutrino__msg_info64_t__srcnd__first__bit ada___qnx__neutrino__msg_info64_t__srcnd__last__bit))

;; ada___qnx__neutrino__msg_info64_t__srcnd__position_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__srcnd__position))

(declare-const ada___qnx__neutrino__msg_info64_t__pid__first__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__pid__last__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__pid__position Int)

;; ada___qnx__neutrino__msg_info64_t__pid__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__pid__first__bit))

;; ada___qnx__neutrino__msg_info64_t__pid__last__bit_axiom
(assert
  (< ada___qnx__neutrino__msg_info64_t__pid__first__bit ada___qnx__neutrino__msg_info64_t__pid__last__bit))

;; ada___qnx__neutrino__msg_info64_t__pid__position_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__pid__position))

(declare-const ada___qnx__neutrino__msg_info64_t__tid__first__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__tid__last__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__tid__position Int)

;; ada___qnx__neutrino__msg_info64_t__tid__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__tid__first__bit))

;; ada___qnx__neutrino__msg_info64_t__tid__last__bit_axiom
(assert
  (< ada___qnx__neutrino__msg_info64_t__tid__first__bit ada___qnx__neutrino__msg_info64_t__tid__last__bit))

;; ada___qnx__neutrino__msg_info64_t__tid__position_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__tid__position))

(declare-const ada___qnx__neutrino__msg_info64_t__chid__first__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__chid__last__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__chid__position Int)

;; ada___qnx__neutrino__msg_info64_t__chid__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__chid__first__bit))

;; ada___qnx__neutrino__msg_info64_t__chid__last__bit_axiom
(assert
  (< ada___qnx__neutrino__msg_info64_t__chid__first__bit ada___qnx__neutrino__msg_info64_t__chid__last__bit))

;; ada___qnx__neutrino__msg_info64_t__chid__position_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__chid__position))

(declare-const ada___qnx__neutrino__msg_info64_t__scoid__first__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__scoid__last__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__scoid__position Int)

;; ada___qnx__neutrino__msg_info64_t__scoid__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__scoid__first__bit))

;; ada___qnx__neutrino__msg_info64_t__scoid__last__bit_axiom
(assert
  (< ada___qnx__neutrino__msg_info64_t__scoid__first__bit ada___qnx__neutrino__msg_info64_t__scoid__last__bit))

;; ada___qnx__neutrino__msg_info64_t__scoid__position_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__scoid__position))

(declare-const ada___qnx__neutrino__msg_info64_t__coid__first__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__coid__last__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__coid__position Int)

;; ada___qnx__neutrino__msg_info64_t__coid__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__coid__first__bit))

;; ada___qnx__neutrino__msg_info64_t__coid__last__bit_axiom
(assert
  (< ada___qnx__neutrino__msg_info64_t__coid__first__bit ada___qnx__neutrino__msg_info64_t__coid__last__bit))

;; ada___qnx__neutrino__msg_info64_t__coid__position_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__coid__position))

(declare-const ada___qnx__neutrino__msg_info64_t__priority__first__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__priority__last__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__priority__position Int)

;; ada___qnx__neutrino__msg_info64_t__priority__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__priority__first__bit))

;; ada___qnx__neutrino__msg_info64_t__priority__last__bit_axiom
(assert
  (< ada___qnx__neutrino__msg_info64_t__priority__first__bit ada___qnx__neutrino__msg_info64_t__priority__last__bit))

;; ada___qnx__neutrino__msg_info64_t__priority__position_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__priority__position))

(declare-const ada___qnx__neutrino__msg_info64_t__flags__first__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__flags__last__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__flags__position Int)

;; ada___qnx__neutrino__msg_info64_t__flags__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__flags__first__bit))

;; ada___qnx__neutrino__msg_info64_t__flags__last__bit_axiom
(assert
  (< ada___qnx__neutrino__msg_info64_t__flags__first__bit ada___qnx__neutrino__msg_info64_t__flags__last__bit))

;; ada___qnx__neutrino__msg_info64_t__flags__position_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__flags__position))

(declare-const ada___qnx__neutrino__msg_info64_t__msglen__first__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__msglen__last__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__msglen__position Int)

;; ada___qnx__neutrino__msg_info64_t__msglen__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__msglen__first__bit))

;; ada___qnx__neutrino__msg_info64_t__msglen__last__bit_axiom
(assert
  (< ada___qnx__neutrino__msg_info64_t__msglen__first__bit ada___qnx__neutrino__msg_info64_t__msglen__last__bit))

;; ada___qnx__neutrino__msg_info64_t__msglen__position_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__msglen__position))

(declare-const ada___qnx__neutrino__msg_info64_t__srcmsglen__first__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__srcmsglen__last__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__srcmsglen__position Int)

;; ada___qnx__neutrino__msg_info64_t__srcmsglen__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__srcmsglen__first__bit))

;; ada___qnx__neutrino__msg_info64_t__srcmsglen__last__bit_axiom
(assert
  (< ada___qnx__neutrino__msg_info64_t__srcmsglen__first__bit ada___qnx__neutrino__msg_info64_t__srcmsglen__last__bit))

;; ada___qnx__neutrino__msg_info64_t__srcmsglen__position_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__srcmsglen__position))

(declare-const ada___qnx__neutrino__msg_info64_t__dstmsglen__first__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__dstmsglen__last__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__dstmsglen__position Int)

;; ada___qnx__neutrino__msg_info64_t__dstmsglen__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__dstmsglen__first__bit))

;; ada___qnx__neutrino__msg_info64_t__dstmsglen__last__bit_axiom
(assert
  (< ada___qnx__neutrino__msg_info64_t__dstmsglen__first__bit ada___qnx__neutrino__msg_info64_t__dstmsglen__last__bit))

;; ada___qnx__neutrino__msg_info64_t__dstmsglen__position_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__dstmsglen__position))

(declare-const ada___qnx__neutrino__msg_info64_t__type_id__first__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__type_id__last__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__type_id__position Int)

;; ada___qnx__neutrino__msg_info64_t__type_id__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__type_id__first__bit))

;; ada___qnx__neutrino__msg_info64_t__type_id__last__bit_axiom
(assert
  (< ada___qnx__neutrino__msg_info64_t__type_id__first__bit ada___qnx__neutrino__msg_info64_t__type_id__last__bit))

;; ada___qnx__neutrino__msg_info64_t__type_id__position_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__type_id__position))

(declare-const ada___qnx__neutrino__msg_info64_t__reserved__first__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__reserved__last__bit Int)

(declare-const ada___qnx__neutrino__msg_info64_t__reserved__position Int)

;; ada___qnx__neutrino__msg_info64_t__reserved__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__reserved__first__bit))

;; ada___qnx__neutrino__msg_info64_t__reserved__last__bit_axiom
(assert
  (< ada___qnx__neutrino__msg_info64_t__reserved__first__bit ada___qnx__neutrino__msg_info64_t__reserved__last__bit))

;; ada___qnx__neutrino__msg_info64_t__reserved__position_axiom
(assert (<= 0 ada___qnx__neutrino__msg_info64_t__reserved__position))

(declare-const dummy9 us_rep)

(declare-datatypes ((msg_info_t__ref 0))
  (((msg_info_t__refqtmk (msg_info_t__content us_rep)))))

;; state
(declare-fun state (Int) Int)

;; state__function_guard
(declare-fun state__function_guard (Int
  Int) Bool)

(declare-sort errno_t 0)

;; in_range
(define-fun in_range6 ((x Int)) Bool
  (and (<= 0 x) (<= x 134)))

(declare-const dummy10 errno_t)

(declare-sort unsigned_16 0)

(declare-const attr__ATTRIBUTE_MODULUS3 (_ BitVec 16))

(declare-const dummy11 unsigned_16)

;; to_rep
(declare-fun to_rep9 (unsigned_16) (_ BitVec 16))

;; of_rep
(declare-fun of_rep9 ((_ BitVec 16)) unsigned_16)

;; inversion_axiom
(assert
  (forall ((x unsigned_16))
    (! (= (of_rep9 (to_rep9 x)) x) :pattern ((to_rep9 x)) )))

;; range_axiom
(assert true)

;; coerce_axiom
(assert
  (forall ((x (_ BitVec 16)))
    (! (= (to_rep9 (of_rep9 x)) x) :pattern ((to_rep9 (of_rep9 x))) )))

(declare-sort integer_8 0)

;; integer_8'int
(declare-fun integer_8qtint (integer_8) Int)

;; integer_8'axiom
(assert
  (forall ((i integer_8))
    (and (<= (- 128) (integer_8qtint i)) (<= (integer_8qtint i) 127))))

;; in_range
(define-fun in_range7 ((x Int)) Bool
  (and (<= (- 128) x) (<= x 127)))

(declare-const dummy12 integer_8)

;; to_rep
(define-fun to_rep10 ((x integer_8)) Int
  (integer_8qtint x))

;; of_rep
(declare-fun of_rep10 (Int) integer_8)

;; inversion_axiom
(assert
  (forall ((x integer_8))
    (! (= (of_rep10 (to_rep10 x)) x) :pattern ((to_rep10 x)) )))

;; range_axiom
(assert
  (forall ((x integer_8))
    (! (in_range7 (to_rep10 x)) :pattern ((to_rep10 x)) )))

;; coerce_axiom
(assert
  (forall ((x Int))
    (! (=> (in_range7 x) (= (to_rep10 (of_rep10 x)) x)) :pattern ((to_rep10
                                                                    (of_rep10
                                                                    x))) )))

(declare-sort zero_8_t 0)

;; zero_8_t'int
(declare-fun zero_8_tqtint (zero_8_t) Int)

;; zero_8_t'axiom
(assert
  (forall ((i zero_8_t))
    (and (<= 0 (zero_8_tqtint i)) (<= (zero_8_tqtint i) 0))))

;; in_range
(define-fun in_range8 ((x Int)) Bool
  (and (<= 0 x) (<= x 0)))

(declare-const dummy13 zero_8_t)

;; to_rep
(define-fun to_rep11 ((x zero_8_t)) Int
  (zero_8_tqtint x))

;; of_rep
(declare-fun of_rep11 (Int) zero_8_t)

;; inversion_axiom
(assert
  (forall ((x zero_8_t))
    (! (= (of_rep11 (to_rep11 x)) x) :pattern ((to_rep11 x)) )))

;; range_axiom
(assert
  (forall ((x zero_8_t))
    (! (in_range8 (to_rep11 x)) :pattern ((to_rep11 x)) )))

;; coerce_axiom
(assert
  (forall ((x Int))
    (! (=> (in_range8 x) (= (to_rep11 (of_rep11 x)) x)) :pattern ((to_rep11
                                                                    (of_rep11
                                                                    x))) )))

;; bool_eq
(define-fun bool_eq ((a (Array Int zero_8_t)) (a__first Int) (a__last Int) (b (Array Int zero_8_t)) (b__first Int) (b__last Int)) Bool
  (ite (and
         (ite (<= a__first a__last)
           (and
             (<= b__first b__last)
             (= (- a__last a__first) (- b__last b__first)))
           (< b__last b__first))
         (forall ((temp___idx_169 Int))
           (=>
             (and (<= a__first temp___idx_169) (<= temp___idx_169 a__last))
             (= (to_rep11 (select a temp___idx_169)) (to_rep11
                                                       (select b (+ (- b__first a__first) temp___idx_169)))))))
    true
    false))

;; bool_eq_rev
(assert
  (forall ((a (Array Int zero_8_t)) (b (Array Int zero_8_t)))
    (forall ((a__first Int) (a__last Int) (b__first Int) (b__last Int))
      (=>
        (= (bool_eq b b__first b__last a a__first a__last) true)
        (and
          (ite (<= a__first a__last)
            (and
              (<= b__first b__last)
              (= (- a__last a__first) (- b__last b__first)))
            (< b__last b__first))
          (forall ((temp___idx_169 Int))
            (=>
              (and (<= a__first temp___idx_169) (<= temp___idx_169 a__last))
              (= (to_rep11 (select a temp___idx_169)) (to_rep11
                                                        (select b (+ (- b__first a__first) temp___idx_169)))))))))))

(declare-const dummy14 (Array Int zero_8_t))

(declare-const value__size1 Int)

(declare-const object__size1 Int)

(declare-const component__size Int)

(declare-const alignment1 Int)

(declare-sort sigval_kind_t 0)

;; in_range
(define-fun in_range9 ((x Int)) Bool
  (and (<= 0 x) (<= x 1)))

(declare-const dummy15 sigval_kind_t)

;; to_rep
(declare-fun to_rep12 (sigval_kind_t) Int)

;; of_rep
(declare-fun of_rep12 (Int) sigval_kind_t)

;; inversion_axiom
(assert
  (forall ((x sigval_kind_t))
    (! (= (of_rep12 (to_rep12 x)) x) :pattern ((to_rep12 x)) )))

;; range_axiom
(assert
  (forall ((x sigval_kind_t))
    (! (in_range9 (to_rep12 x)) :pattern ((to_rep12 x)) )))

;; coerce_axiom
(assert
  (forall ((x Int))
    (! (=> (in_range9 x) (= (to_rep12 (of_rep12 x)) x)) :pattern ((to_rep12
                                                                    (of_rep12
                                                                    x))) )))

(declare-sort sival_int_t 0)

;; sival_int_t'int
(declare-fun sival_int_tqtint (sival_int_t) Int)

;; sival_int_t'axiom
(assert
  (forall ((i sival_int_t))
    (and
      (<= (- 2147483648) (sival_int_tqtint i))
      (<= (sival_int_tqtint i) 2147483647))))

;; in_range
(define-fun in_range10 ((x Int)) Bool
  (and (<= (- 2147483648) x) (<= x 2147483647)))

(declare-const dummy16 sival_int_t)

;; to_rep
(define-fun to_rep13 ((x sival_int_t)) Int
  (sival_int_tqtint x))

;; of_rep
(declare-fun of_rep13 (Int) sival_int_t)

;; inversion_axiom
(assert
  (forall ((x sival_int_t))
    (! (= (of_rep13 (to_rep13 x)) x) :pattern ((to_rep13 x)) )))

;; range_axiom
(assert
  (forall ((x sival_int_t))
    (! (in_range10 (to_rep13 x)) :pattern ((to_rep13 x)) )))

;; coerce_axiom
(assert
  (forall ((x Int))
    (! (=> (in_range10 x) (= (to_rep13 (of_rep13 x)) x)) :pattern ((to_rep13
                                                                    (of_rep13
                                                                    x))) )))

(declare-sort address 0)

(declare-const attr__ATTRIBUTE_MODULUS4 (_ BitVec 64))

(declare-const dummy17 address)

;; to_rep
(declare-fun to_rep14 (address) (_ BitVec 64))

;; of_rep
(declare-fun of_rep14 ((_ BitVec 64)) address)

;; inversion_axiom
(assert
  (forall ((x address))
    (! (= (of_rep14 (to_rep14 x)) x) :pattern ((to_rep14 x)) )))

;; coerce_axiom
(assert
  (forall ((x (_ BitVec 64)))
    (! (= (to_rep14 (of_rep14 x)) x) :pattern ((to_rep14 (of_rep14 x))) )))

(declare-datatypes ((us_split_discrs 0))
  (((us_split_discrsqtmk
    (rec__ada___qnx__siginfo__sigval_t__kind sigval_kind_t)))))

(declare-datatypes ((us_split_fields2 0))
  (((us_split_fieldsqtmk1
    (rec__ada___qnx__siginfo__sigval_t__sival_int sival_int_t)(rec__ada___qnx__siginfo__sigval_t__sival_ptr address)))))

(declare-datatypes ((us_rep1 0))
  (((us_repqtmk1
    (us_split_discrs1 us_split_discrs)(us_split_fields3 us_split_fields2)))))

(declare-const value__size2 Int)

(declare-const object__size2 Int)

(declare-const alignment2 Int)

;; value__size_axiom
(assert (<= 0 value__size2))

;; object__size_axiom
(assert (<= 0 object__size2))

;; alignment_axiom
(assert (<= 0 alignment2))

(declare-const ada___qnx__siginfo__sigval_t__kind__first__bit Int)

(declare-const ada___qnx__siginfo__sigval_t__kind__last__bit Int)

(declare-const ada___qnx__siginfo__sigval_t__kind__position Int)

;; ada___qnx__siginfo__sigval_t__kind__first__bit_axiom
(assert (<= 0 ada___qnx__siginfo__sigval_t__kind__first__bit))

;; ada___qnx__siginfo__sigval_t__kind__last__bit_axiom
(assert
  (< ada___qnx__siginfo__sigval_t__kind__first__bit ada___qnx__siginfo__sigval_t__kind__last__bit))

;; ada___qnx__siginfo__sigval_t__kind__position_axiom
(assert (<= 0 ada___qnx__siginfo__sigval_t__kind__position))

(declare-const ada___qnx__siginfo__sigval_t__sival_int__first__bit Int)

(declare-const ada___qnx__siginfo__sigval_t__sival_int__last__bit Int)

(declare-const ada___qnx__siginfo__sigval_t__sival_int__position Int)

;; ada___qnx__siginfo__sigval_t__sival_int__first__bit_axiom
(assert (<= 0 ada___qnx__siginfo__sigval_t__sival_int__first__bit))

;; ada___qnx__siginfo__sigval_t__sival_int__last__bit_axiom
(assert
  (< ada___qnx__siginfo__sigval_t__sival_int__first__bit ada___qnx__siginfo__sigval_t__sival_int__last__bit))

;; ada___qnx__siginfo__sigval_t__sival_int__position_axiom
(assert (<= 0 ada___qnx__siginfo__sigval_t__sival_int__position))

(declare-const ada___qnx__siginfo__sigval_t__sival_ptr__first__bit Int)

(declare-const ada___qnx__siginfo__sigval_t__sival_ptr__last__bit Int)

(declare-const ada___qnx__siginfo__sigval_t__sival_ptr__position Int)

;; ada___qnx__siginfo__sigval_t__sival_ptr__first__bit_axiom
(assert (<= 0 ada___qnx__siginfo__sigval_t__sival_ptr__first__bit))

;; ada___qnx__siginfo__sigval_t__sival_ptr__last__bit_axiom
(assert
  (< ada___qnx__siginfo__sigval_t__sival_ptr__first__bit ada___qnx__siginfo__sigval_t__sival_ptr__last__bit))

;; ada___qnx__siginfo__sigval_t__sival_ptr__position_axiom
(assert (<= 0 ada___qnx__siginfo__sigval_t__sival_ptr__position))

(declare-const dummy18 us_rep1)

(declare-datatypes ((us_split_fields4 0))
  (((us_split_fieldsqtmk2
    (rec__ada___qnx__neutrino__pulse_t__the_type unsigned_16)(rec__ada___qnx__neutrino__pulse_t__the_subtype unsigned_16)(rec__ada___qnx__neutrino__pulse_t__code integer_8)(rec__ada___qnx__neutrino__pulse_t__zero (Array Int zero_8_t))(rec__ada___qnx__neutrino__pulse_t__value us_rep1)(rec__ada___qnx__neutrino__pulse_t__scoid connection_id_t)))))

(declare-datatypes ((us_rep2 0))
  (((us_repqtmk2 (us_split_fields5 us_split_fields4)))))

(declare-const value__size3 Int)

(declare-const object__size3 Int)

(declare-const alignment3 Int)

;; value__size_axiom
(assert (<= 0 value__size3))

;; object__size_axiom
(assert (<= 0 object__size3))

;; alignment_axiom
(assert (<= 0 alignment3))

(declare-const ada___qnx__neutrino__pulse_t__the_type__first__bit Int)

(declare-const ada___qnx__neutrino__pulse_t__the_type__last__bit Int)

(declare-const ada___qnx__neutrino__pulse_t__the_type__position Int)

;; ada___qnx__neutrino__pulse_t__the_type__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__pulse_t__the_type__first__bit))

;; ada___qnx__neutrino__pulse_t__the_type__last__bit_axiom
(assert
  (< ada___qnx__neutrino__pulse_t__the_type__first__bit ada___qnx__neutrino__pulse_t__the_type__last__bit))

;; ada___qnx__neutrino__pulse_t__the_type__position_axiom
(assert (<= 0 ada___qnx__neutrino__pulse_t__the_type__position))

(declare-const ada___qnx__neutrino__pulse_t__the_subtype__first__bit Int)

(declare-const ada___qnx__neutrino__pulse_t__the_subtype__last__bit Int)

(declare-const ada___qnx__neutrino__pulse_t__the_subtype__position Int)

;; ada___qnx__neutrino__pulse_t__the_subtype__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__pulse_t__the_subtype__first__bit))

;; ada___qnx__neutrino__pulse_t__the_subtype__last__bit_axiom
(assert
  (< ada___qnx__neutrino__pulse_t__the_subtype__first__bit ada___qnx__neutrino__pulse_t__the_subtype__last__bit))

;; ada___qnx__neutrino__pulse_t__the_subtype__position_axiom
(assert (<= 0 ada___qnx__neutrino__pulse_t__the_subtype__position))

(declare-const ada___qnx__neutrino__pulse_t__code__first__bit Int)

(declare-const ada___qnx__neutrino__pulse_t__code__last__bit Int)

(declare-const ada___qnx__neutrino__pulse_t__code__position Int)

;; ada___qnx__neutrino__pulse_t__code__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__pulse_t__code__first__bit))

;; ada___qnx__neutrino__pulse_t__code__last__bit_axiom
(assert
  (< ada___qnx__neutrino__pulse_t__code__first__bit ada___qnx__neutrino__pulse_t__code__last__bit))

;; ada___qnx__neutrino__pulse_t__code__position_axiom
(assert (<= 0 ada___qnx__neutrino__pulse_t__code__position))

(declare-const ada___qnx__neutrino__pulse_t__zero__first__bit Int)

(declare-const ada___qnx__neutrino__pulse_t__zero__last__bit Int)

(declare-const ada___qnx__neutrino__pulse_t__zero__position Int)

;; ada___qnx__neutrino__pulse_t__zero__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__pulse_t__zero__first__bit))

;; ada___qnx__neutrino__pulse_t__zero__last__bit_axiom
(assert
  (< ada___qnx__neutrino__pulse_t__zero__first__bit ada___qnx__neutrino__pulse_t__zero__last__bit))

;; ada___qnx__neutrino__pulse_t__zero__position_axiom
(assert (<= 0 ada___qnx__neutrino__pulse_t__zero__position))

(declare-const ada___qnx__neutrino__pulse_t__value__first__bit Int)

(declare-const ada___qnx__neutrino__pulse_t__value__last__bit Int)

(declare-const ada___qnx__neutrino__pulse_t__value__position Int)

;; ada___qnx__neutrino__pulse_t__value__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__pulse_t__value__first__bit))

;; ada___qnx__neutrino__pulse_t__value__last__bit_axiom
(assert
  (< ada___qnx__neutrino__pulse_t__value__first__bit ada___qnx__neutrino__pulse_t__value__last__bit))

;; ada___qnx__neutrino__pulse_t__value__position_axiom
(assert (<= 0 ada___qnx__neutrino__pulse_t__value__position))

(declare-const ada___qnx__neutrino__pulse_t__scoid__first__bit Int)

(declare-const ada___qnx__neutrino__pulse_t__scoid__last__bit Int)

(declare-const ada___qnx__neutrino__pulse_t__scoid__position Int)

;; ada___qnx__neutrino__pulse_t__scoid__first__bit_axiom
(assert (<= 0 ada___qnx__neutrino__pulse_t__scoid__first__bit))

;; ada___qnx__neutrino__pulse_t__scoid__position_axiom
(assert (<= 0 ada___qnx__neutrino__pulse_t__scoid__position))

(declare-const dummy19 us_rep2)

(declare-datatypes ((connection_id_t__init_wrapper 0))
  (((connection_id_t__init_wrapperqtmk
    (rec__value connection_id_t)(us_attr__init Bool)))))

(declare-const dummy20 connection_id_t__init_wrapper)

;; dummy__def
(assert (= (us_attr__init dummy20) false))

(declare-datatypes ((unsigned_16__init_wrapper 0))
  (((unsigned_16__init_wrapperqtmk
    (rec__value1 unsigned_16)(us_attr__init1 Bool)))))

(declare-const dummy21 unsigned_16__init_wrapper)

(declare-datatypes ((integer_8__init_wrapper 0))
  (((integer_8__init_wrapperqtmk
    (rec__value2 integer_8)(us_attr__init2 Bool)))))

(declare-datatypes ((zero_8_t__init_wrapper 0))
  (((zero_8_t__init_wrapperqtmk (rec__value3 zero_8_t)(us_attr__init3 Bool)))))

;; convert
(declare-fun convert ((Array Int zero_8_t__init_wrapper)) (Array Int zero_8_t))

;; convert__def
(assert
  (forall ((a (Array Int zero_8_t__init_wrapper)))
    (forall ((temp___170 Int))
      (= (to_rep11 (of_rep11 (to_rep11 (rec__value3 (select a temp___170)))))
      (to_rep11
        (select (convert a) temp___170))))))

;; convert
(declare-fun convert1 ((Array Int zero_8_t)) (Array Int zero_8_t__init_wrapper))

;; convert__def
(assert
  (forall ((a (Array Int zero_8_t)))
    (let ((b (convert1 a)))
      (forall ((temp___171 Int))
        (and
          (= (us_attr__init3
               (zero_8_t__init_wrapperqtmk
                 (of_rep11 (to_rep11 (select a temp___171)))
                 true)) (us_attr__init3 (select b temp___171)))
          (= (to_rep11
               (rec__value3
                 (zero_8_t__init_wrapperqtmk
                   (of_rep11 (to_rep11 (select a temp___171)))
                   true))) (to_rep11 (rec__value3 (select b temp___171)))))))))

(declare-datatypes ((sival_int_t__init_wrapper 0))
  (((sival_int_t__init_wrapperqtmk
    (rec__value4 sival_int_t)(us_attr__init4 Bool)))))

(declare-datatypes ((address__init_wrapper 0))
  (((address__init_wrapperqtmk (rec__value5 address)(us_attr__init5 Bool)))))

(declare-const dummy25 address__init_wrapper)

(declare-datatypes ((us_split_fields6 0))
  (((us_split_fieldsqtmk3
    (rec__ada___qnx__siginfo__sigval_t__sival_int1 sival_int_t__init_wrapper)(rec__ada___qnx__siginfo__sigval_t__sival_ptr1 address__init_wrapper)))))

(declare-datatypes ((sigval_t__init_wrapper 0))
  (((sigval_t__init_wrapperqtmk
    (us_split_discrs2 us_split_discrs)(us_split_fields7 us_split_fields6)))))

;; ada___qnx__siginfo__sigval_t__sival_int__pred
(define-fun ada___qnx__siginfo__sigval_t__sival_int__pred ((a sigval_t__init_wrapper)) Bool
  (= (to_rep12
       (rec__ada___qnx__siginfo__sigval_t__kind (us_split_discrs2 a))) 0))

;; ada___qnx__siginfo__sigval_t__sival_ptr__pred
(define-fun ada___qnx__siginfo__sigval_t__sival_ptr__pred ((a sigval_t__init_wrapper)) Bool
  (= (to_rep12
       (rec__ada___qnx__siginfo__sigval_t__kind (us_split_discrs2 a))) 1))

(declare-datatypes ((us_split_fields8 0))
  (((us_split_fieldsqtmk4
    (rec__ada___qnx__neutrino__pulse_t__the_type1 unsigned_16__init_wrapper)(rec__ada___qnx__neutrino__pulse_t__the_subtype1 unsigned_16__init_wrapper)(rec__ada___qnx__neutrino__pulse_t__code1 integer_8__init_wrapper)(rec__ada___qnx__neutrino__pulse_t__zero1 (Array Int zero_8_t__init_wrapper))(rec__ada___qnx__neutrino__pulse_t__value1 sigval_t__init_wrapper)(rec__ada___qnx__neutrino__pulse_t__scoid1 connection_id_t__init_wrapper)))))

(declare-const pulse__split_fields us_split_fields8)

(declare-const chid1 Int)

(declare-const status1 Int)

(assert
  (or
    (or
      (= status1 11)
      (or
        (= status1 22)
        (or
          (= status1 12)
          (or (= status1 74) (or (= status1 1) (= status1 48))))))
    (and (= status1 0) (= (state chid1) 1))))

(assert (and (<= 0 status1) (<= status1 134)))

;; Assume
(assert
  (and
    (and
      (= (to_rep9
           (rec__value1
             (rec__ada___qnx__neutrino__pulse_t__the_type1
               pulse__split_fields))) #x0000)
      (= (us_attr__init1
           (rec__ada___qnx__neutrino__pulse_t__the_type1 pulse__split_fields)) true))
    (and
      (and
        (and
          (= (to_rep9
               (rec__value1
                 (rec__ada___qnx__neutrino__pulse_t__the_subtype1
                   pulse__split_fields))) #x0000)
          (= (us_attr__init1
               (rec__ada___qnx__neutrino__pulse_t__the_subtype1
                 pulse__split_fields)) true))
        (forall ((temp___479 Int))
          (=>
            (and (<= 0 temp___479) (<= temp___479 2))
            (let ((temp___480 (select (rec__ada___qnx__neutrino__pulse_t__zero1
                                        pulse__split_fields) temp___479)))
              (and
                (= (to_rep11 (rec__value3 temp___480)) 0)
                (= (us_attr__init3 temp___480) true))))))
      (= (to_rep12
           (rec__ada___qnx__siginfo__sigval_t__kind
             (us_split_discrs2
               (rec__ada___qnx__neutrino__pulse_t__value1
                 pulse__split_fields)))) 0))))

(declare-const status2 Int)

(declare-const pulse__split_fields1 us_split_fields8)

(assert
  (or
    (or (= status2 14) (or (= status2 4) (or (= status2 3) (= status2 117))))
    (and
      (= status2 0)
      (and
        (= (us_attr__init1
             (rec__ada___qnx__neutrino__pulse_t__the_type1
               pulse__split_fields1)) true)
        (and
          (and
            (and
              (= (us_attr__init1
                   (rec__ada___qnx__neutrino__pulse_t__the_subtype1
                     pulse__split_fields1)) true)
              (= (us_attr__init2
                   (rec__ada___qnx__neutrino__pulse_t__code1
                     pulse__split_fields1)) true))
            (forall ((temp___422 Int))
              (=>
                (and (<= 0 temp___422) (<= temp___422 2))
                (= (us_attr__init3
                     (select (rec__ada___qnx__neutrino__pulse_t__zero1
                               pulse__split_fields1) temp___422)) true))))
          (and
            (let ((temp___424 (rec__ada___qnx__neutrino__pulse_t__value1
                                pulse__split_fields1)))
              (and
                (=>
                  (ada___qnx__siginfo__sigval_t__sival_int__pred temp___424)
                  (= (us_attr__init4
                       (rec__ada___qnx__siginfo__sigval_t__sival_int1
                         (us_split_fields7 temp___424))) true))
                (=>
                  (ada___qnx__siginfo__sigval_t__sival_ptr__pred temp___424)
                  (= (us_attr__init5
                       (rec__ada___qnx__siginfo__sigval_t__sival_ptr1
                         (us_split_fields7 temp___424))) true))))
            (= (us_attr__init
                 (rec__ada___qnx__neutrino__pulse_t__scoid1
                   pulse__split_fields1)) true)))))))

(assert (and (<= 0 status2) (<= status2 134)))

(check-sat)

[NikolajBjorner]

running with solver.axioms2files=true produces a ton of files (I had to fix a few bugs in how the files are generated). Some of the files are SAT (z3 returns unknown, but it is really SAT), which pinpoints the bug. The next step is to break or log more at the offending lemma (for me it is lemma number 10465 when using smt.random_seed=3).

[NikolajBjorner]

Turns out the theory axioms all double checked. To minimize, the following script works

from z3 import *

s1 = Solver()
s1.from_file("C:/z3/build/6270.smt2")

asserts = s1.assertions()

while True:
    progress = False
    fmls = { f for f in asserts }
    for a in asserts:
        fmls -= { a }
        found = False
        print("try", len(fmls), a)
        for i in range(10):
            s = Solver()
            s.set("random_seed", i)
            s.set("timeout", 2000)
            s.add(fmls)
            if unsat == s.check():
                print("unsat", i)
                progress = True
                found = True
                break
        if not found:
            print("not unsat")
            fmls |= { a }
    asserts = list(fmls)
    if not progress:
        print(s.sexpr())
        break

It produces

(declare-sort zero_8_t 0)
(declare-datatypes ((zero_8_t__init_wrapper 0)) (((zero_8_t__init_wrapperqtmk (rec__value3 zero_8_t) (us_attr__init3 Bool)))))
(declare-fun zero_8_tqtint (zero_8_t) Int)
(declare-fun of_rep11 (Int) zero_8_t)
(declare-fun convert1 ((Array Int zero_8_t)) (Array Int zero_8_t__init_wrapper))
(assert (forall ((x zero_8_t))
  (! (= (of_rep11 (zero_8_tqtint x)) x) :pattern ((zero_8_tqtint x)))))
(assert (forall ((x zero_8_t))
  (! (and (<= 0 (zero_8_tqtint x)) (<= (zero_8_tqtint x) 0))
     :pattern ((zero_8_tqtint x)))))
(assert (forall ((a (Array Int zero_8_t)) (temp___171 Int))
  (let ((a!1 (zero_8_tqtint (of_rep11 (zero_8_tqtint (select a temp___171)))))
        (a!2 (zero_8_tqtint (rec__value3 (select (convert1 a) temp___171)))))
    (and (us_attr__init3 (select (convert1 a) temp___171)) (= a!1 a!2)))))

[NikolajBjorner]

The command-line doesn't repro well with the above API based minimization. This approach works better:

from z3 import *

def parse_commands(ins):
    buffer = ""
    lp = 0
    rp = 0
    for line in ins:
        for ch in line:
            if ch == '(':
                lp += 1
            elif ch == ')':
                rp += 1
            if lp > 0:
                buffer += ch
            if lp > 0 and lp == rp:
                yield buffer
                lp = 0
                rp = 0
                buffer = ""

def get_cmds():
    with open("C:/z3/build/6270.smt2") as ins:
        for cmd in parse_commands(ins):
            yield cmd

def save_cmds(file, cmds):
    with open(file, 'w') as ous:
        for cmd in cmds:
            ous.write(cmd)
            ous.write("\n")

cmds = list(get_cmds())
print(list(cmds))

import subprocess
import re

has_unsat = re.compile("unsat")

while True:
    progress = False
    for i in range(len(cmds)):
        cmd = cmds[i]
        if cmd.startswith("(assert"):
            found = False
            cmds[i] = "(echo \"removed\")"
            save_cmds("tmp.smt2", cmds)
            for seed in range(10):
                out = subprocess.Popen(f"C:\\z3\\release\\z3.exe tmp.smt2 /T:2 smt.random_seed={seed}", stdout=subprocess.PIPE).communicate()[0]
                if out != None:
                    out = out.decode(sys.stdout.encoding)
                    print(out)
                    found = has_unsat.search(out)
                    if found:
                        progress = True
                        break
            if not found:
                cmds[i] = cmd
            else:
                save_cmds("repro.smt2", cmds)
    if not progress:
        break

The bug appears to be that MBQI introduces fresh distinct values for elements in the domain of zero_8_t. The domain of zero_8_t can only have a single element, though. So MBQI leaks assertions (that there are distinct elements) in a domain when there arent.

[zhendongsu]

Not sure, but the following minimization/reduction might be of help:

[508] % z3release small.smt2
unsat
[509] % cat small.smt2
(declare-sort g 0)
(declare-datatypes ((p 0)) (((b (q g)))))
(declare-datatypes ((r 0)) (((s (ac Bool)))))
(declare-datatypes ((t 0)) (((u (v Bool)))))
(declare-datatypes ((w 0)) (((d (x Bool)))))
(declare-datatypes ((y 0)) (((z (ae g) (af Bool)))))
(declare-datatypes ((ak 0)) (((g (am Bool)))))
(declare-datatypes ((an 0)) (((ax (ao Bool)))))
(declare-datatypes ((ap 0)) (((aq (ar ak) (ay an)))))
(declare-datatypes ((az 0)) (((cv (ca p) (cb ap)))))
(declare-datatypes ((ce 0)) (((cf (cg t)(ch t) (ci w) (cj (Array Int y)) (ck az) (cl r)))))
(declare-fun h (g) Int)
(declare-fun l (Int) g)
(declare-fun ag ((Array Int y)) (Array Int g))
(declare-fun ai ((Array Int g)) (Array Int y))
(define-fun cz ((a az)) Bool true)
(declare-fun cm () Int)
(declare-fun cn () ce)
(assert (forall ((i g)) (= 0 (h i))))
(assert (forall ((k g)) (= (l (h k)) k)))
(assert (forall ((a (Array Int y)) (ah Int)) (= (h (l (h (ae (select a ah))))) (h (select (ag a) ah)))))
(assert (forall ((a (Array Int g)) (aj Int)) (= (af (z (l (h (select a aj))) true)) (af (select (ai a) aj)))))
(assert (forall ((a (Array Int g)) (aj Int)) (= (h (ae (z (l (h (select a aj))) true))) (h (ae (select (ai a) aj))))))
(assert (or (= cm 0) (ac (cl cn)) (and (v (cg cn)) (v (ch cn)) (x (ci cn)) (am (ar (cb (ck cn)))) (not (ao (ay (cb (ck cn))))))))
(check-sat)

[yannickmoy]

great! thanks for the fix and the fantastic investigation, looks like it was a fun one...