diff options
| author | Morgan Deters <mdeters@gmail.com> | 2012-10-06 05:27:33 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2012-10-06 05:27:33 +0000 |
| commit | 8116fa6b55db64301ed89f1f174b95780449007f (patch) | |
| tree | f75566f83d9bbefd9fd5cb2b34feab7d7a3faa84 /test | |
| parent | 9b871cceb0f9c3372504f9f7b786a7c1dd7cd700 (diff) | |
* 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.)
Diffstat (limited to 'test')
| -rw-r--r-- | test/regress/regress0/Makefile.am | 2 | ||||
| -rw-r--r-- | test/regress/regress0/bug274.cvc | 65 | ||||
| -rw-r--r-- | test/regress/regress0/bug296.smt2 | 1696 |
3 files changed, 1763 insertions, 0 deletions
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) |