test/regress/regress1/bug543.smt2


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20

; COMMAND-LINE: --incremental
; EXPECT: sat
(set-option :produce-models true)
(set-logic QF_ALL_SUPPORTED)
(declare-fun _substvar_1807_ () Bool)
(declare-fun local_id_x$1 () (_ BitVec 32))
(declare-fun local_id_x$2 () (_ BitVec 32))
(declare-fun $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@5 () (Array Bool (Array (_ BitVec 32) (_ BitVec 32))))
(declare-fun $$_ZZ19bitonic_sort_kernelPfjjE7sh_data () (Array Bool (Array (_ BitVec 32) (_ BitVec 32))))
(declare-fun $0$1@2 () (_ BitVec 32))
(declare-fun $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@0 () (Array Bool (Array (_ BitVec 32) (_ BitVec 32))))
(declare-fun v1$1@0 () (_ BitVec 32))
(declare-fun $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@1 () (Array Bool (Array (_ BitVec 32) (_ BitVec 32))))
(declare-fun v1$2@0 () (_ BitVec 32))
(assert (not (= #b1 #b0)))
(define-fun $_Z19bitonic_sort_kernelPfjj () Bool (=> true (let ((__partitioned_block_$truebb_0$7_correct (=> true (=> true (=> (and true true (= $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@5 (store $$_ZZ19bitonic_sort_kernelPfjjE7sh_data true (store (select $$_ZZ19bitonic_sort_kernelPfjjE7sh_data true) local_id_x$1 $0$1@2))) true true) false))))) (let ((inline$_UPDATE_WRITE_READ_BENIGN_FLAG_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$_UPDATE_BENIGN_FLAG_correct (=> true (=> true __partitioned_block_$truebb_0$7_correct)))) (let ((inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$_LOG_WRITE_correct (=> true (=> true inline$_UPDATE_WRITE_READ_BENIGN_FLAG_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$_UPDATE_BENIGN_FLAG_correct)))) (let ((inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$Entry_correct (=> true (=> true inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$_LOG_WRITE_correct)))) (let ((inline$$bugle_barrier$1$anon8_Then_correct (=> true (=> true inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$Entry_correct)))) (let ((inline$$bugle_barrier$1$anon3_correct (=> true (=> true (=> true (=> true inline$$bugle_barrier$1$anon8_Then_correct)))))) (let ((inline$$bugle_barrier$1$anon7_Then_correct (=> true (=> true inline$$bugle_barrier$1$anon3_correct)))) (let ((inline$$bugle_barrier$1$anon6_Else_correct (=> true (=> true (=> true (=> true inline$$bugle_barrier$1$anon7_Then_correct)))))) (let ((inline$$bugle_barrier$1$Entry_correct (=> true (=> true (=> true inline$$bugle_barrier$1$anon6_Else_correct))))) (let ((__partitioned_block_$truebb_0$4_correct (=> true (=> true (=> true inline$$bugle_barrier$1$Entry_correct))))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$4$_LOG_READ_correct (=> true (=> true __partitioned_block_$truebb_0$4_correct)))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$4$Entry_correct (=> true (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$4$_LOG_READ_correct))))) (let ((__partitioned_block_$truebb_0$3_correct (=> true (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$4$Entry_correct))))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$3$_LOG_READ_correct (=> true (=> true __partitioned_block_$truebb_0$3_correct)))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$3$Entry_correct (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$3$_LOG_READ_correct)))) (let ((__partitioned_block_$truebb_0$2_correct (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$3$Entry_correct)))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$2$_LOG_READ_correct (=> true (=> true __partitioned_block_$truebb_0$2_correct)))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$2$Entry_correct (=> true (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$2$_LOG_READ_correct))))) (let ((__partitioned_block_$truebb_0$1_correct (=> true (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$2$Entry_correct))))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$_LOG_READ_correct (=> true (=> true __partitioned_block_$truebb_0$1_correct)))) (let ((inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$Entry_correct (=> true (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$_LOG_READ_correct))))) (let ((__partitioned_block_$truebb_0_correct (=> true (=> true inline$_LOG_READ_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$1$Entry_correct)))) (let (($1_correct (=> true (=> true (=> true (=> true (=> true __partitioned_block_$truebb_0_correct))))))) (let ((__partitioned_block_$0_0$4_correct (=> true (=> true (=> true (=> true (=> true (=> true (=> true (and _substvar_1807_ (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true $1_correct)))))))))))))))))))))))))))) (let ((inline$$bugle_barrier$0$Return_correct (=> true (=> true __partitioned_block_$0_0$4_correct)))) (let ((inline$$bugle_barrier$0$anon8_Else_correct (=> true (=> true inline$$bugle_barrier$0$Return_correct)))) (let ((inline$$bugle_barrier$0$anon3_correct (=> true (=> true (=> true (=> true inline$$bugle_barrier$0$anon8_Else_correct)))))) (let ((inline$$bugle_barrier$0$anon7_Then_correct (=> true (=> true inline$$bugle_barrier$0$anon3_correct)))) (let ((inline$$bugle_barrier$0$anon6_Else_correct (=> true (=> true (=> true (=> true inline$$bugle_barrier$0$anon7_Then_correct)))))) (let ((inline$$bugle_barrier$0$Entry_correct (=> true (=> true (=> true inline$$bugle_barrier$0$anon6_Else_correct))))) (let ((__partitioned_block_$0_0$3_correct (=> true (=> true (=> (and true true (= $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@0 (store $$_ZZ19bitonic_sort_kernelPfjjE7sh_data true (store (select $$_ZZ19bitonic_sort_kernelPfjjE7sh_data true) local_id_x$1 v1$1@0))) (= $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@1 (store $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@0 false (store (select $$_ZZ19bitonic_sort_kernelPfjjE7sh_data@0 false) local_id_x$2 v1$2@0))) true) inline$$bugle_barrier$0$Entry_correct))))) (let ((inline$_UPDATE_WRITE_READ_BENIGN_FLAG_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$0$_UPDATE_BENIGN_FLAG_correct (=> true (=> true __partitioned_block_$0_0$3_correct)))) (let ((inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$0$_LOG_WRITE_correct (=> true (=> true inline$_UPDATE_WRITE_READ_BENIGN_FLAG_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$0$_UPDATE_BENIGN_FLAG_correct)))) (let ((inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$0$Entry_correct (=> true (=> true inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$0$_LOG_WRITE_correct)))) (let ((__partitioned_block_$0_0$1_correct (=> true (=> true (=> true inline$_LOG_WRITE_$$_ZZ19bitonic_sort_kernelPfjjE7sh_data$0$Entry_correct))))) (let ((inline$_LOG_READ_$$data$0$_LOG_READ_correct (=> true (=> true __partitioned_block_$0_0$1_correct)))) (let ((inline$_LOG_READ_$$data$0$Entry_correct (=> true (=> true inline$_LOG_READ_$$data$0$_LOG_READ_correct)))) (let ((__partitioned_block_$0_0_correct (=> true (=> true (=> true inline$_LOG_READ_$$data$0$Entry_correct))))) (let ((PreconditionGeneratedEntry_correct (=> true (=> true (=> true __partitioned_block_$0_0_correct))))) PreconditionGeneratedEntry_correct)))))))))))))))))))))))))))))))))))))))))
(push 1)
(assert (not (=> true $_Z19bitonic_sort_kernelPfjj)))
(check-sat)