* 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.)

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0a5270d83ad6f3e3be41ed5c285ab7c1294f4cb4..d63a63ba20cf59c1637eae53af29e0de45ce6759 100644 (file)
--- 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 6fe2e2af009bda22bcebee138622ae7c8b872779..7b7559ce64f456e417ea7c90c7146ef6178b0abb 100644 (file)
--- 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 b1ef7154d92270c5be2fe65ef2fce975f0d7eada..c43c7c0df24a94d3ebc60622a832b17c6770c5f4 100644 (file)
--- 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 ed12c447eccca72eb1bf59d2edce6db9845d8edd..8b2f05ca7512cf0ba90d461935b2d92ab44eaadd 100644 (file)
--- 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 (file)
index 0000000..7b3df50
--- /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 (file)
index 0000000..f360094
--- /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)