summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-10-06 05:27:33 +0000
committerMorgan Deters <mdeters@gmail.com>2012-10-06 05:27:33 +0000
commit8116fa6b55db64301ed89f1f174b95780449007f (patch)
treef75566f83d9bbefd9fd5cb2b34feab7d7a3faa84
parent9b871cceb0f9c3372504f9f7b786a7c1dd7cd700 (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
-rw-r--r--src/smt/smt_engine.cpp5
-rw-r--r--src/util/configuration.cpp4
-rw-r--r--src/util/configuration.h4
-rw-r--r--test/regress/regress0/Makefile.am2
-rw-r--r--test/regress/regress0/bug274.cvc65
-rw-r--r--test/regress/regress0/bug296.smt21696
6 files changed, 1770 insertions, 6 deletions
diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 0a5270d83..d63a63ba2 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -2447,7 +2447,7 @@ void SmtEngine::pop() throw(ModalException) {
if(!options::incrementalSolving()) {
throw ModalException("Cannot pop when not solving incrementally (use --incremental)");
}
- if(d_userContext->getLevel() == 0) {
+ if(d_userLevels.size() == 0) {
throw ModalException("Cannot pop beyond the first user frame");
}
@@ -2457,7 +2457,8 @@ void SmtEngine::pop() throw(ModalException) {
d_needPostsolve = false;
}
- AlwaysAssert(d_userLevels.size() > 0 && d_userLevels.back() < d_userContext->getLevel());
+ AlwaysAssert(d_userContext->getLevel() > 0);
+ AlwaysAssert(d_userLevels.back() < d_userContext->getLevel());
while (d_userLevels.back() < d_userContext->getLevel()) {
internalPop(true);
}
diff --git a/src/util/configuration.cpp b/src/util/configuration.cpp
index 6fe2e2af0..7b7559ce6 100644
--- a/src/util/configuration.cpp
+++ b/src/util/configuration.cpp
@@ -3,9 +3,9 @@
** \verbatim
** Original author: mdeters
** Major contributors: none
- ** Minor contributors (to current version): acsys, cconway
+ ** Minor contributors (to current version): lianah, acsys, cconway, dejan, bobot
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
diff --git a/src/util/configuration.h b/src/util/configuration.h
index b1ef7154d..c43c7c0df 100644
--- a/src/util/configuration.h
+++ b/src/util/configuration.h
@@ -3,9 +3,9 @@
** \verbatim
** Original author: mdeters
** Major contributors: none
- ** Minor contributors (to current version): acsys
+ ** Minor contributors (to current version): acsys, lianah, bobot
** This file is part of the CVC4 prototype.
- ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys)
+ ** Copyright (c) 2009-2012 The Analysis of Computer Systems Group (ACSys)
** Courant Institute of Mathematical Sciences
** New York University
** See the file COPYING in the top-level source directory for licensing
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index ed12c447e..8b2f05ca7 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -117,9 +117,11 @@ BUG_TESTS = \
bug216.smt2 \
bug220.smt2 \
bug239.smt \
+ bug274.cvc \
bug288.smt \
bug288b.smt \
bug288c.smt \
+ bug296.smt2 \
buggy-ite.smt2 \
bug303.smt2 \
bug310.cvc \
diff --git a/test/regress/regress0/bug274.cvc b/test/regress/regress0/bug274.cvc
new file mode 100644
index 000000000..7b3df50d8
--- /dev/null
+++ b/test/regress/regress0/bug274.cvc
@@ -0,0 +1,65 @@
+% EXPECT: unsat
+% EXIT: 20
+DATATYPE DT1 =
+ DT1_a |
+ DT1_b |
+ DT1_c |
+ DT1_d |
+ DT1_e |
+ DT1_f |
+ DT1_g |
+ DT1_h |
+ DT1_i |
+ DT1_j |
+ DT1_k |
+ DT1_l |
+ DT1_m |
+ DT1_n |
+ DT1_o |
+ DT1_p |
+ DT1_q |
+ DT1_r |
+ DT1_s |
+ DT1_t |
+ DT1_u |
+ DT1_v |
+ DT1_w |
+ DT1_x |
+ DT1_y |
+ DT1_z
+END;
+DATATYPE DT2 =
+ DT2_a |
+ DT2_b |
+ DT2_c |
+ DT2_d
+END;
+DATATYPE DT3 =
+ DT3_a |
+ DT3_b
+END;
+var1 : DT3;
+var2 : DT3;
+var3 : DT1;
+var4 : DT3;
+var5 : DT3;
+var6 : DT3;
+var7 : DT3;
+var8 : DT3;
+var9 : DT3;
+var10 : DT3;
+var11 : DT2;
+var12 : DT3;
+var13 : DT3;
+var14 : DT3;
+var16 : DT3;
+var17 : DT3;
+var18 : DT3;
+var20 : DT3;
+var21 : DT3;
+CHECKSAT
+(
+ (((NOT(var13 = DT3_a)) AND (NOT(var10 = DT3_b))) AND (NOT((((((var7 = DT3_b) AND (var4 = DT3_b)) AND (var1 = DT3_a)) OR ((((var5 = DT3_a) AND (var17 = DT3_b)) OR ((var21 = DT3_b) AND ((var3 = DT1_f) OR (var3 = DT1_g)))) <=> (DT3_b = DT3_b))) OR (((var14 = DT3_a) AND (var2 = DT3_a)) AND (((((var8 = DT3_a) AND (var18 = DT3_b)) OR ((var6 = DT3_a) AND (var11 /= DT2_a))) OR (var20 = DT3_b)) OR (var9 = DT3_b)))) OR ((NOT(((((var7 = DT3_b) AND (var4 = DT3_b)) AND (var1 = DT3_a)) OR ((((var5 = DT3_a) AND (var17 = DT3_b)) OR ((var21 = DT3_b) AND ((var3 = DT1_f) OR (var3 = DT1_g)))) <=> (DT3_b = DT3_b))) OR (((var14 = DT3_a) AND (var2 = DT3_a)) AND (((((var8 = DT3_a) AND (var18 = DT3_b)) OR ((var6 = DT3_a) AND (var11 /= DT2_a))) OR (var20 = DT3_b)) OR (var9 = DT3_b))))) AND ((var14 = DT3_b) AND (TRUE))))))
+ AND
+ (NOT((var12 = DT3_a) OR ((var12 = DT3_b) AND ((var16 = DT3_b) OR (TRUE)))))
+);
diff --git a/test/regress/regress0/bug296.smt2 b/test/regress/regress0/bug296.smt2
new file mode 100644
index 000000000..f3600942a
--- /dev/null
+++ b/test/regress/regress0/bug296.smt2
@@ -0,0 +1,1696 @@
+(set-logic QF_ALL_SUPPORTED)
+(set-info :status unsat)
+(declare-datatypes
+ () (
+ (MsgResult (MsgResult_MsgOK (destMsgResult_MsgOK Real))
+ (MsgResult_MsgAudit (destMsgResult_MsgAudit Real)))
+ (MsgTree (MsgTree_Leaf)
+ (MsgTree_Node (destMsgTree_Node MsgTree_Node_recd)))
+ (TreeResult (TreeResult_TreeOK (destTreeResult_TreeOK MsgTree))
+ (TreeResult_TreeAudit (destTreeResult_TreeAudit Real)))
+ (MsgTree_Node_recd
+ (MsgTree_Node_recd (MsgTree_Node_recd_Value Real)
+ (MsgTree_Node_recd_Left MsgTree)
+ (MsgTree_Node_recd_Right MsgTree)))))
+(declare-fun Guardfn (MsgTree) TreeResult)
+(declare-fun Input () MsgTree)
+(declare-fun M () Real)
+(declare-fun f (Real) MsgResult)
+(declare-fun n () MsgTree_Node_recd)
+(declare-fun ARB () Bool)
+(declare-fun Guard_Checkfn (MsgTree) Bool)
+(define-fun DWS_Idempotentfn ((M1 Real)) Bool
+ (ite (is-MsgResult_MsgOK (f M1))
+ (and (is-MsgResult_MsgOK (f (destMsgResult_MsgOK (f M1))))
+ (= (destMsgResult_MsgOK (f M1))
+ (destMsgResult_MsgOK (f (destMsgResult_MsgOK (f M1))))))
+ (or (is-MsgResult_MsgAudit (f M1)) ARB)))
+(assert
+ (and
+ (=>
+ (and (not (is-MsgTree_Leaf Input))
+ (and (is-MsgTree_Node Input)
+ (and
+ (not
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value (destMsgTree_Node Input)))))
+ (and
+ (is-MsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value (destMsgTree_Node Input))))
+ (and
+ (not
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))))
+ (and
+ (is-TreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (is-TreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))))))
+ (Guard_Checkfn
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right (destMsgTree_Node Input))))))
+ (and
+ (=>
+ (and (not (is-MsgTree_Leaf Input))
+ (and (is-MsgTree_Node Input)
+ (and
+ (not
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (and
+ (is-MsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (is-TreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input))))))))
+ (Guard_Checkfn
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input))))))
+ (and
+ (DWS_Idempotentfn
+ (MsgTree_Node_recd_Value (destMsgTree_Node Input)))
+ (and
+ (is-TreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))))))))
+ (not
+ (Guard_Checkfn
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))))))
+(assert
+ (=
+ (Guard_Checkfn
+ (destTreeResult_TreeOK
+ (Guardfn (MsgTree_Node_recd_Right (destMsgTree_Node Input)))))
+ (ite
+ (is-MsgTree_Leaf
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right (destMsgTree_Node Input)))))
+ true
+ (and
+ (is-MsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))))
+ (and
+ (=
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))
+ (and
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))
+(assert
+ (=
+ (Guard_Checkfn
+ (destTreeResult_TreeOK
+ (Guardfn (MsgTree_Node_recd_Left (destMsgTree_Node Input)))))
+ (ite
+ (is-MsgTree_Leaf
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input)))))
+ true
+ (and
+ (is-MsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input))))))))
+ (and
+ (=
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input))))))
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))))))))
+ (and
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))))))
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))))))))))))
+(assert
+ (=
+ (Guard_Checkfn
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f (MsgTree_Node_recd_Value (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))
+ (ite
+ (is-MsgTree_Leaf
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))
+ true
+ (and
+ (is-MsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))))))))))))
+ (and
+ (=
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))))))))))
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))))
+ (and
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))))))))
+(assert
+ (=
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right (destMsgTree_Node Input)))))))
+ (ite
+ (is-MsgTree_Leaf
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right (destMsgTree_Node Input)))))))
+ true
+ (and
+ (is-MsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))))))
+ (and
+ (=
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))))
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))
+ (and
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))
+(assert
+ (=
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right (destMsgTree_Node Input)))))))
+ (ite
+ (is-MsgTree_Leaf
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right (destMsgTree_Node Input)))))))
+ true
+ (and
+ (is-MsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))))))
+ (and
+ (=
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))))
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))
+ (and
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))
+(assert
+ (=
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input)))))))
+ (ite
+ (is-MsgTree_Leaf
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input)))))))
+ true
+ (and
+ (is-MsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))))))))
+ (and
+ (=
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))))))
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))))))))))
+ (and
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))))))))
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))))))))))))))
+(assert
+ (=
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input)))))))
+ (ite
+ (is-MsgTree_Leaf
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input)))))))
+ true
+ (and
+ (is-MsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))))))))
+ (and
+ (=
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))))))
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))))))))))
+ (and
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))))))))
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))))))))))))))
+(assert
+ (=
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))
+ (ite
+ (is-MsgTree_Leaf
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))
+ true
+ (and
+ (is-MsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))))))))))))))
+ (and
+ (=
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))))))))))))
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))))))
+ (and
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))))
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))))))))))
+(assert
+ (=
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))
+ (ite
+ (is-MsgTree_Leaf
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))
+ true
+ (and
+ (is-MsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))))))))))))))
+ (and
+ (=
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))))))))))))
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))))))
+ (and
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))))
+ (Guard_Checkfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))))))))))))))))))))))
+(assert
+ (not
+ (not
+ (is-MsgTree_Leaf
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right (destMsgTree_Node Input))))))))))
+(assert
+ (not
+ (not
+ (is-MsgTree_Leaf
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right (destMsgTree_Node Input))))))))))
+(assert
+ (not
+ (not
+ (is-MsgTree_Leaf
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input))))))))))
+(assert
+ (not
+ (not
+ (is-MsgTree_Leaf
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left (destMsgTree_Node Input))))))))))
+(assert
+ (not
+ (not
+ (is-MsgTree_Leaf
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))))))))))))))
+(assert
+ (not
+ (not
+ (is-MsgTree_Leaf
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node
+ (destTreeResult_TreeOK
+ (ite (is-MsgTree_Leaf Input)
+ (TreeResult_TreeOK MsgTree_Leaf)
+ (ite
+ (is-MsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (TreeResult_TreeAudit
+ (destMsgResult_MsgAudit
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input)))))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input)))
+ (ite
+ (is-TreeResult_TreeAudit
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input)))
+ (TreeResult_TreeOK
+ (MsgTree_Node
+ (MsgTree_Node_recd
+ (destMsgResult_MsgOK
+ (f
+ (MsgTree_Node_recd_Value
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Left
+ (destMsgTree_Node Input))))
+ (destTreeResult_TreeOK
+ (Guardfn
+ (MsgTree_Node_recd_Right
+ (destMsgTree_Node Input))))))))))))))))))
+(check-sat)
+(exit)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback