Potential non-termination or bitvector performance

[dc-mak]

18:36 ➜  z3 --version
Z3 version 4.13.0 - 64 bit

mwe.smt.txt

contents of mwe.smt.txt

(set-option :print-success true)
(set-option :produce-models true)
(declare-datatype cn_tuple_0 ((cn_tuple_0)))
(declare-datatype cn_tuple_2
 (par (a0 a1) ((cn_tuple_2 (cn_get_0_of_2 a0) (cn_get_1_of_2 a1)))))
(declare-datatype pointer
 ((NULL) (AiA (alloc_id cn_tuple_0) (addr (_ BitVec 64)))))
(declare-datatype int_list_498
 ((int_list_498 (head_struct_fld (_ BitVec 32)) (tail_struct_fld pointer))))
(declare-datatype int_queue_520
 ((int_queue_520 (front_struct_fld pointer) (back_struct_fld pointer))))
(declare-datatype int_queueCell_521
 ((int_queueCell_521 (first_struct_fld (_ BitVec 32))
   (next_struct_fld pointer))))
(declare-datatypes ((seq_472 0))
 (((Seq_Nil_507)
   (Seq_Cons_508 (head_data_fld (_ BitVec 32)) (tail_data_fld seq_472)))))
(declare-fun unpack_IntQueuePtr1_708 () (cn_tuple_2 int_queue_520 seq_472))
(assert
 (or
  (and (= (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) NULL)
   (= (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) NULL))
  (and
   (not (= (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) NULL))
   (not (= (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)) NULL)))))
(declare-fun default_uf_9 () pointer)
; A
(assert
 (=
  (bvurem
   (match (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708))
    (((NULL) #x0000000000000000) ((AiA alloc_id addr) addr)))
   #x0000000000000008)
  #x0000000000000000))
(declare-fun default_uf_10 () cn_tuple_0)
(declare-fun ambiguous_719 () Bool)
(assert
 (= ambiguous_719
  (and
   (and
    (and
     ((_ is AiA) (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)))
     ((_ is AiA) (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708))))
    (not
     (=
      (match (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708))
       (((NULL) default_uf_10) ((AiA alloc_id addr) alloc_id)))
      (match (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708))
       (((NULL) default_uf_10) ((AiA alloc_id addr) alloc_id))))))
   (=
    (match (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708))
     (((NULL) #x0000000000000000) ((AiA alloc_id addr) addr)))
    (match (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708))
     (((NULL) #x0000000000000000) ((AiA alloc_id addr) addr)))))))
(declare-fun both_eq_720 () Bool)
(assert
 (= both_eq_720
  (= (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708))
   (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708)))))
(declare-fun neither_721 () Bool)
(assert (= neither_721 (and (not both_eq_720) (not ambiguous_719))))
(declare-fun ptrEq_722 () Bool)
(assert (and (=> both_eq_720 ptrEq_722) (=> neither_721 (not ptrEq_722))))
(push 1)
(assert ptrEq_722)
(push 1)
; B
; (assert
;  (and
;   (not
;    (=
;     (match (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708))
;      (((NULL) default_uf_9)
;       ((AiA alloc_id addr)
;        (AiA alloc_id
;         addr))))
;     (match (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708))
;      (((NULL) default_uf_9)
;       ((AiA alloc_id addr)
;        (AiA alloc_id
;         addr))))))))
(assert
 (and
  (not
   (=
    (match (front_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708))
     (((NULL) default_uf_9)
      ((AiA alloc_id addr)
       (AiA alloc_id
        (bvadd addr (bvmul #x0000000000000001 #x0000000000000004))))))
    (match (back_struct_fld (cn_get_0_of_2 unpack_IntQueuePtr1_708))
     (((NULL) default_uf_9)
      ((AiA alloc_id addr)
       (AiA alloc_id
        (bvadd addr (bvmul #x0000000000000001 #x0000000000000004))))))))))
(check-sat)

The file as is doesn't seem to terminate (the original bigger file this was cut down for ran for about 6 hours on GitHub CI before being cancelled).

If you comment assertion "A", then it takes a while but does come back correctly with unsat.

If you uncomment assertion "B", then it will come back with unsat quickly.

This may be related to #7295