diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-22 17:41:11 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-22 17:41:11 -0500 |
commit | fee510eacd6ea9d35906218ce3d4b88f7d86f8b1 (patch) | |
tree | 0b7e96a0afbb56791c8ac4d2a834e391df1b6fd2 /test/regress/regress0/fmf/german73.smt2 | |
parent | 2bf0735176e0ff5fb9720bfb255ca22443584dcc (diff) | |
parent | 852d41b2878ae4981ab4a9b246345bb05bbe23ab (diff) |
Merge branch 'master' of https://github.com/CVC4/CVC4
Conflicts:
src/theory/arith/theory_arith_private.cpp
src/theory/quantifiers_engine.cpp
Diffstat (limited to 'test/regress/regress0/fmf/german73.smt2')
-rwxr-xr-x | test/regress/regress0/fmf/german73.smt2 | 106 |
1 files changed, 106 insertions, 0 deletions
diff --git a/test/regress/regress0/fmf/german73.smt2 b/test/regress/regress0/fmf/german73.smt2 new file mode 100755 index 000000000..388a53624 --- /dev/null +++ b/test/regress/regress0/fmf/german73.smt2 @@ -0,0 +1,106 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: unsat +; EXIT: 20 +(set-logic ALL_SUPPORTED) +(set-info :status unsat) +(declare-datatypes () ((UNIT (Unit)))) +(declare-datatypes () ((BOOL (Truth) (Falsity)))) + +; Decls -------------- +(declare-sort node$type 0) +(declare-sort data$type 0) +(declare-datatypes () ((cache_state$type (invalid) (shared) (exclusive)))) +(declare-datatypes () ((cache$type (c_cache$type (c_state cache_state$type) (c_data data$type))))) +(declare-datatypes () ((msg_cmd$type (empty) (reqs) (reqe) (inv) (invack) (gnts) (gnte)))) +(declare-datatypes () ((msg$type (c_msg$type (m_cmd msg_cmd$type) (m_data data$type))))) +(declare-fun dummy () data$type) + +; Var Decls -------------- +(declare-fun memdata$1 () data$type) +(declare-fun shrset$1 () (Array node$type BOOL)) +(declare-fun recv_invack$i () node$type) +(declare-fun exgntd () BOOL) +(declare-fun invset () (Array node$type BOOL)) +(declare-fun chan3$1 () (Array node$type msg$type)) +(declare-fun shrset () (Array node$type BOOL)) +(declare-fun exgntd$1 () BOOL) +(declare-fun chan2 () (Array node$type msg$type)) +(declare-fun chan3 () (Array node$type msg$type)) +(declare-fun curcmd () msg_cmd$type) + +; Asserts -------------- +(assert (not (=> (and (forall ((n node$type)) + (=> (= (select invset n) + Truth) (= (select + shrset + n) Truth))) + (forall ((n node$type)) (=> + (or + (= + (m_cmd + (select + chan2 + n)) + inv) + (= + (m_cmd + (select + chan3 + n)) + invack)) + (not + (= + (select + invset + n) + Truth))))) + (=> (= (m_cmd (select chan3 recv_invack$i)) + invack) (=> (not (= curcmd empty)) + (=> (= chan3$1 (store + chan3 + recv_invack$i + (let ( + (vup_101 + (select + chan3 + recv_invack$i))) + (c_msg$type + empty + (m_data + vup_101))))) + (=> (= shrset$1 (store + shrset + recv_invack$i + Falsity)) + (= (ite (= exgntd Truth) + (ite (=> (= exgntd$1 + Falsity) + (=> (= memdata$1 + (m_data + (select + chan3$1 + recv_invack$i))) + (forall ( + (n node$type)) + (=> (= (select + invset + n) + Truth) + (= (select + shrset$1 + n) Truth))))) + Truth Falsity) + (ite (forall ( + (n node$type)) + (=> (= (select + invset + n) + Truth) + (= (select + shrset$1 + n) Truth))) + Truth Falsity)) + Truth)))))))) + +(check-sat) +(exit) |