diff options
Diffstat (limited to 'test/regress/regress1/bug296.smt2')
-rw-r--r-- | test/regress/regress1/bug296.smt2 | 1698 |
1 files changed, 1698 insertions, 0 deletions
diff --git a/test/regress/regress1/bug296.smt2 b/test/regress/regress1/bug296.smt2 new file mode 100644 index 000000000..3aea7e9c9 --- /dev/null +++ b/test/regress/regress1/bug296.smt2 @@ -0,0 +1,1698 @@ +; COMMAND-LINE: --lang=smt2.5 +; EXPECT: unsat +(set-logic QF_ALL) +(set-info :status unsat) +(declare-datatypes + () ( + (MsgResult (MsgResult_MsgOK (destMsgResult_MsgOK Real)) + (MsgResult_MsgAudit (destMsgResult_MsgAudit Real))) + (MsgTree (MsgTree_Leaf) + (MsgTree_Node (destMsgTree_Node MsgTree_Node_recd))) + (TreeResult (TreeResult_TreeOK (destTreeResult_TreeOK MsgTree)) + (TreeResult_TreeAudit (destTreeResult_TreeAudit Real))) + (MsgTree_Node_recd + (MsgTree_Node_recd (MsgTree_Node_recd_Value Real) + (MsgTree_Node_recd_Left MsgTree) + (MsgTree_Node_recd_Right MsgTree))))) +(declare-fun Guardfn (MsgTree) TreeResult) +(declare-fun Input () MsgTree) +(declare-fun M () Real) +(declare-fun f (Real) MsgResult) +(declare-fun n () MsgTree_Node_recd) +(declare-fun ARB () Bool) +(declare-fun Guard_Checkfn (MsgTree) Bool) +(define-fun DWS_Idempotentfn ((M1 Real)) Bool + (ite (is-MsgResult_MsgOK (f M1)) + (and (is-MsgResult_MsgOK (f (destMsgResult_MsgOK (f M1)))) + (= (destMsgResult_MsgOK (f M1)) + (destMsgResult_MsgOK (f (destMsgResult_MsgOK (f M1)))))) + (or (is-MsgResult_MsgAudit (f M1)) ARB))) +(assert + (and + (=> + (and (not (is-MsgTree_Leaf Input)) + (and (is-MsgTree_Node Input) + (and + (not + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value (destMsgTree_Node Input))))) + (and + (is-MsgResult_MsgOK + (f + (MsgTree_Node_recd_Value (destMsgTree_Node Input)))) + (and + (not + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))))) + (and + (is-TreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (is-TreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))))))) + (Guard_Checkfn + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right (destMsgTree_Node Input)))))) + (and + (=> + (and (not (is-MsgTree_Leaf Input)) + (and (is-MsgTree_Node Input) + (and + (not + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (and + (is-MsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (is-TreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input)))))))) + (Guard_Checkfn + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input)))))) + (and + (DWS_Idempotentfn + (MsgTree_Node_recd_Value (destMsgTree_Node Input))) + (and + (is-TreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))))))))) + (not + (Guard_Checkfn + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))))))) +(assert + (= + (Guard_Checkfn + (destTreeResult_TreeOK + (Guardfn (MsgTree_Node_recd_Right (destMsgTree_Node Input))))) + (ite + (is-MsgTree_Leaf + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right (destMsgTree_Node Input))))) + true + (and + (is-MsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))))) + (and + (= + (MsgTree_Node_recd_Value + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))) + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))) + (and + (Guard_Checkfn + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))) + (Guard_Checkfn + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))) +(assert + (= + (Guard_Checkfn + (destTreeResult_TreeOK + (Guardfn (MsgTree_Node_recd_Left (destMsgTree_Node Input))))) + (ite + (is-MsgTree_Leaf + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input))))) + true + (and + (is-MsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input)))))))) + (and + (= + (MsgTree_Node_recd_Value + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input)))))) + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))))))))) + (and + (Guard_Checkfn + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))))))) + (Guard_Checkfn + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))))))))))))) +(assert + (= + (Guard_Checkfn + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f (MsgTree_Node_recd_Value (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))) + (ite + (is-MsgTree_Leaf + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))) + true + (and + (is-MsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))))))))))))) + (and + (= + (MsgTree_Node_recd_Value + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))))))))))) + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))))) + (and + (Guard_Checkfn + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))) + (Guard_Checkfn + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))))))))) +(assert + (= + (Guard_Checkfn + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right (destMsgTree_Node Input))))))) + (ite + (is-MsgTree_Leaf + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right (destMsgTree_Node Input))))))) + true + (and + (is-MsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))))))) + (and + (= + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))))) + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))) + (and + (Guard_Checkfn + (MsgTree_Node_recd_Left + (destMsgTree_Node + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))) + (Guard_Checkfn + (MsgTree_Node_recd_Right + (destMsgTree_Node + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))) +(assert + (= + (Guard_Checkfn + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right (destMsgTree_Node Input))))))) + (ite + (is-MsgTree_Leaf + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right (destMsgTree_Node Input))))))) + true + (and + (is-MsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))))))) + (and + (= + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))))) + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))) + (and + (Guard_Checkfn + (MsgTree_Node_recd_Left + (destMsgTree_Node + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))) + (Guard_Checkfn + (MsgTree_Node_recd_Right + (destMsgTree_Node + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))) +(assert + (= + (Guard_Checkfn + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input))))))) + (ite + (is-MsgTree_Leaf + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input))))))) + true + (and + (is-MsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))))))))) + (and + (= + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))))))) + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))))))))))) + (and + (Guard_Checkfn + (MsgTree_Node_recd_Left + (destMsgTree_Node + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))))))))) + (Guard_Checkfn + (MsgTree_Node_recd_Right + (destMsgTree_Node + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))))))))))))))) +(assert + (= + (Guard_Checkfn + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input))))))) + (ite + (is-MsgTree_Leaf + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input))))))) + true + (and + (is-MsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))))))))) + (and + (= + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))))))) + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))))))))))) + (and + (Guard_Checkfn + (MsgTree_Node_recd_Left + (destMsgTree_Node + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))))))))) + (Guard_Checkfn + (MsgTree_Node_recd_Right + (destMsgTree_Node + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))))))))))))))) +(assert + (= + (Guard_Checkfn + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))) + (ite + (is-MsgTree_Leaf + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))) + true + (and + (is-MsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))))))))))))))) + (and + (= + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))))))))))))) + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))))))) + (and + (Guard_Checkfn + (MsgTree_Node_recd_Left + (destMsgTree_Node + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))))) + (Guard_Checkfn + (MsgTree_Node_recd_Right + (destMsgTree_Node + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))))))))))) +(assert + (= + (Guard_Checkfn + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))) + (ite + (is-MsgTree_Leaf + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))) + true + (and + (is-MsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))))))))))))))) + (and + (= + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))))))))))))) + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))))))) + (and + (Guard_Checkfn + (MsgTree_Node_recd_Left + (destMsgTree_Node + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))))) + (Guard_Checkfn + (MsgTree_Node_recd_Right + (destMsgTree_Node + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))))))))))))))))))))))) +(assert + (not + (not + (is-MsgTree_Leaf + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right (destMsgTree_Node Input)))))))))) +(assert + (not + (not + (is-MsgTree_Leaf + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right (destMsgTree_Node Input)))))))))) +(assert + (not + (not + (is-MsgTree_Leaf + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input)))))))))) +(assert + (not + (not + (is-MsgTree_Leaf + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left (destMsgTree_Node Input)))))))))) +(assert + (not + (not + (is-MsgTree_Leaf + (MsgTree_Node_recd_Left + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))))))))))))))) +(assert + (not + (not + (is-MsgTree_Leaf + (MsgTree_Node_recd_Right + (destMsgTree_Node + (destTreeResult_TreeOK + (ite (is-MsgTree_Leaf Input) + (TreeResult_TreeOK MsgTree_Leaf) + (ite + (is-MsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (TreeResult_TreeAudit + (destMsgResult_MsgAudit + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input))))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input))) + (ite + (is-TreeResult_TreeAudit + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))) + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input))) + (TreeResult_TreeOK + (MsgTree_Node + (MsgTree_Node_recd + (destMsgResult_MsgOK + (f + (MsgTree_Node_recd_Value + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Left + (destMsgTree_Node Input)))) + (destTreeResult_TreeOK + (Guardfn + (MsgTree_Node_recd_Right + (destMsgTree_Node Input)))))))))))))))))) +(check-sat) +(exit) |