diff options
Diffstat (limited to 'test/regress/regress1/bug521.smt2')
| -rw-r--r-- | test/regress/regress1/bug521.smt2 | 323 |
1 files changed, 323 insertions, 0 deletions
diff --git a/test/regress/regress1/bug521.smt2 b/test/regress/regress1/bug521.smt2 new file mode 100644 index 000000000..8f840a1f6 --- /dev/null +++ b/test/regress/regress1/bug521.smt2 @@ -0,0 +1,323 @@ +;(set-option :produce-unsat-cores true) +(set-option :incremental true) +(set-option :print-success false) +(set-info :smt-lib-version 2.0) +(set-info :status sat) +(set-option :produce-models true) +(set-logic ALL_SUPPORTED) +; done setting options + +; Boogie universal background predicate +; Copyright (c) 2004-2010, Microsoft Corp. +(set-info :category "industrial") +(declare-sort |T@U| 0) +(declare-sort |T@T| 0) +(declare-fun real_pow (Real Real) Real) +(declare-fun UOrdering2 (|T@U| |T@U|) Bool) +(declare-fun UOrdering3 (|T@T| |T@U| |T@U|) Bool) + +(declare-fun group_size_y () (_ BitVec 32)) +(declare-fun group_size_z () (_ BitVec 32)) +(declare-fun num_groups_y () (_ BitVec 32)) +(declare-fun num_groups_z () (_ BitVec 32)) +(declare-fun group_size_x () (_ BitVec 32)) +(declare-fun num_groups_x () (_ BitVec 32)) +(declare-fun ControlFlow (Int Int) Int) +(declare-fun %lbl%+1458 () Bool) +(declare-fun %lbl%@3203 () Bool) +(declare-fun _WRITE_HAS_OCCURRED_$$p$1@2 () Bool) +(declare-fun _WRITE_SOURCE_$$p$1@2 () (_ BitVec 32)) +(declare-fun %lbl%@3213 () Bool) +(declare-fun _READ_HAS_OCCURRED_$$p$1 () Bool) +(declare-fun _READ_SOURCE_$$p$1 () (_ BitVec 32)) +(declare-fun %lbl%@3225 () Bool) +(declare-fun %lbl%@3240 () Bool) +(declare-fun %lbl%+1440 () Bool) +(declare-fun $mv_state (Int Int) Bool) +(declare-fun $mv_state_const () Int) +(declare-fun call465formal@_offset$2@0 () (_ BitVec 32)) +(declare-fun group_id_x$2 () (_ BitVec 32)) +(declare-fun local_id_x$2 () (_ BitVec 32)) +(declare-fun call465formal@_value$2@0 () (_ BitVec 32)) +(declare-fun %lbl%@3060 () Bool) +(declare-fun _WRITE_HAS_OCCURRED_$$p$1@1 () Bool) +(declare-fun _WRITE_OFFSET_$$p$1@1 () (_ BitVec 32)) +(declare-fun _WRITE_VALUE_$$p$1@1 () (_ BitVec 32)) +(declare-fun %lbl%@3078 () Bool) +(declare-fun _READ_OFFSET_$$p$1 () (_ BitVec 32)) +(declare-fun _READ_VALUE_$$p$1 () (_ BitVec 32)) +(declare-fun %lbl%@3099 () Bool) +(declare-fun _WRITE_SOURCE_$$p$1@1 () (_ BitVec 32)) +(declare-fun %lbl%@3109 () Bool) +(declare-fun %lbl%@3121 () Bool) +(declare-fun %lbl%@3136 () Bool) +(declare-fun %lbl%+1434 () Bool) +(declare-fun inline$_LOG_WRITE_$$p$1$track@1 () Bool) +(declare-fun _WRITE_HAS_OCCURRED_$$p$1@0 () Bool) +(declare-fun inline$_LOG_WRITE_$$p$1$_offset$1@0 () (_ BitVec 32)) +(declare-fun _WRITE_OFFSET_$$p$1@0 () (_ BitVec 32)) +(declare-fun inline$_LOG_WRITE_$$p$1$_value$1@0 () (_ BitVec 32)) +(declare-fun _WRITE_VALUE_$$p$1@0 () (_ BitVec 32)) +(declare-fun _WRITE_SOURCE_$$p$1@0 () (_ BitVec 32)) +(declare-fun %lbl%+1432 () Bool) +(declare-fun group_id_x$1 () (_ BitVec 32)) +(declare-fun local_id_x$1 () (_ BitVec 32)) +(declare-fun %lbl%+1328 () Bool) +(declare-fun group_id_y$1 () (_ BitVec 32)) +(declare-fun group_id_y$2 () (_ BitVec 32)) +(declare-fun group_id_z$1 () (_ BitVec 32)) +(declare-fun group_id_z$2 () (_ BitVec 32)) +(declare-fun %lbl%+1330 () Bool) +(declare-fun %lbl%+1324 () Bool) +(declare-fun %lbl%@2798 () Bool) +(declare-fun %lbl%+1334 () Bool) +(declare-fun call397formal@_offset$2@0 () (_ BitVec 32)) +(declare-fun call397formal@_value$2@0 () (_ BitVec 32)) +(declare-fun %lbl%@2667 () Bool) +(declare-fun %lbl%@2685 () Bool) +(declare-fun %lbl%@2706 () Bool) +(declare-fun %lbl%@2716 () Bool) +(declare-fun %lbl%@2728 () Bool) +(declare-fun %lbl%@2743 () Bool) +(declare-fun %lbl%+1189 () Bool) +(declare-fun inline$_LOG_WRITE_$$p$0$track@1 () Bool) +(declare-fun _WRITE_HAS_OCCURRED_$$p$1 () Bool) +(declare-fun inline$_LOG_WRITE_$$p$0$_offset$1@0 () (_ BitVec 32)) +(declare-fun _WRITE_OFFSET_$$p$1 () (_ BitVec 32)) +(declare-fun inline$_LOG_WRITE_$$p$0$_value$1@0 () (_ BitVec 32)) +(declare-fun _WRITE_VALUE_$$p$1 () (_ BitVec 32)) +(declare-fun _WRITE_SOURCE_$$p$1 () (_ BitVec 32)) +(declare-fun %lbl%+1187 () Bool) +(declare-fun %lbl%+1462 () Bool) +(declare-fun local_id_y$1 () (_ BitVec 32)) +(declare-fun local_id_y$2 () (_ BitVec 32)) +(declare-fun local_id_z$1 () (_ BitVec 32)) +(declare-fun local_id_z$2 () (_ BitVec 32)) +(assert (not (= (ite (= group_size_y #x00000001) #b1 #b0) #b0))) +(assert (not (= (ite (= group_size_z #x00000001) #b1 #b0) #b0))) +(assert (not (= (ite (= num_groups_y #x00000001) #b1 #b0) #b0))) +(assert (not (= (ite (= num_groups_z #x00000001) #b1 #b0) #b0))) +(assert (not (= (ite (= group_size_x #x00000400) #b1 #b0) #b0))) +(assert (not (= (ite (= num_groups_x #x00000400) #b1 #b0) #b0))) +(define-fun $foo () Bool (=> (= (ControlFlow 0 0) 1462) (let ((GeneratedUnifiedExit_correct (=> (and %lbl%+1458 true) (and +(or %lbl%@3203 (=> (= (ControlFlow 0 1458) (- 0 3203)) (=> (not _WRITE_HAS_OCCURRED_$$p$1@2) (= _WRITE_SOURCE_$$p$1@2 #x00000000)))) +(=> (=> (not _WRITE_HAS_OCCURRED_$$p$1@2) (= _WRITE_SOURCE_$$p$1@2 #x00000000)) (and +(or %lbl%@3213 (=> (= (ControlFlow 0 1458) (- 0 3213)) (=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000)))) +(=> (=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000)) (and +(or %lbl%@3225 (=> (= (ControlFlow 0 1458) (- 0 3225)) (=> _WRITE_HAS_OCCURRED_$$p$1@2 (or +(= _WRITE_SOURCE_$$p$1@2 #x00000001) +(= _WRITE_SOURCE_$$p$1@2 #x00000002))))) +(=> (=> _WRITE_HAS_OCCURRED_$$p$1@2 (or +(= _WRITE_SOURCE_$$p$1@2 #x00000001) +(= _WRITE_SOURCE_$$p$1@2 #x00000002))) (and +(or %lbl%@3240 (=> (= (ControlFlow 0 1458) (- 0 3240)) (=> _READ_HAS_OCCURRED_$$p$1 false))) +(=> (=> _READ_HAS_OCCURRED_$$p$1 false) true))))))))))) +(let (($0$3_correct (=> (and %lbl%+1440 true) (=> (and +($mv_state $mv_state_const 1) +true +(= call465formal@_offset$2@0 (bvadd (bvadd (bvmul group_size_x group_id_x$2) local_id_x$2) #x00000001)) +(= call465formal@_value$2@0 (bvadd (bvmul group_size_x group_id_x$2) local_id_x$2))) (and +(or %lbl%@3060 (=> (= (ControlFlow 0 1440) (- 0 3060)) (not (and +true +_WRITE_HAS_OCCURRED_$$p$1@1 +(= _WRITE_OFFSET_$$p$1@1 call465formal@_offset$2@0) +(not (= _WRITE_VALUE_$$p$1@1 call465formal@_value$2@0)))))) +(=> (not (and +true +_WRITE_HAS_OCCURRED_$$p$1@1 +(= _WRITE_OFFSET_$$p$1@1 call465formal@_offset$2@0) +(not (= _WRITE_VALUE_$$p$1@1 call465formal@_value$2@0)))) (and +(or %lbl%@3078 (=> (= (ControlFlow 0 1440) (- 0 3078)) (not (and +true +_READ_HAS_OCCURRED_$$p$1 +(= _READ_OFFSET_$$p$1 call465formal@_offset$2@0) +(not (= _READ_VALUE_$$p$1 call465formal@_value$2@0)))))) +(=> (not (and +true +_READ_HAS_OCCURRED_$$p$1 +(= _READ_OFFSET_$$p$1 call465formal@_offset$2@0) +(not (= _READ_VALUE_$$p$1 call465formal@_value$2@0)))) (and +(or %lbl%@3099 (=> (= (ControlFlow 0 1440) (- 0 3099)) (=> (not _WRITE_HAS_OCCURRED_$$p$1@1) (= _WRITE_SOURCE_$$p$1@1 #x00000000)))) +(=> (=> (not _WRITE_HAS_OCCURRED_$$p$1@1) (= _WRITE_SOURCE_$$p$1@1 #x00000000)) (and +(or %lbl%@3109 (=> (= (ControlFlow 0 1440) (- 0 3109)) (=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000)))) +(=> (=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000)) (and +(or %lbl%@3121 (=> (= (ControlFlow 0 1440) (- 0 3121)) (=> _WRITE_HAS_OCCURRED_$$p$1@1 (or +(= _WRITE_SOURCE_$$p$1@1 #x00000001) +(= _WRITE_SOURCE_$$p$1@1 #x00000002))))) +(=> (=> _WRITE_HAS_OCCURRED_$$p$1@1 (or +(= _WRITE_SOURCE_$$p$1@1 #x00000001) +(= _WRITE_SOURCE_$$p$1@1 #x00000002))) (and +(or %lbl%@3136 (=> (= (ControlFlow 0 1440) (- 0 3136)) (=> _READ_HAS_OCCURRED_$$p$1 false))) +(=> (=> _READ_HAS_OCCURRED_$$p$1 false) (=> (=> (not _WRITE_HAS_OCCURRED_$$p$1@1) (= _WRITE_SOURCE_$$p$1@1 #x00000000)) (=> (and +(=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000)) +(=> _WRITE_HAS_OCCURRED_$$p$1@1 (or +(= _WRITE_SOURCE_$$p$1@1 #x00000001) +(= _WRITE_SOURCE_$$p$1@1 #x00000002)))) (=> (and +(=> _READ_HAS_OCCURRED_$$p$1 false) +(= _WRITE_HAS_OCCURRED_$$p$1@2 _WRITE_HAS_OCCURRED_$$p$1@1) +(= _WRITE_SOURCE_$$p$1@2 _WRITE_SOURCE_$$p$1@1) +(= (ControlFlow 0 1440) 1458)) GeneratedUnifiedExit_correct))))))))))))))))))) +(let ((inline$_LOG_WRITE_$$p$1$_LOG_WRITE_correct (=> (and %lbl%+1434 true) (=> (= _WRITE_HAS_OCCURRED_$$p$1@1 (ite (and +true +inline$_LOG_WRITE_$$p$1$track@1) true _WRITE_HAS_OCCURRED_$$p$1@0)) (=> (and +(= _WRITE_OFFSET_$$p$1@1 (ite (and +true +inline$_LOG_WRITE_$$p$1$track@1) inline$_LOG_WRITE_$$p$1$_offset$1@0 _WRITE_OFFSET_$$p$1@0)) +(= _WRITE_VALUE_$$p$1@1 (ite (and +true +inline$_LOG_WRITE_$$p$1$track@1) inline$_LOG_WRITE_$$p$1$_value$1@0 _WRITE_VALUE_$$p$1@0)) +(= _WRITE_SOURCE_$$p$1@1 (ite (and +true +inline$_LOG_WRITE_$$p$1$track@1) #x00000002 _WRITE_SOURCE_$$p$1@0)) +(= (ControlFlow 0 1434) 1440)) $0$3_correct))))) +(let ((inline$_LOG_WRITE_$$p$1$Entry_correct (=> (and %lbl%+1432 true) (=> (= inline$_LOG_WRITE_$$p$1$_offset$1@0 (bvadd (bvadd (bvmul group_size_x group_id_x$1) local_id_x$1) #x00000001)) (=> (and +(= inline$_LOG_WRITE_$$p$1$_value$1@0 (bvadd (bvmul group_size_x group_id_x$1) local_id_x$1)) +(= (ControlFlow 0 1432) 1434)) inline$_LOG_WRITE_$$p$1$_LOG_WRITE_correct))))) +(let ((inline$$bugle_barrier$0$anon1_Else_correct (=> (and %lbl%+1328 true) (=> (=> (and +(= group_id_x$1 group_id_x$2) +(= group_id_y$1 group_id_y$2) +(= group_id_z$1 group_id_z$2)) (=> (= #b1 #b1) (not _READ_HAS_OCCURRED_$$p$1))) (=> (and +(=> (and +(= group_id_x$1 group_id_x$2) +(= group_id_y$1 group_id_y$2) +(= group_id_z$1 group_id_z$2)) (=> (= #b1 #b1) (not _WRITE_HAS_OCCURRED_$$p$1@0))) +(= (ControlFlow 0 1328) 1432)) inline$_LOG_WRITE_$$p$1$Entry_correct))))) +(let ((inline$$bugle_barrier$0$anon1_Then_correct (=> (and %lbl%+1330 true) true))) +(let ((inline$$bugle_barrier$0$Entry_correct (=> (and %lbl%+1324 true) (and +(or %lbl%@2798 (=> (= (ControlFlow 0 1324) (- 0 2798)) (=> (and +(= group_id_x$1 group_id_x$2) +(= group_id_y$1 group_id_y$2) +(= group_id_z$1 group_id_z$2)) (= true true)))) +(=> (=> (and +(= group_id_x$1 group_id_x$2) +(= group_id_y$1 group_id_y$2) +(= group_id_z$1 group_id_z$2)) (= true true)) (and +(=> (= (ControlFlow 0 1324) 1330) inline$$bugle_barrier$0$anon1_Then_correct) +(=> (= (ControlFlow 0 1324) 1328) inline$$bugle_barrier$0$anon1_Else_correct))))))) +(let (($0$1_correct (=> (and %lbl%+1334 true) (=> (and +($mv_state $mv_state_const 0) +true +(= call397formal@_offset$2@0 (bvadd (bvmul group_size_x group_id_x$2) local_id_x$2)) +(= call397formal@_value$2@0 (bvadd (bvmul group_size_x group_id_x$2) local_id_x$2))) (and +(or %lbl%@2667 (=> (= (ControlFlow 0 1334) (- 0 2667)) (not (and +true +_WRITE_HAS_OCCURRED_$$p$1@0 +(= _WRITE_OFFSET_$$p$1@0 call397formal@_offset$2@0) +(not (= _WRITE_VALUE_$$p$1@0 call397formal@_value$2@0)))))) +(=> (not (and +true +_WRITE_HAS_OCCURRED_$$p$1@0 +(= _WRITE_OFFSET_$$p$1@0 call397formal@_offset$2@0) +(not (= _WRITE_VALUE_$$p$1@0 call397formal@_value$2@0)))) (and +(or %lbl%@2685 (=> (= (ControlFlow 0 1334) (- 0 2685)) (not (and +true +_READ_HAS_OCCURRED_$$p$1 +(= _READ_OFFSET_$$p$1 call397formal@_offset$2@0) +(not (= _READ_VALUE_$$p$1 call397formal@_value$2@0)))))) +(=> (not (and +true +_READ_HAS_OCCURRED_$$p$1 +(= _READ_OFFSET_$$p$1 call397formal@_offset$2@0) +(not (= _READ_VALUE_$$p$1 call397formal@_value$2@0)))) (and +(or %lbl%@2706 (=> (= (ControlFlow 0 1334) (- 0 2706)) (=> (not _WRITE_HAS_OCCURRED_$$p$1@0) (= _WRITE_SOURCE_$$p$1@0 #x00000000)))) +(=> (=> (not _WRITE_HAS_OCCURRED_$$p$1@0) (= _WRITE_SOURCE_$$p$1@0 #x00000000)) (and +(or %lbl%@2716 (=> (= (ControlFlow 0 1334) (- 0 2716)) (=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000)))) +(=> (=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000)) (and +(or %lbl%@2728 (=> (= (ControlFlow 0 1334) (- 0 2728)) (=> _WRITE_HAS_OCCURRED_$$p$1@0 (or +(= _WRITE_SOURCE_$$p$1@0 #x00000001) +(= _WRITE_SOURCE_$$p$1@0 #x00000002))))) +(=> (=> _WRITE_HAS_OCCURRED_$$p$1@0 (or +(= _WRITE_SOURCE_$$p$1@0 #x00000001) +(= _WRITE_SOURCE_$$p$1@0 #x00000002))) (and +(or %lbl%@2743 (=> (= (ControlFlow 0 1334) (- 0 2743)) (=> _READ_HAS_OCCURRED_$$p$1 false))) +(=> (=> _READ_HAS_OCCURRED_$$p$1 false) (=> (=> (not _WRITE_HAS_OCCURRED_$$p$1@0) (= _WRITE_SOURCE_$$p$1@0 #x00000000)) (=> (and +(=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000)) +(=> _WRITE_HAS_OCCURRED_$$p$1@0 (or +(= _WRITE_SOURCE_$$p$1@0 #x00000001) +(= _WRITE_SOURCE_$$p$1@0 #x00000002))) +(=> _READ_HAS_OCCURRED_$$p$1 false) +(= (ControlFlow 0 1334) 1324)) inline$$bugle_barrier$0$Entry_correct)))))))))))))))))) +(let ((inline$_LOG_WRITE_$$p$0$_LOG_WRITE_correct (=> (and %lbl%+1189 true) (=> (= _WRITE_HAS_OCCURRED_$$p$1@0 (ite (and +true +inline$_LOG_WRITE_$$p$0$track@1) true _WRITE_HAS_OCCURRED_$$p$1)) (=> (and +(= _WRITE_OFFSET_$$p$1@0 (ite (and +true +inline$_LOG_WRITE_$$p$0$track@1) inline$_LOG_WRITE_$$p$0$_offset$1@0 _WRITE_OFFSET_$$p$1)) +(= _WRITE_VALUE_$$p$1@0 (ite (and +true +inline$_LOG_WRITE_$$p$0$track@1) inline$_LOG_WRITE_$$p$0$_value$1@0 _WRITE_VALUE_$$p$1)) +(= _WRITE_SOURCE_$$p$1@0 (ite (and +true +inline$_LOG_WRITE_$$p$0$track@1) #x00000001 _WRITE_SOURCE_$$p$1)) +(= (ControlFlow 0 1189) 1334)) $0$1_correct))))) +(let ((inline$_LOG_WRITE_$$p$0$Entry_correct (=> (and %lbl%+1187 true) (=> (= inline$_LOG_WRITE_$$p$0$_offset$1@0 (bvadd (bvmul group_size_x group_id_x$1) local_id_x$1)) (=> (and +(= inline$_LOG_WRITE_$$p$0$_value$1@0 (bvadd (bvmul group_size_x group_id_x$1) local_id_x$1)) +(= (ControlFlow 0 1187) 1189)) inline$_LOG_WRITE_$$p$0$_LOG_WRITE_correct))))) +(let (($0_correct (=> (and %lbl%+1462 true) (=> (and +(not _READ_HAS_OCCURRED_$$p$1) +(not _WRITE_HAS_OCCURRED_$$p$1) +(= _READ_SOURCE_$$p$1 #x00000000) +(= _WRITE_SOURCE_$$p$1 #x00000000) +(bvsgt group_size_x #x00000000) +(bvsgt num_groups_x #x00000000) +(bvsge group_id_x$1 #x00000000) +(bvsge group_id_x$2 #x00000000)) (=> (and +(bvslt group_id_x$1 num_groups_x) +(bvslt group_id_x$2 num_groups_x) +(bvsge local_id_x$1 #x00000000) +(bvsge local_id_x$2 #x00000000) +(bvslt local_id_x$1 group_size_x) +(bvslt local_id_x$2 group_size_x) +(bvsgt group_size_y #x00000000) +(bvsgt num_groups_y #x00000000) +(bvsge group_id_y$1 #x00000000) +(bvsge group_id_y$2 #x00000000) +(bvslt group_id_y$1 num_groups_y) +(bvslt group_id_y$2 num_groups_y) +(bvsge local_id_y$1 #x00000000) +(bvsge local_id_y$2 #x00000000) +(bvslt local_id_y$1 group_size_y) +(bvslt local_id_y$2 group_size_y) +(bvsgt group_size_z #x00000000) +(bvsgt num_groups_z #x00000000) +(bvsge group_id_z$1 #x00000000) +(bvsge group_id_z$2 #x00000000) +(bvslt group_id_z$1 num_groups_z) +(bvslt group_id_z$2 num_groups_z) +(bvsge local_id_z$1 #x00000000) +(bvsge local_id_z$2 #x00000000) +(bvslt local_id_z$1 group_size_z) +(bvslt local_id_z$2 group_size_z) +(=> (not _WRITE_HAS_OCCURRED_$$p$1) (= _WRITE_SOURCE_$$p$1 #x00000000)) +(=> (not _READ_HAS_OCCURRED_$$p$1) (= _READ_SOURCE_$$p$1 #x00000000)) +(=> _WRITE_HAS_OCCURRED_$$p$1 (or +(= _WRITE_SOURCE_$$p$1 #x00000001) +(= _WRITE_SOURCE_$$p$1 #x00000002))) +(=> _READ_HAS_OCCURRED_$$p$1 false) +(=> (and +(= group_id_x$1 group_id_x$2) +(= group_id_y$1 group_id_y$2) +(= group_id_z$1 group_id_z$2)) (or +(not (= local_id_x$1 local_id_x$2)) +(not (= local_id_y$1 local_id_y$2)) +(not (= local_id_z$1 local_id_z$2)))) +(= (ControlFlow 0 1462) 1187)) inline$_LOG_WRITE_$$p$0$Entry_correct))))) +$0_correct))))))))))))) +(push 1) +(set-info :boogie-vc-id $foo) +(assert (not +(=> true $foo) +)) +(check-sat) +;(get-value ((ControlFlow 0 0))) +; (get-value ((ControlFlow 0 1462))) +; (get-value ((ControlFlow 0 1187))) +; (get-value ((ControlFlow 0 1189))) +; (get-value ((ControlFlow 0 1334))) +; (get-value ((ControlFlow 0 1324))) +; (get-value ((ControlFlow 0 1328))) +; (get-value ((ControlFlow 0 1432))) +; (get-value ((ControlFlow 0 1434))) +; (get-value ((ControlFlow 0 1440))) +; (get-model) +; (assert (not (= (ControlFlow 0 1440) (- 3060)))) |