diff options
| author | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-16 18:28:03 -0400 |
|---|---|---|
| committer | Morgan Deters <mdeters@cs.nyu.edu> | 2013-07-17 17:21:26 -0400 |
| commit | 004bcc12f592991db93ffd92cfb5925940c80980 (patch) | |
| tree | 1bb1db6b03f80b4833a681622f211b6bfaa911b9 /test/regress/regress0/bug521.minimized.smt2 | |
| parent | cffc449795c777217c6412998c7900ad80c389e8 (diff) | |
Fix bug 516; include some bug testcases.
Diffstat (limited to 'test/regress/regress0/bug521.minimized.smt2')
| -rw-r--r-- | test/regress/regress0/bug521.minimized.smt2 | 15 |
1 files changed, 15 insertions, 0 deletions
diff --git a/test/regress/regress0/bug521.minimized.smt2 b/test/regress/regress0/bug521.minimized.smt2 new file mode 100644 index 000000000..6751d4077 --- /dev/null +++ b/test/regress/regress0/bug521.minimized.smt2 @@ -0,0 +1,15 @@ +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(declare-fun _substvar_301_ () Bool) +(declare-fun _substvar_300_ () Bool) +(declare-fun group_size_x () (_ BitVec 32)) +(declare-fun _WRITE_OFFSET_$$p$1@1 () (_ BitVec 32)) +(declare-fun inline$_LOG_WRITE_$$p$1$_offset$1@0 () (_ BitVec 32)) +(declare-fun _WRITE_OFFSET_$$p$1@0 () (_ BitVec 32)) +(declare-fun group_id_x$1 () (_ BitVec 32)) +(declare-fun local_id_x$1 () (_ BitVec 32)) +(declare-fun inline$_LOG_WRITE_$$p$0$_offset$1@0 () (_ BitVec 32)) +(define-fun $foo () Bool (=> true (let ((inline$_LOG_WRITE_$$p$1$_LOG_WRITE_correct (=> true (=> true (=> (= _WRITE_OFFSET_$$p$1@1 (ite _substvar_300_ inline$_LOG_WRITE_$$p$1$_offset$1@0 _WRITE_OFFSET_$$p$1@0)) false))))) (let ((inline$_LOG_WRITE_$$p$1$Entry_correct (=> true (=> (= inline$_LOG_WRITE_$$p$1$_offset$1@0 (bvadd (bvadd (bvmul group_size_x group_id_x$1) local_id_x$1) #x00000001)) (=> true inline$_LOG_WRITE_$$p$1$_LOG_WRITE_correct))))) (let ((inline$$bugle_barrier$0$anon1_Else_correct (=> true (=> true (=> true inline$_LOG_WRITE_$$p$1$Entry_correct))))) (let ((inline$$bugle_barrier$0$Entry_correct (=> true (and _substvar_301_ (=> true (=> true inline$$bugle_barrier$0$anon1_Else_correct)))))) (let (($0$1_correct (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true (=> true inline$$bugle_barrier$0$Entry_correct)))))))))))) (let ((inline$_LOG_WRITE_$$p$0$_LOG_WRITE_correct (=> true (=> true (=> (= _WRITE_OFFSET_$$p$1@0 inline$_LOG_WRITE_$$p$0$_offset$1@0) $0$1_correct))))) (let ((inline$_LOG_WRITE_$$p$0$Entry_correct (=> true (=> (= inline$_LOG_WRITE_$$p$0$_offset$1@0 (bvadd (bvmul group_size_x group_id_x$1) local_id_x$1)) (=> true inline$_LOG_WRITE_$$p$0$_LOG_WRITE_correct))))) (let (($0_correct (=> true (=> true (=> true inline$_LOG_WRITE_$$p$0$Entry_correct))))) $0_correct)))))))))) +(assert (not (=> true $foo))) +(check-sat) +(exit) |