diff options
Diffstat (limited to 'test/regress/regress1/bug512.smt2')
-rw-r--r-- | test/regress/regress1/bug512.smt2 | 146 |
1 files changed, 146 insertions, 0 deletions
diff --git a/test/regress/regress1/bug512.smt2 b/test/regress/regress1/bug512.smt2 new file mode 100644 index 000000000..1c8a0626a --- /dev/null +++ b/test/regress/regress1/bug512.smt2 @@ -0,0 +1,146 @@ +; COMMAND-LINE: --tlimit-per 2500 -iq +; EXPECT: unknown +; EXPECT: (:reason-unknown incomplete) +; EXPECT: unsat +(set-option :print-success false) +(set-info :smt-lib-version 2.0) +;(set-option :AUTO_CONFIG false) +;(set-option :MODEL_HIDE_UNUSED_PARTITIONS false) +;(set-option :MODEL_V2 true) +;(set-option :ASYNC_COMMANDS false) +;(set-option :PHASE_SELECTION 0) +;(set-option :RESTART_STRATEGY 0) +;(set-option :RESTART_FACTOR |1.5|) +;(set-option :ARITH_RANDOM_INITIAL_VALUE true) +;(set-option :CASE_SPLIT 3) +;(set-option :DELAY_UNITS true) +;(set-option :DELAY_UNITS_THRESHOLD 16) +;(set-option :NNF_SK_HACK true) +;(set-option :MBQI false) +;(set-option :QI_EAGER_THRESHOLD 100) +;(set-option :QI_COST |"(+ weight generation)"|) +;(set-option :TYPE_CHECK true) +;(set-option :BV_REFLECT true) +; 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 tickleBool (Bool) Bool) +(assert (and (tickleBool true) (tickleBool false))) +(declare-fun Ctor (T@T) Int) +(declare-fun intType () T@T) +(declare-fun realType () T@T) +(declare-fun boolType () T@T) +(declare-fun int_2_U (Int) T@U) +(declare-fun U_2_int (T@U) Int) +(declare-fun type (T@U) T@T) +(declare-fun real_2_U (Real) T@U) +(declare-fun U_2_real (T@U) Real) +(declare-fun bool_2_U (Bool) T@U) +(declare-fun U_2_bool (T@U) Bool) +(declare-fun %lbl%+67 () Bool) +(declare-fun i@0 () Int) +(declare-fun x@@5 () Int) +(declare-fun y@@1 () Int) +(declare-fun i@1 () Int) +(declare-fun %lbl%@186 () Bool) +(declare-fun %lbl%+69 () Bool) +(declare-fun %lbl%@157 () Bool) +(declare-fun %lbl%+65 () Bool) +(declare-fun %lbl%+63 () Bool) +(declare-fun %lbl%@125 () Bool) +(declare-fun %lbl%+97 () Bool) +(assert (and +(= (Ctor intType) 0) +(= (Ctor realType) 1) +(= (Ctor boolType) 2) +(forall ((arg0 Int) ) (! (= (U_2_int (int_2_U arg0)) arg0) + :qid |typeInv:U_2_int| + :pattern ( (int_2_U arg0)) +)) +(forall ((x T@U) ) (! (=> (= (type x) intType) (= (int_2_U (U_2_int x)) x)) + :qid |cast:U_2_int| + :pattern ( (U_2_int x)) +)) +(forall ((arg0@@0 Int) ) (! (= (type (int_2_U arg0@@0)) intType) + :qid |funType:int_2_U| + :pattern ( (int_2_U arg0@@0)) +)) +(forall ((arg0@@1 Real) ) (! (= (U_2_real (real_2_U arg0@@1)) arg0@@1) + :qid |typeInv:U_2_real| + :pattern ( (real_2_U arg0@@1)) +)) +(forall ((x@@0 T@U) ) (! (=> (= (type x@@0) realType) (= (real_2_U (U_2_real x@@0)) x@@0)) + :qid |cast:U_2_real| + :pattern ( (U_2_real x@@0)) +)) +(forall ((arg0@@2 Real) ) (! (= (type (real_2_U arg0@@2)) realType) + :qid |funType:real_2_U| + :pattern ( (real_2_U arg0@@2)) +)) +(forall ((arg0@@3 Bool) ) (! (= (U_2_bool (bool_2_U arg0@@3)) arg0@@3) + :qid |typeInv:U_2_bool| + :pattern ( (bool_2_U arg0@@3)) +)) +(forall ((x@@1 T@U) ) (! (=> (= (type x@@1) boolType) (= (bool_2_U (U_2_bool x@@1)) x@@1)) + :qid |cast:U_2_bool| + :pattern ( (U_2_bool x@@1)) +)) +(forall ((arg0@@4 Bool) ) (! (= (type (bool_2_U arg0@@4)) boolType) + :qid |funType:bool_2_U| + :pattern ( (bool_2_U arg0@@4)) +)))) +(assert (forall ((x@@2 T@U) ) (! (UOrdering2 x@@2 x@@2) + :qid |bg:subtype-refl| + :no-pattern (U_2_int x@@2) + :no-pattern (U_2_bool x@@2) +))) +(assert (forall ((x@@3 T@U) (y T@U) (z T@U) ) (! (let ((alpha (type x@@3))) +(=> (and +(= (type y) alpha) +(= (type z) alpha) +(UOrdering2 x@@3 y) +(UOrdering2 y z)) (UOrdering2 x@@3 z))) + :qid |bg:subtype-trans| + :pattern ( (UOrdering2 x@@3 y) (UOrdering2 y z)) +))) +(assert (forall ((x@@4 T@U) (y@@0 T@U) ) (! (let ((alpha@@0 (type x@@4))) +(=> (= (type y@@0) alpha@@0) (=> (and +(UOrdering2 x@@4 y@@0) +(UOrdering2 y@@0 x@@4)) (= x@@4 y@@0)))) + :qid |bg:subtype-antisymm| + :pattern ( (UOrdering2 x@@4 y@@0) (UOrdering2 y@@0 x@@4)) +))) +(push 1) +(set-info :boogie-vc-id foo) +(assert (not +(let ((anon3_LoopBody_correct (=> (! (and %lbl%+67 true) :lblpos +67) (=> (and +(< i@0 (+ x@@5 y@@1)) +(= i@1 (+ i@0 1))) (and +(! (or %lbl%@186 (<= i@1 (+ x@@5 y@@1))) :lblneg @186) +(=> (<= i@1 (+ x@@5 y@@1)) true)))))) +(let ((anon3_LoopDone_correct (=> (! (and %lbl%+69 true) :lblpos +69) (=> (<= (+ x@@5 y@@1) i@0) (and +(! (or %lbl%@157 (= i@0 (- x@@5 y@@1))) :lblneg @157) +(=> (= i@0 (- x@@5 y@@1)) true)))))) +(let ((anon3_LoopHead_correct (=> (! (and %lbl%+65 true) :lblpos +65) (=> (<= i@0 (+ x@@5 y@@1)) (and +anon3_LoopDone_correct +anon3_LoopBody_correct))))) +(let ((anon0_correct (=> (! (and %lbl%+63 true) :lblpos +63) (and +(! (or %lbl%@125 (<= x@@5 (+ x@@5 y@@1))) :lblneg @125) +(=> (<= x@@5 (+ x@@5 y@@1)) anon3_LoopHead_correct))))) +(let ((PreconditionGeneratedEntry_correct (=> (! (and %lbl%+97 true) :lblpos +97) (=> (>= y@@1 0) anon0_correct)))) +PreconditionGeneratedEntry_correct))))) +)) +(check-sat) +(get-info :reason-unknown) +;(labels) +(assert %lbl%@157) +(check-sat) +(pop 1) |