diff options
Diffstat (limited to 'test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2')
-rw-r--r-- | test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 | 21 |
1 files changed, 21 insertions, 0 deletions
diff --git a/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 b/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 new file mode 100644 index 000000000..2a46d2a21 --- /dev/null +++ b/test/regress/regress1/quantifiers/nested9_true-unreach-call.i_575.smt2 @@ -0,0 +1,21 @@ +; COMMAND-LINE: --cbqi-bv +; EXPECT: unsat +(set-logic BV) +(set-info :status unsat) +(declare-fun c_main_~i~6 () (_ BitVec 32)) +(declare-fun c_main_~j~6 () (_ BitVec 32)) +(declare-fun c_main_~k~6 () (_ BitVec 32)) +(assert + (and (bvsle c_main_~i~6 (_ bv3 32)) (bvsle c_main_~i~6 (_ bv2 32)) + (exists ((v_nnf_34 (_ BitVec 32))) + (and (bvsle (bvadd v_nnf_34 (_ bv3 32)) c_main_~k~6) + (bvsle v_nnf_34 (_ bv3 32)) (bvsle c_main_~j~6 (bvadd (bvmul (_ bv2 32) v_nnf_34) (_ bv1 32))))))) +(assert + (not + (and (bvsle c_main_~i~6 (_ bv3 32)) (bvsle c_main_~i~6 (_ bv2 32)) + (exists ((v_nnf_30 (_ BitVec 32))) + (and (bvsle (bvadd v_nnf_30 (_ bv1 32)) c_main_~k~6) + (bvsle v_nnf_30 (_ bv3 32)) (bvsle c_main_~j~6 (bvadd (bvmul (_ bv2 32) v_nnf_30) (_ bv1 32)))))))) +(check-sat) +(exit) + |