From 8116fa6b55db64301ed89f1f174b95780449007f Mon Sep 17 00:00:00 2001 From: Morgan Deters Date: Sat, 6 Oct 2012 05:27:33 +0000 Subject: [PATCH] * Include a few bug testcases for resolved bugs. * Fix error message if you POP beyond the bottom user stack frame. (this commit was certified error- and warning-free by the test-and-commit script.) --- src/smt/smt_engine.cpp | 5 +- src/util/configuration.cpp | 4 +- src/util/configuration.h | 4 +- test/regress/regress0/Makefile.am | 2 + test/regress/regress0/bug274.cvc | 65 ++ test/regress/regress0/bug296.smt2 | 1696 +++++++++++++++++++++++++++++ 6 files changed, 1770 insertions(+), 6 deletions(-) create mode 100644 test/regress/regress0/bug274.cvc create mode 100644 test/regress/regress0/bug296.smt2 diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp index 0a5270d83..d63a63ba2 100644 --- a/src/smt/smt_engine.cpp +++ b/src/smt/smt_engine.cpp @@ -2447,7 +2447,7 @@ void SmtEngine::pop() throw(ModalException) { if(!options::incrementalSolving()) { throw ModalException("Cannot pop when not solving incrementally (use --incremental)"); } - if(d_userContext->getLevel() == 0) { + if(d_userLevels.size() == 0) { throw ModalException("Cannot pop beyond the first user frame"); } @@ -2457,7 +2457,8 @@ void SmtEngine::pop() throw(ModalException) { d_needPostsolve = false; } - AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel()); + AlwaysAssert(d_userContext->getLevel() > 0); + AlwaysAssert(d_userLevels.back() < d_userContext->getLevel()); while (d_userLevels.back() < d_userContext->getLevel()) { internalPop(true); } diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp index 6fe2e2af0..7b7559ce6 100644 --- a/src/util/configuration.cpp +++ b/src/util/configuration.cpp @@ -3,9 +3,9 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): acsys, cconway + ** Minor contributors (to current version): lianah, acsys, cconway, dejan, bobot ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/src/util/configuration.h b/src/util/configuration.h index b1ef7154d..c43c7c0df 100644 --- a/src/util/configuration.h +++ b/src/util/configuration.h @@ -3,9 +3,9 @@ ** \verbatim ** Original author: mdeters ** Major contributors: none - ** Minor contributors (to current version): acsys + ** Minor contributors (to current version): acsys, lianah, bobot ** This file is part of the CVC4 prototype. - ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys) ** Courant Institute of Mathematical Sciences ** New York University ** See the file COPYING in the top-level source directory for licensing diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index ed12c447e..8b2f05ca7 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -117,9 +117,11 @@ BUG_TESTS = \ bug216.smt2 \ bug220.smt2 \ bug239.smt \ + bug274.cvc \ bug288.smt \ bug288b.smt \ bug288c.smt \ + bug296.smt2 \ buggy-ite.smt2 \ bug303.smt2 \ bug310.cvc \ diff --git a/test/regress/regress0/bug274.cvc b/test/regress/regress0/bug274.cvc new file mode 100644 index 000000000..7b3df50d8 --- /dev/null +++ b/test/regress/regress0/bug274.cvc @@ -0,0 +1,65 @@ +% EXPECT: unsat +% EXIT: 20 +DATATYPE DT1 = + DT1_a | + DT1_b | + DT1_c | + DT1_d | + DT1_e | + DT1_f | + DT1_g | + DT1_h | + DT1_i | + DT1_j | + DT1_k | + DT1_l | + DT1_m | + DT1_n | + DT1_o | + DT1_p | + DT1_q | + DT1_r | + DT1_s | + DT1_t | + DT1_u | + DT1_v | + DT1_w | + DT1_x | + DT1_y | + DT1_z +END; +DATATYPE DT2 = + DT2_a | + DT2_b | + DT2_c | + DT2_d +END; +DATATYPE DT3 = + DT3_a | + DT3_b +END; +var1 : DT3; +var2 : DT3; +var3 : DT1; +var4 : DT3; +var5 : DT3; +var6 : DT3; +var7 : DT3; +var8 : DT3; +var9 : DT3; +var10 : DT3; +var11 : DT2; +var12 : DT3; +var13 : DT3; +var14 : DT3; +var16 : DT3; +var17 : DT3; +var18 : DT3; +var20 : DT3; +var21 : DT3; +CHECKSAT +( + (((NOT(var13 = DT3_a)) AND (NOT(var10 = DT3_b))) AND (NOT((((((var7 = DT3_b) AND (var4 = DT3_b)) AND (var1 = DT3_a)) OR ((((var5 = DT3_a) AND (var17 = DT3_b)) OR ((var21 = DT3_b) AND ((var3 = DT1_f) OR (var3 = DT1_g)))) <=> (DT3_b = DT3_b))) OR (((var14 = DT3_a) AND (var2 = DT3_a)) AND (((((var8 = DT3_a) AND (var18 = DT3_b)) OR ((var6 = DT3_a) AND (var11 /= DT2_a))) OR (var20 = DT3_b)) OR (var9 = DT3_b)))) OR ((NOT(((((var7 = DT3_b) AND (var4 = DT3_b)) AND (var1 = DT3_a)) OR ((((var5 = DT3_a) AND (var17 = DT3_b)) OR ((var21 = DT3_b) AND ((var3 = DT1_f) OR (var3 = DT1_g)))) <=> (DT3_b = DT3_b))) OR (((var14 = DT3_a) AND (var2 = DT3_a)) AND (((((var8 = DT3_a) AND (var18 = DT3_b)) OR ((var6 = DT3_a) AND (var11 /= DT2_a))) OR (var20 = DT3_b)) OR (var9 = DT3_b))))) AND ((var14 = DT3_b) AND (TRUE)))))) + AND + (NOT((var12 = DT3_a) OR ((var12 = DT3_b) AND ((var16 = DT3_b) OR (TRUE))))) +); diff --git a/test/regress/regress0/bug296.smt2 b/test/regress/regress0/bug296.smt2 new file mode 100644 index 000000000..f3600942a --- /dev/null +++ b/test/regress/regress0/bug296.smt2 @@ -0,0 +1,1696 @@ +(set-logic QF_ALL_SUPPORTED) +(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) -- 2.30.2