Refactor regressions (#1581)

1 files changed, 20 insertions, 0 deletions

diff --git a/test/regress/regress1/bug543.smt2 b/test/regress/regress1/bug543.smt2
new file mode 100644
index 000000000..9155de7a9
--- /dev/null
+++ b/test/regress/regress1/bug543.smt2
@@ -0,0 +1,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)
+