diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-22 16:33:15 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2013-05-22 16:33:30 -0500 |
commit | 852d41b2878ae4981ab4a9b246345bb05bbe23ab (patch) | |
tree | 8f19be94ed3432517a3dcde87c6bb6eb868203f0 /test/regress/regress0/fmf/german169.smt2 | |
parent | fd076209b073aff3ad3db6eccfc51a59ec5d87c2 (diff) |
Add regressions for finite model finding
Diffstat (limited to 'test/regress/regress0/fmf/german169.smt2')
-rwxr-xr-x | test/regress/regress0/fmf/german169.smt2 | 104 |
1 files changed, 104 insertions, 0 deletions
diff --git a/test/regress/regress0/fmf/german169.smt2 b/test/regress/regress0/fmf/german169.smt2 new file mode 100755 index 000000000..f0906d6b5 --- /dev/null +++ b/test/regress/regress0/fmf/german169.smt2 @@ -0,0 +1,104 @@ +; COMMAND-LINE: --finite-model-find +; EXPECT: sat +; EXIT: 10 +(set-logic ALL_SUPPORTED) +(set-info :status sat) +(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 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 auxnode () node$type) +(declare-fun curcmd () msg_cmd$type) + +; Asserts -------------- +(assert (not (=> (and (and (forall ((n node$type)) + (=> (= (m_cmd (select + chan2 + n)) + gnte) (= exgntd + Truth))) + (forall ((n node$type)) + (=> (= exgntd Truth) + (= (select shrset n) + (ite (= n auxnode) Truth + Falsity))))) (forall + ((n node$type)) + (=> (= + (m_cmd + (select + chan3 + n)) + invack) + (= (m_cmd + (select + chan2 + n)) + empty)))) + (=> (= (m_cmd (select chan3 recv_invack$i)) + invack) (=> (not (= curcmd empty)) + (=> (= chan3$1 (store + chan3 + recv_invack$i + (let ( + (vup_228 + (select + chan3 + recv_invack$i))) + (c_msg$type + empty + (m_data + vup_228))))) + (=> (= 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)) + (=> (= (m_cmd + (select + chan2 + n)) + gnte) + (= exgntd$1 + Truth))))) + Truth Falsity) + (ite (forall ( + (n node$type)) + (=> (= (m_cmd + (select + chan2 + n)) + gnte) + (= exgntd + Truth))) + Truth Falsity)) + Truth)))))))) + +(check-sat) +(exit) |