diff options
Diffstat (limited to 'test/regress/regress1/fmf/german169.smt2')
| -rw-r--r-- | test/regress/regress1/fmf/german169.smt2 | 148 |
1 files changed, 74 insertions, 74 deletions
diff --git a/test/regress/regress1/fmf/german169.smt2 b/test/regress/regress1/fmf/german169.smt2 index c88de064c..c4a40ccc1 100644 --- a/test/regress/regress1/fmf/german169.smt2 +++ b/test/regress/regress1/fmf/german169.smt2 @@ -1,17 +1,17 @@ -; COMMAND-LINE: --finite-model-find --lang=smt2.5 +; COMMAND-LINE: --finite-model-find ; EXPECT: sat (set-logic ALL_SUPPORTED) (set-info :status sat) -(declare-datatypes () ((UNIT (Unit)))) -(declare-datatypes () ((BOOL (Truth) (Falsity)))) +(declare-datatypes ((UNIT 0)) (((Unit)))) +(declare-datatypes ((BOOL 0)) (((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-datatypes ((cache_state$type 0)) (((invalid) (shared) (exclusive)))) +(declare-datatypes ((cache$type 0)) (((c_cache$type (c_state cache_state$type) (c_data data$type))))) +(declare-datatypes ((msg_cmd$type 0)) (((empty) (reqs) (reqe) (inv) (invack) (gnts) (gnte)))) +(declare-datatypes ((msg$type 0)) (((c_msg$type (m_cmd msg_cmd$type) (m_data data$type))))) (declare-fun dummy () data$type) ; Var Decls -------------- @@ -28,76 +28,76 @@ (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 +(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))) + (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) + (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)) + (n node$type)) + (=> (= (m_cmd + (select + chan2 + n)) + gnte) + (= exgntd + Truth))) + Truth Falsity)) Truth)))))))) - + (check-sat) (exit) |