\profile "Java Profile";
\settings {
"#Proof-Settings-Config-File
#Thu Nov 07 16:36:06 CET 2019
[StrategyProperty]OSS_OPTIONS_KEY=OSS_ON
[StrategyProperty]VBT_PHASE=VBT_SYM_EX
[SMTSettings]useUninterpretedMultiplication=true
[SMTSettings]SelectedTaclets=
[StrategyProperty]METHOD_OPTIONS_KEY=METHOD_CONTRACT
[StrategyProperty]USER_TACLETS_OPTIONS_KEY3=USER_TACLETS_OFF
[StrategyProperty]SYMBOLIC_EXECUTION_ALIAS_CHECK_OPTIONS_KEY=SYMBOLIC_EXECUTION_ALIAS_CHECK_NEVER
[StrategyProperty]LOOP_OPTIONS_KEY=LOOP_SCOPE_INVARIANT
[StrategyProperty]USER_TACLETS_OPTIONS_KEY2=USER_TACLETS_OFF
[StrategyProperty]USER_TACLETS_OPTIONS_KEY1=USER_TACLETS_OFF
[StrategyProperty]QUANTIFIERS_OPTIONS_KEY=QUANTIFIERS_NON_SPLITTING_WITH_PROGS
[StrategyProperty]NON_LIN_ARITH_OPTIONS_KEY=NON_LIN_ARITH_COMPLETION
[SMTSettings]instantiateHierarchyAssumptions=true
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT_INTERNAL
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
[StrategyProperty]SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OPTIONS_KEY=SYMBOLIC_EXECUTION_NON_EXECUTION_BRANCH_HIDING_OFF
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[Choice]DefaultChoices=assertions-assertions\\:on , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:ban , JavaCard-JavaCard\\:off , Strings-Strings\\:on , modelFields-modelFields\\:treatAsAxiom , bigint-bigint\\:on , sequences-sequences\\:on , moreSeqRules-moreSeqRules\\:off , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , permissions-permissions\\:off , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , mergeGenerateIsWeakeningGoal-mergeGenerateIsWeakeningGoal\\:off
[SMTSettings]useConstantsForBigOrSmallIntegers=true
[StrategyProperty]STOPMODE_OPTIONS_KEY=STOPMODE_DEFAULT
[StrategyProperty]QUERYAXIOM_OPTIONS_KEY=QUERYAXIOM_ON
[StrategyProperty]INF_FLOW_CHECK_PROPERTY=INF_FLOW_CHECK_FALSE
[SMTSettings]maxGenericSorts=2
[SMTSettings]integersMinimum=-2147483645
[SMTSettings]invariantForall=false
[SMTSettings]UseBuiltUniqueness=false
[SMTSettings]explicitTypeHierarchy=false
[Strategy]ActiveStrategy=JavaCardDLStrategy
[StrategyProperty]SPLITTING_OPTIONS_KEY=SPLITTING_DELAYED
[StrategyProperty]MPS_OPTIONS_KEY=MPS_MERGE
"
}
\javaSource "..";
\proofObligation "#Proof Obligation Settings
#Thu Nov 07 16:36:06 CET 2019
name=MarbleRPS[MarbleRPS\\:\\:createNewPlayer(org.hyperledger.fabric.shim.ChaincodeStub,int,java.lang.String)].JML normal_behavior operation contract.0
contract=MarbleRPS[MarbleRPS\\:\\:createNewPlayer(org.hyperledger.fabric.shim.ChaincodeStub,int,java.lang.String)].JML normal_behavior operation contract.0
class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
";
\proof {
(keyLog "0" (keyUser "jonas" ) (keyVersion "2d2a68348e607ba00900a9ecfaee13afec14c614"))
(autoModeTime "15638")
(branch "dummy ID"
(builtin "One Step Simplification" (formula "1") (newnames "stub,pid,name,result,exc,heapAtPre,o,f"))
(rule "impRight" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "2"))
(rule "andLeft" (formula "1"))
(rule "notLeft" (formula "4"))
(rule "notLeft" (formula "3"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "2"))
(rule "replace_known_right" (formula "2") (term "0") (ifseqformula "5"))
(builtin "One Step Simplification" (formula "2"))
(rule "replace_known_right" (formula "3") (term "0") (ifseqformula "6"))
(builtin "One Step Simplification" (formula "3"))
(rule "polySimp_addComm0" (formula "7") (term "1,0,0,0,1"))
(rule "assignment" (formula "7") (term "1"))
(builtin "One Step Simplification" (formula "7"))
(rule "methodBodyExpand" (formula "7") (term "1") (newnames "heapBefore_createNewPlayer,savedHeapBefore_createNewPlayer"))
(builtin "One Step Simplification" (formula "7"))
(rule "variableDeclarationAssign" (formula "7") (term "1"))
(rule "variableDeclaration" (formula "7") (term "1") (newnames "p"))
(rule "instanceCreationAssignment" (formula "7") (term "1") (inst "#v0=p_1"))
(rule "variableDeclarationAssign" (formula "7") (term "1"))
(rule "variableDeclaration" (formula "7") (term "1") (newnames "p_1"))
(rule "staticMethodCallStaticWithAssignmentViaTypereference" (formula "7") (term "1") (inst "#v0=p_2"))
(rule "variableDeclaration" (formula "7") (term "1") (newnames "p_2"))
(rule "methodBodyExpand" (formula "7") (term "1") (newnames "heapBefore_,savedHeapBefore_"))
(builtin "One Step Simplification" (formula "7"))
(rule "variableDeclaration" (formula "7") (term "1") (newnames "__NEW__"))
(rule "staticMethodCallStaticWithAssignmentViaTypereference" (formula "7") (term "1") (inst "#v0=p_3"))
(rule "variableDeclaration" (formula "7") (term "1") (newnames "p_3"))
(rule "allocateInstance" (formula "7"))
(builtin "One Step Simplification" (formula "8"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "2")))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "notLeft" (formula "1"))
(rule "notLeft" (formula "1"))
(rule "blockEmpty" (formula "10") (term "1"))
(rule "assignment" (formula "10") (term "1"))
(builtin "One Step Simplification" (formula "10"))
(rule "methodBodyExpand" (formula "10") (term "1") (newnames "heapBefore_,savedHeapBefore_"))
(builtin "One Step Simplification" (formula "10"))
(rule "assignment_write_attribute_this" (formula "10"))
(builtin "One Step Simplification" (formula "10"))
(rule "methodCallWithinClass" (formula "10") (term "1"))
(rule "methodBodyExpand" (formula "10") (term "1") (newnames "heapBefore_,savedHeapBefore_"))
(builtin "One Step Simplification" (formula "10"))
(rule "methodCallSuper" (formula "10") (term "1"))
(rule "methodBodyExpand" (formula "10") (term "1") (newnames "heapBefore_,savedHeapBefore_"))
(builtin "One Step Simplification" (formula "10"))
(rule "methodCallSuper" (formula "10") (term "1"))
(rule "methodBodyExpand" (formula "10") (term "1") (newnames "heapBefore__0,savedHeapBefore__0"))
(builtin "One Step Simplification" (formula "10"))
(rule "methodCallEmpty" (formula "10") (term "1"))
(rule "methodCallEmpty" (formula "10") (term "1"))
(rule "blockEmpty" (formula "10") (term "1"))
(rule "assignment_write_attribute_this" (formula "10"))
(builtin "One Step Simplification" (formula "10"))
(rule "assignment_write_attribute_this" (formula "10"))
(builtin "One Step Simplification" (formula "10"))
(rule "methodCallEmpty" (formula "10") (term "1"))
(rule "blockEmpty" (formula "10") (term "1"))
(rule "methodCallReturnIgnoreResult" (formula "10") (term "1"))
(rule "methodCallReturn" (formula "10") (term "1"))
(rule "assignment" (formula "10") (term "1"))
(builtin "One Step Simplification" (formula "10"))
(rule "methodCallEmpty" (formula "10") (term "1"))
(rule "blockEmpty" (formula "10") (term "1"))
(rule "assignment" (formula "10") (term "1"))
(builtin "One Step Simplification" (formula "10"))
(rule "variableDeclarationAssign" (formula "10") (term "1"))
(rule "variableDeclaration" (formula "10") (term "1") (newnames "var"))
(rule "assignment" (formula "10") (term "1"))
(builtin "One Step Simplification" (formula "10"))
(rule "variableDeclarationAssign" (formula "10") (term "1"))
(rule "variableDeclaration" (formula "10") (term "1") (newnames "var_1"))
(rule "assignment" (formula "10") (term "1"))
(builtin "One Step Simplification" (formula "10"))
(rule "methodBodyExpand" (formula "10") (term "1") (newnames "heapBefore_,savedHeapBefore_"))
(builtin "One Step Simplification" (formula "10"))
(rule "methodCallSuper" (formula "10") (term "1"))
(rule "methodBodyExpand" (formula "10") (term "1") (newnames "heapBefore__0,savedHeapBefore__0"))
(builtin "One Step Simplification" (formula "10"))
(rule "methodCallSuper" (formula "10") (term "1"))
(rule "methodBodyExpand" (formula "10") (term "1") (newnames "heapBefore__1,savedHeapBefore__1"))
(builtin "One Step Simplification" (formula "10"))
(rule "methodCallEmpty" (formula "10") (term "1"))
(rule "methodCallEmpty" (formula "10") (term "1"))
(rule "blockEmpty" (formula "10") (term "1"))
(rule "assignment_write_attribute_this" (formula "10"))
(builtin "One Step Simplification" (formula "10"))
(rule "assignment_write_attribute_this" (formula "10"))
(builtin "One Step Simplification" (formula "10"))
(rule "methodCallEmpty" (formula "10") (term "1"))
(rule "blockEmpty" (formula "10") (term "1"))
(rule "assignment_write_attribute" (formula "10"))
(branch "Normal Execution (p_1 != null)"
(builtin "One Step Simplification" (formula "10"))
(rule "assignment" (formula "10") (term "1"))
(builtin "One Step Simplification" (formula "10"))
(rule "methodCallUnfoldArguments" (formula "10") (term "1"))
(rule "variableDeclarationAssign" (formula "10") (term "1"))
(rule "variableDeclaration" (formula "10") (term "1") (newnames "var_2"))
(rule "assignment" (formula "10") (term "1"))
(builtin "One Step Simplification" (formula "10"))
(rule "variableDeclarationAssign" (formula "10") (term "1"))
(rule "variableDeclaration" (formula "10") (term "1") (newnames "var_3"))
(rule "assignment" (formula "10") (term "1"))
(builtin "One Step Simplification" (formula "10"))
(rule "variableDeclarationAssign" (formula "10") (term "1"))
(rule "variableDeclaration" (formula "10") (term "1") (newnames "var_4"))
(builtin "Use Operation Contract" (formula "10") (newnames "heapBefore_serialize,result_0,exc_0,heapAfter_serialize,anon_heap_serialize") (contract "Player[org.hyperledger.fabric.shim.LedgerData::serialize()].JML normal_behavior operation contract.0"))
(branch "Post (serialize)"
(builtin "One Step Simplification" (formula "12"))
(builtin "One Step Simplification" (formula "7"))
(rule "andLeft" (formula "7"))
(rule "selectCreatedOfAnonAsFormulaEQ" (formula "8") (term "1,1,0") (ifseqformula "7"))
(rule "andLeft" (formula "8"))
(rule "andLeft" (formula "9"))
(rule "andLeft" (formula "8"))
(rule "andLeft" (formula "9"))
(rule "andLeft" (formula "10"))
(rule "notLeft" (formula "10"))
(rule "notLeft" (formula "10"))
(rule "replace_known_right" (formula "8") (term "0") (ifseqformula "11"))
(builtin "One Step Simplification" (formula "8") (ifInst "" (formula "12")))
(rule "dismissNonSelectedField" (formula "12") (term "0"))
(rule "dismissNonSelectedField" (formula "12") (term "0"))
(rule "dismissNonSelectedField" (formula "12") (term "0"))
(rule "assignment" (formula "17") (term "1"))
(builtin "One Step Simplification" (formula "17"))
(rule "pullOutSelect" (formula "12") (term "0") (inst "selectSK=java_lang_Object_created__0"))
(rule "simplifySelectOfCreate" (formula "1"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "15")))
(rule "castDel" (formula "1") (term "1,0"))
(rule "eqSymm" (formula "1") (term "0,0"))
(rule "sortsDisjointModuloNull" (formula "1") (term "0,0"))
(rule "replace_known_right" (formula "1") (term "1,0,0") (ifseqformula "15"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "12")))
(rule "applyEqReverse" (formula "13") (term "0") (ifseqformula "1"))
(rule "hideAuxiliaryEq" (formula "1"))
(builtin "Use Operation Contract" (formula "17") (newnames "heapBefore_putState,exc_1,heapAfter_putState,anon_heap_putState") (contract "org.hyperledger.fabric.shim.ChaincodeStub[org.hyperledger.fabric.shim.ChaincodeStub::putState(int,[B)].JML normal_behavior operation contract.0"))
(branch "Post (putState)"
(builtin "One Step Simplification" (formula "19"))
(builtin "One Step Simplification" (formula "12"))
(rule "andLeft" (formula "12"))
(rule "andLeft" (formula "13"))
(rule "andLeft" (formula "14"))
(rule "eqSymm" (formula "14"))
(rule "blockEmpty" (formula "21") (term "1"))
(rule "pullOutSelect" (formula "14") (term "0,0") (inst "selectSK=org_hyperledger_fabric_shim_ChaincodeStub_transactionLog_0"))
(rule "simplifySelectOfAnonEQ" (formula "14") (ifseqformula "7"))
(builtin "One Step Simplification" (formula "14") (ifInst "" (formula "20")))
(rule "eqSymm" (formula "15"))
(rule "ifthenelse_negated" (formula "14") (term "0"))
(rule "dismissNonSelectedField" (formula "14") (term "0,0,0"))
(rule "dismissNonSelectedField" (formula "14") (term "1,0"))
(rule "dismissNonSelectedField" (formula "14") (term "0,0,0"))
(rule "dismissNonSelectedField" (formula "14") (term "1,0"))
(rule "dismissNonSelectedField" (formula "14") (term "0,0,0"))
(rule "dismissNonSelectedField" (formula "14") (term "1,0"))
(rule "pullOutSelect" (formula "15") (term "0") (inst "selectSK=org_hyperledger_fabric_shim_ChaincodeStub_transactionLog_1"))
(rule "simplifySelectOfAnonEQ" (formula "15") (ifseqformula "12"))
(builtin "One Step Simplification" (formula "15") (ifInst "" (formula "21")))
(rule "replaceKnownSelect_taclet000_2" (formula "15") (term "2,0"))
(rule "selectCreatedOfAnonAsFormulaEQ" (formula "15") (term "0,1,0,0") (ifseqformula "7"))
(rule "eqSymm" (formula "16"))
(rule "applyEqReverse" (formula "15") (term "1") (ifseqformula "16"))
(rule "hideAuxiliaryEq" (formula "16"))
(rule "elementOfSingleton" (formula "15") (term "0,0,0"))
(builtin "One Step Simplification" (formula "15"))
(rule "pullOutSelect" (formula "14") (term "0,0,0") (inst "selectSK=java_lang_Object_created__1"))
(rule "simplifySelectOfCreate" (formula "14"))
(builtin "One Step Simplification" (formula "14") (ifInst "" (formula "20")))
(rule "castDel" (formula "14") (term "1,0"))
(rule "eqSymm" (formula "14") (term "0,0"))
(rule "applyEq" (formula "14") (term "2,0") (ifseqformula "3"))
(builtin "One Step Simplification" (formula "14"))
(rule "applyEqReverse" (formula "15") (term "0,0,0") (ifseqformula "14"))
(builtin "One Step Simplification" (formula "15"))
(rule "simplifySelectOfCreate" (formula "15"))
(builtin "One Step Simplification" (formula "15") (ifInst "" (formula "20")))
(rule "applyEqReverse" (formula "16") (term "0,1") (ifseqformula "15"))
(rule "hideAuxiliaryEq" (formula "14"))
(rule "hideAuxiliaryEq" (formula "14"))
(rule "returnUnfold" (formula "21") (term "1") (inst "#v0=r"))
(rule "variableDeclarationAssign" (formula "21") (term "1"))
(rule "variableDeclaration" (formula "21") (term "1") (newnames "r"))
(rule "methodCallWithAssignmentUnfoldArguments" (formula "21") (term "1"))
(rule "variableDeclarationAssign" (formula "21") (term "1"))
(rule "variableDeclaration" (formula "21") (term "1") (newnames "var_5"))
(rule "stringAssignment" (formula "21") (term "1"))
(builtin "One Step Simplification" (formula "23"))
(builtin "One Step Simplification" (formula "1"))
(builtin "One Step Simplification" (formula "2"))
(rule "selectCreatedOfAnonAsFormulaEQ" (formula "2") (ifseqformula "14"))
(rule "selectCreatedOfAnonAsFormulaEQ" (formula "2") (term "0") (ifseqformula "9"))
(rule "notLeft" (formula "1"))
(rule "dismissNonSelectedField" (formula "1") (term "0,0,0"))
(rule "dismissNonSelectedField" (formula "1") (term "0,0,0"))
(rule "dismissNonSelectedField" (formula "1") (term "0,0,0"))
(rule "pullOutSelect" (formula "1") (term "0,0,0") (inst "selectSK=java_lang_Object_created__2"))
(rule "simplifySelectOfCreate" (formula "1"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "21")))
(rule "castDel" (formula "1") (term "1,0"))
(rule "sortsDisjointModuloNull" (formula "1") (term "0,0"))
(rule "replace_known_right" (formula "1") (term "0,0,0") (ifseqformula "21"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "17")))
(rule "applyEqReverse" (formula "2") (term "0,0,0") (ifseqformula "1"))
(rule "hideAuxiliaryEq" (formula "1"))
(rule "commute_or_2" (formula "1"))
(rule "equalityToSeqGetAndSeqLenLeft" (formula "10") (inst "iv=iv"))
(rule "andLeft" (formula "10"))
(rule "inEqSimp_commuteLeq" (formula "11") (term "0,0,0"))
(rule "applyEq" (formula "11") (term "0,1,1,0,0") (ifseqformula "12"))
(rule "applyEq" (formula "10") (term "0,0") (ifseqformula "12"))
(builtin "One Step Simplification" (formula "10"))
(rule "true_left" (formula "10"))
(rule "applyEq" (formula "10") (term "0,0,1,0") (ifseqformula "11"))
(builtin "One Step Simplification" (formula "10"))
(rule "true_left" (formula "10"))
(rule "equalityToSeqGetAndSeqLenLeft" (formula "15") (inst "iv=iv"))
(rule "andLeft" (formula "15"))
(rule "lenOfSeqConcat" (formula "15") (term "1"))
(builtin "One Step Simplification" (formula "15"))
(rule "polySimp_addComm0" (formula "15") (term "1"))
(rule "inEqSimp_commuteLeq" (formula "16") (term "0,0,0"))
(rule "applyEq" (formula "16") (term "1,1,0,0") (ifseqformula "15"))
(rule "applyEq" (formula "15") (term "0,0") (ifseqformula "17"))
(rule "lenOfSeqConcat" (formula "15") (term "0"))
(builtin "One Step Simplification" (formula "15"))
(rule "polySimp_addComm0" (formula "15") (term "0"))
(builtin "One Step Simplification" (formula "15"))
(rule "true_left" (formula "15"))
(rule "applyEq" (formula "15") (term "0,0,1,0") (ifseqformula "16"))
(builtin "One Step Simplification" (formula "15"))
(rule "true_left" (formula "15"))
(rule "methodCallWithAssignmentWithinClass" (formula "23") (term "1") (inst "#v0=r_1"))
(rule "variableDeclaration" (formula "23") (term "1") (newnames "r_1"))
(rule "variableDeclarationAssign" (formula "23") (term "1"))
(rule "variableDeclaration" (formula "23") (term "1") (newnames "message"))
(rule "assignment" (formula "23") (term "1"))
(builtin "One Step Simplification" (formula "23"))
(rule "methodBodyExpand" (formula "23") (term "1") (newnames "heapBefore_newSuccessResponse,savedHeapBefore_newSuccessResponse"))
(builtin "One Step Simplification" (formula "23"))
(rule "returnUnfold" (formula "23") (term "1") (inst "#v0=r_2"))
(rule "variableDeclarationAssign" (formula "23") (term "1"))
(rule "variableDeclaration" (formula "23") (term "1") (newnames "r_2"))
(rule "methodCallWithAssignmentWithinClass" (formula "23") (term "1") (inst "#v0=r_3"))
(rule "variableDeclaration" (formula "23") (term "1") (newnames "r_3"))
(rule "variableDeclarationAssign" (formula "23") (term "1"))
(rule "variableDeclaration" (formula "23") (term "1") (newnames "message_1"))
(rule "assignment" (formula "23") (term "1"))
(builtin "One Step Simplification" (formula "23"))
(rule "variableDeclarationAssign" (formula "23") (term "1"))
(rule "variableDeclaration" (formula "23") (term "1") (newnames "payload"))
(rule "assignment" (formula "23") (term "1"))
(builtin "One Step Simplification" (formula "23"))
(rule "methodBodyExpand" (formula "23") (term "1") (newnames "heapBefore_newSuccessResponse_0,savedHeapBefore_newSuccessResponse_0"))
(builtin "One Step Simplification" (formula "23"))
(rule "returnUnfold" (formula "23") (term "1") (inst "#v0=r_4"))
(rule "variableDeclarationAssign" (formula "23") (term "1"))
(rule "variableDeclaration" (formula "23") (term "1") (newnames "r_4"))
(rule "instanceCreationAssignmentUnfoldArguments" (formula "23") (term "1"))
(rule "variableDeclarationAssign" (formula "23") (term "1"))
(rule "variableDeclaration" (formula "23") (term "1") (newnames "var_6"))
(rule "activeUseStaticFieldReadAccess" (formula "23") (term "1"))
(rule "assignment_read_static_attribute" (formula "23") (term "1"))
(builtin "One Step Simplification" (formula "23"))
(rule "pullOutSelect" (formula "23") (term "0,1,0") (inst "selectSK=org_hyperledger_fabric_shim_Chaincode_Response_Status_SUCCESS_0"))
(rule "simplifySelectOfAnonEQ" (formula "1") (ifseqformula "14"))
(builtin "One Step Simplification" (formula "1"))
(rule "elementOfSingleton" (formula "1") (term "0,0"))
(builtin "One Step Simplification" (formula "1"))
(rule "simplifySelectOfAnonEQ" (formula "1") (ifseqformula "9"))
(builtin "One Step Simplification" (formula "1"))
(rule "simplifySelectOfStore" (formula "1"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "21")))
(rule "simplifySelectOfStore" (formula "1"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "21")))
(rule "simplifySelectOfStore" (formula "1"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "21")))
(rule "simplifySelectOfCreate" (formula "1"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "21")) (ifInst "" (formula "21")))
(rule "applyEqReverse" (formula "24") (term "0,1,0") (ifseqformula "1"))
(rule "hideAuxiliaryEq" (formula "1"))
(rule "variableDeclarationAssign" (formula "23") (term "1"))
(rule "variableDeclaration" (formula "23") (term "1") (newnames "var_7"))
(rule "assignment" (formula "23") (term "1"))
(builtin "One Step Simplification" (formula "23"))
(rule "variableDeclarationAssign" (formula "23") (term "1"))
(rule "variableDeclaration" (formula "23") (term "1") (newnames "var_8"))
(rule "assignment" (formula "23") (term "1"))
(builtin "One Step Simplification" (formula "23"))
(rule "onlyCreatedObjectsAreReferenced" (formula "23") (term "0,1,0,0,0") (ifseqformula "3"))
(rule "instanceCreationAssignment" (formula "24") (term "1") (inst "#v0=r_5"))
(rule "variableDeclarationAssign" (formula "24") (term "1"))
(rule "variableDeclaration" (formula "24") (term "1") (newnames "r_5"))
(rule "staticMethodCallStaticWithAssignmentViaTypereference" (formula "24") (term "1") (inst "#v0=r_6"))
(rule "variableDeclaration" (formula "24") (term "1") (newnames "r_6"))
(rule "methodBodyExpand" (formula "24") (term "1") (newnames "heapBefore__0,savedHeapBefore__0"))
(builtin "One Step Simplification" (formula "24"))
(rule "variableDeclaration" (formula "24") (term "1") (newnames "__NEW___1"))
(rule "staticMethodCallStaticWithAssignmentViaTypereference" (formula "24") (term "1") (inst "#v0=r_7"))
(rule "variableDeclaration" (formula "24") (term "1") (newnames "r_7"))
(rule "allocateInstance" (formula "24"))
(builtin "One Step Simplification" (formula "25"))
(builtin "One Step Simplification" (formula "1"))
(rule "wellFormedAnonEQ" (formula "1") (term "0,1,0") (ifseqformula "15"))
(rule "wellFormedAnonEQ" (formula "1") (term "0,0,1,0") (ifseqformula "10"))
(rule "selectCreatedOfAnonAsFormulaEQ" (formula "1") (term "0,1,1,0") (ifseqformula "15"))
(rule "wellFormedStorePrimitive" (formula "1") (term "0,0,0,1,0"))
(rule "selectCreatedOfAnonAsFormulaEQ" (formula "1") (term "0,0,1,1,0") (ifseqformula "10"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "notLeft" (formula "1"))
(rule "replace_known_left" (formula "1") (term "1,0") (ifseqformula "15"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "10")))
(rule "dismissNonSelectedField" (formula "1") (term "0,0,0,0,1"))
(rule "dismissNonSelectedField" (formula "1") (term "0,0,0,0,1"))
(rule "dismissNonSelectedField" (formula "1") (term "0,0,0,0,1"))
(rule "blockEmpty" (formula "27") (term "1"))
(rule "assignment" (formula "27") (term "1"))
(builtin "One Step Simplification" (formula "27"))
(rule "wellFormedStoreObject" (formula "1") (term "0"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "26")))
(rule "dismissNonSelectedField" (formula "1") (term "0,0"))
(rule "pullOutSelect" (formula "1") (term "0,0,0,0,1") (inst "selectSK=java_lang_Object_created__3"))
(rule "simplifySelectOfCreate" (formula "1"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "25")))
(rule "castDel" (formula "1") (term "1,0"))
(rule "eqSymm" (formula "1") (term "0,0"))
(rule "sortsDisjointModuloNull" (formula "1") (term "0,0"))
(rule "replace_known_right" (formula "1") (term "1,0,0") (ifseqformula "25"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "20")))
(rule "applyEqReverse" (formula "2") (term "0,0,0,0,1") (ifseqformula "1"))
(rule "hideAuxiliaryEq" (formula "1"))
(rule "pullOutSelect" (formula "1") (term "0,0") (inst "selectSK=java_lang_Object_created__4"))
(rule "simplifySelectOfCreate" (formula "1"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "25")))
(rule "castDel" (formula "1") (term "1,0"))
(rule "sortsDisjointModuloNull" (formula "1") (term "0,0"))
(rule "replace_known_right" (formula "1") (term "0,0,0") (ifseqformula "25"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "27")))
(rule "applyEqReverse" (formula "2") (term "0,0") (ifseqformula "1"))
(rule "hideAuxiliaryEq" (formula "1"))
(rule "replace_known_left" (formula "1") (term "0") (ifseqformula "8"))
(builtin "One Step Simplification" (formula "1"))
(rule "notLeft" (formula "1"))
(rule "orRight" (formula "18"))
(rule "orRight" (formula "18"))
(rule "methodBodyExpand" (formula "29") (term "1") (newnames "heapBefore__0,savedHeapBefore__0"))
(builtin "One Step Simplification" (formula "29"))
(rule "assignment_write_attribute_this" (formula "29"))
(builtin "One Step Simplification" (formula "29"))
(rule "methodCallWithinClass" (formula "29") (term "1"))
(rule "methodBodyExpand" (formula "29") (term "1") (newnames "heapBefore__0,savedHeapBefore__0"))
(builtin "One Step Simplification" (formula "29"))
(rule "methodCallSuper" (formula "29") (term "1"))
(rule "methodBodyExpand" (formula "29") (term "1") (newnames "heapBefore__1,savedHeapBefore__1"))
(builtin "One Step Simplification" (formula "29"))
(rule "methodCallEmpty" (formula "29") (term "1"))
(rule "blockEmpty" (formula "29") (term "1"))
(rule "assignment_write_attribute_this" (formula "29"))
(builtin "One Step Simplification" (formula "29"))
(rule "assignment_write_attribute_this" (formula "29"))
(builtin "One Step Simplification" (formula "29"))
(rule "assignment_write_attribute_this" (formula "29"))
(builtin "One Step Simplification" (formula "29"))
(rule "methodCallEmpty" (formula "29") (term "1"))
(rule "blockEmpty" (formula "29") (term "1"))
(rule "methodCallReturnIgnoreResult" (formula "29") (term "1"))
(rule "methodCallReturn" (formula "29") (term "1"))
(rule "assignment" (formula "29") (term "1"))
(builtin "One Step Simplification" (formula "29"))
(rule "methodCallEmpty" (formula "29") (term "1"))
(rule "blockEmpty" (formula "29") (term "1"))
(rule "assignment" (formula "29") (term "1"))
(builtin "One Step Simplification" (formula "29"))
(rule "variableDeclarationAssign" (formula "29") (term "1"))
(rule "variableDeclaration" (formula "29") (term "1") (newnames "var_9"))
(rule "assignment" (formula "29") (term "1"))
(builtin "One Step Simplification" (formula "29"))
(rule "variableDeclarationAssign" (formula "29") (term "1"))
(rule "variableDeclaration" (formula "29") (term "1") (newnames "var_10"))
(rule "assignment" (formula "29") (term "1"))
(builtin "One Step Simplification" (formula "29"))
(rule "variableDeclarationAssign" (formula "29") (term "1"))
(rule "variableDeclaration" (formula "29") (term "1") (newnames "var_11"))
(rule "assignment" (formula "29") (term "1"))
(builtin "One Step Simplification" (formula "29"))
(rule "methodBodyExpand" (formula "29") (term "1") (newnames "heapBefore__2,savedHeapBefore__2"))
(builtin "One Step Simplification" (formula "29"))
(rule "methodCallSuper" (formula "29") (term "1"))
(rule "methodBodyExpand" (formula "29") (term "1") (newnames "heapBefore__3,savedHeapBefore__3"))
(builtin "One Step Simplification" (formula "29"))
(rule "methodCallEmpty" (formula "29") (term "1"))
(rule "blockEmpty" (formula "29") (term "1"))
(rule "assignment_write_attribute_this" (formula "29"))
(builtin "One Step Simplification" (formula "29"))
(rule "assignment_write_attribute_this" (formula "29"))
(builtin "One Step Simplification" (formula "29"))
(rule "assignment_write_attribute_this" (formula "29"))
(builtin "One Step Simplification" (formula "29"))
(rule "methodCallEmpty" (formula "29") (term "1"))
(rule "blockEmpty" (formula "29") (term "1"))
(rule "assignment_write_attribute" (formula "29"))
(branch "Normal Execution (r_5 != null)"
(builtin "One Step Simplification" (formula "29"))
(rule "assignment" (formula "29") (term "1"))
(builtin "One Step Simplification" (formula "29"))
(rule "blockEmpty" (formula "29") (term "1"))
(rule "methodCallReturn" (formula "29") (term "1"))
(rule "assignment" (formula "29") (term "1"))
(builtin "One Step Simplification" (formula "29"))
(rule "methodCallEmpty" (formula "29") (term "1"))
(rule "blockEmpty" (formula "29") (term "1"))
(rule "assignment" (formula "29") (term "1"))
(builtin "One Step Simplification" (formula "29"))
(rule "methodCallReturn" (formula "29") (term "1"))
(rule "assignment" (formula "29") (term "1"))
(builtin "One Step Simplification" (formula "29"))
(rule "methodCallEmpty" (formula "29") (term "1"))
(rule "blockEmpty" (formula "29") (term "1"))
(rule "assignment" (formula "29") (term "1"))
(builtin "One Step Simplification" (formula "29"))
(rule "blockEmpty" (formula "29") (term "1"))
(rule "methodCallReturn" (formula "29") (term "1"))
(rule "assignment" (formula "29") (term "1"))
(builtin "One Step Simplification" (formula "29"))
(rule "methodCallEmpty" (formula "29") (term "1"))
(rule "tryEmpty" (formula "29") (term "1"))
(rule "emptyModality" (formula "29") (term "1"))
(rule "andRight" (formula "29"))
(branch "Case 1"
(rule "andRight" (formula "29"))
(branch "Case 1"
(builtin "One Step Simplification" (formula "29"))
(rule "dismissNonSelectedField" (formula "29") (term "0,0"))
(rule "dismissNonSelectedField" (formula "29") (term "0,0"))
(rule "dismissNonSelectedField" (formula "29") (term "0,0"))
(rule "dismissNonSelectedField" (formula "29") (term "0,0"))
(rule "array2seqDef" (formula "12") (term "0") (inst "u=u"))
(rule "array2seqDef" (formula "17") (term "1,0,1,1") (inst "u=u"))
(rule "eqSymm" (formula "17"))
(rule "pullOutSelect" (formula "29") (term "0,0") (inst "selectSK=org_hyperledger_fabric_shim_ChaincodeStub_transactionLog_2"))
(rule "simplifySelectOfCreate" (formula "1"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "22")))
(rule "replaceKnownSelect_taclet000_3" (formula "1") (term "0"))
(rule "replaceKnownAuxiliaryConstant_taclet000_4" (formula "1") (term "0"))
(rule "replaceKnownAuxiliaryConstant_taclet000_8" (formula "1") (term "0,0"))
(rule "applyEqReverse" (formula "30") (term "0,0") (ifseqformula "1"))
(rule "hideAuxiliaryEq" (formula "1"))
(rule "lenOfSeqConcat" (formula "29") (term "0"))
(builtin "One Step Simplification" (formula "29"))
(rule "polySimp_homoEq" (formula "29"))
(rule "polySimp_mulComm0" (formula "29") (term "1,0"))
(rule "polySimp_addComm0" (formula "29") (term "1,1,0"))
(rule "polySimp_rightDist" (formula "29") (term "1,0"))
(rule "mul_literals" (formula "29") (term "0,1,0"))
(rule "polySimp_addAssoc" (formula "29") (term "0"))
(rule "polySimp_addComm1" (formula "29") (term "0,0"))
(rule "add_literals" (formula "29") (term "0,0,0"))
(rule "add_zero_left" (formula "29") (term "0,0"))
(rule "polySimp_pullOutFactor1" (formula "29") (term "0"))
(rule "add_literals" (formula "29") (term "1,0"))
(rule "times_zero_1" (formula "29") (term "0"))
(builtin "One Step Simplification" (formula "29"))
(rule "closeTrue" (formula "29"))
)
(branch "Case 2"
(rule "andRight" (formula "29"))
(branch "Case 1"
(builtin "One Step Simplification" (formula "29"))
(rule "dismissNonSelectedField" (formula "29") (term "0,0,0,0,0,0"))
(rule "dismissNonSelectedField" (formula "29") (term "0,0,0,0,0,0"))
(rule "dismissNonSelectedField" (formula "29") (term "0,0,0,0,0,0"))
(rule "dismissNonSelectedField" (formula "29") (term "0,0,0,0,0,0"))
(rule "selectOfCreate" (formula "29") (term "0,0,0,0,0,0"))
(builtin "One Step Simplification" (formula "29") (ifInst "" (formula "21")))
(rule "selectOfAnonEQ" (formula "29") (term "0,0,0,0,0,0") (ifseqformula "15"))
(builtin "One Step Simplification" (formula "29") (ifInst "" (formula "27")))
(rule "selectOfAnonEQ" (formula "29") (term "2,0,0,0,0,0,0") (ifseqformula "10"))
(builtin "One Step Simplification" (formula "29") (ifInst "" (formula "27")))
(rule "selectOfStore" (formula "29") (term "0,0,0,2,0,0,0,0,0,0"))
(builtin "One Step Simplification" (formula "29"))
(rule "ifthenelse_negated" (formula "29") (term "2,0,0,0,0,0,0"))
(rule "selectOfStore" (formula "29") (term "1,2,0,0,0,0,0,0"))
(builtin "One Step Simplification" (formula "29"))
(rule "selectOfStore" (formula "29") (term "1,2,0,0,0,0,0,0"))
(builtin "One Step Simplification" (formula "29"))
(rule "selectOfStore" (formula "29") (term "1,2,0,0,0,0,0,0"))
(builtin "One Step Simplification" (formula "29"))
(rule "selectOfCreate" (formula "29") (term "1,2,0,0,0,0,0,0"))
(builtin "One Step Simplification" (formula "29") (ifInst "" (formula "26")))
(rule "selectOfStore" (formula "29") (term "0,0,2,0,0,0,0,0,0"))
(builtin "One Step Simplification" (formula "29"))
(rule "selectOfStore" (formula "29") (term "0,0,2,0,0,0,0,0,0"))
(builtin "One Step Simplification" (formula "29"))
(rule "selectOfCreate" (formula "29") (term "0,0,2,0,0,0,0,0,0"))
(builtin "One Step Simplification" (formula "29") (ifInst "" (formula "26")))
(rule "selectCreatedOfAnonEQ" (formula "29") (term "0,0,1,0,0,0,0,0,0,0") (ifseqformula "10"))
(builtin "One Step Simplification" (formula "29"))
(rule "ifthenelse_split" (formula "29") (term "0,0,0,0,0,0") (userinteraction))
(branch " (stub, org.hyperledger.fabric.shim.ChaincodeStub::$transactionLog) in {(stub, org.hyperledger.fabric.shim.ChaincodeStub::$transactionLog)} | !( stub.@heap[create(p_3)] [p_3.id := pid] [p_3.name := name] [p_3. := TRUE] = TRUE | stub.@anon_heap_serialize<> = TRUE) TRUE"
(rule "eqTermCut" (formula "13") (term "0") (inst "s=array2seq(heapAfter_putState, result_0)") (userinteraction))
(branch "Assume array2seq(heapAfter_serialize, result_0) = array2seq(heapAfter_putState, result_0)"
(rule "eqTermCut" (formula "31") (term "0,0,0") (inst "s=array2seq(heapAfter_serialize, result_0)") (userinteraction))
(branch "Assume (Seq)(getValue(lastEntry(stub.transactionLog@anon_heap_putState<>, pid))) = array2seq(heapAfter_serialize, result_0)"
(rule "applyEq" (formula "32") (term "0,0,0") (ifseqformula "1") (userinteraction))
(rule "extendDeserializationToPlayer" (formula "32") (term "0,0") (userinteraction))
(rule "applyEq" (formula "32") (term "0,0,0") (ifseqformula "15") (userinteraction))
(rule "extendSerializationToPlayer" (formula "32") (term "0,0,0") (userinteraction))
(rule "serializePlayer" (formula "32") (term "0,0") (userinteraction))
(rule "object2Player" (formula "32") (term "0,0") (userinteraction))
(rule "idOfNewPlayer" (formula "32") (term "0") (userinteraction))
(rule "elementOfSingleton" (formula "2") (term "0"))
(builtin "One Step Simplification" (formula "2"))
(rule "true_left" (formula "2"))
(rule "applyEq" (formula "1") (term "1") (ifseqformula "14"))
(rule "applyEq" (formula "1") (term "0,0,0,0") (ifseqformula "19"))
(rule "applyEq" (formula "14") (term "0") (ifseqformula "13"))
(rule "applyEq" (formula "1") (term "1,0,1,0,0,0,0") (ifseqformula "14"))
(rule "applyEq" (formula "13") (term "1") (ifseqformula "14"))
(rule "applyEq" (formula "19") (term "1,0,1,1") (ifseqformula "14"))
(rule "array2seqDef" (formula "13") (term "0") (inst "u=u"))
(rule "array2seqDef" (formula "14") (term "0") (inst "u=u"))
(rule "pullOutSelect" (formula "31") (term "0") (inst "selectSK=Player_id_0"))
(rule "simplifySelectOfAnonEQ" (formula "1") (ifseqformula "12"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "29")))
(rule "eqSymm" (formula "32"))
(rule "dismissNonSelectedField" (formula "1") (term "2,0"))
(rule "dismissNonSelectedField" (formula "1") (term "0,0,0,0"))
(rule "dismissNonSelectedField" (formula "1") (term "2,0"))
(rule "dismissNonSelectedField" (formula "1") (term "0,0,0,0"))
(rule "ifthenelse_negated" (formula "1") (term "0"))
(rule "dismissNonSelectedField" (formula "1") (term "0,0,0"))
(rule "pullOutSelect" (formula "1") (term "1,0") (inst "selectSK=Player_id_1"))
(rule "simplifySelectOfStore" (formula "1"))
(builtin "One Step Simplification" (formula "1"))
(rule "castDel" (formula "1") (term "0"))
(rule "applyEqReverse" (formula "2") (term "1,0") (ifseqformula "1"))
(rule "hideAuxiliaryEq" (formula "1"))
(rule "pullOutSelect" (formula "1") (term "0,0,0") (inst "selectSK=java_lang_Object_created__5"))
(rule "simplifySelectOfCreate" (formula "1"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "30")))
(rule "castDel" (formula "1") (term "0"))
(rule "applyEqReverse" (formula "2") (term "0,0,0") (ifseqformula "1"))
(builtin "One Step Simplification" (formula "2") (ifInst "" (formula "33")))
(rule "closeFalse" (formula "2"))
)
(branch "Assume (Seq)(getValue(lastEntry(stub.transactionLog@anon_heap_putState<>, pid))) != array2seq(heapAfter_serialize, result_0)"
(rule "notLeft" (formula "1") (userinteraction))
(rule "hide_right" (formula "21") (userinteraction))
(rule "hide_right" (formula "21") (userinteraction))
(rule "hide_right" (formula "21") (userinteraction))
(rule "hide_right" (formula "21") (userinteraction))
(rule "hide_right" (formula "21") (userinteraction))
(rule "hide_right" (formula "21") (userinteraction))
(rule "hide_right" (formula "21") (userinteraction))
(rule "hide_right" (formula "21") (userinteraction))
(rule "hide_right" (formula "21") (userinteraction))
(rule "hide_right" (formula "21") (userinteraction))
(rule "hide_right" (formula "21") (userinteraction))
(rule "hide_right" (formula "21") (userinteraction))
(rule "applyEq" (formula "20") (term "1") (ifseqformula "13") (userinteraction))
(rule "defLastEntry" (formula "20") (term "0,0,0") (userinteraction))
(rule "ifthenelse_split" (formula "20") (term "0,0,0") (userinteraction))
(branch " stub.transactionLog@anon_heap_putState<>.length = 0 TRUE"
(rule "elementOfSingleton" (formula "2") (term "0"))
(builtin "One Step Simplification" (formula "2"))
(rule "true_left" (formula "2"))
(rule "applyEq" (formula "13") (term "0") (ifseqformula "14"))
(rule "eqSymm" (formula "13"))
(rule "applyEq" (formula "1") (term "0,0") (ifseqformula "19"))
(rule "lenOfSeqConcat" (formula "1") (term "0"))
(builtin "One Step Simplification" (formula "1"))
(rule "polySimp_addComm0" (formula "1") (term "0"))
(rule "applyEq" (formula "19") (term "1,0,1,1") (ifseqformula "13"))
(rule "applyEq" (formula "20") (term "1") (ifseqformula "13"))
(rule "polySimp_sepPosMonomial" (formula "1"))
(rule "mul_literals" (formula "1") (term "1"))
(rule "array2seqDef" (formula "14") (term "0") (inst "u=u"))
(rule "array2seqDef" (formula "13") (term "0") (inst "u=u"))
(rule "equalityToSeqGetAndSeqLenRight" (formula "20") (inst "iv=iv"))
(rule "lenOfSeqDefEQ" (formula "20") (term "1,0") (ifseqformula "13"))
(rule "eqSymm" (formula "20") (term "0"))
(rule "polySimp_elimSub" (formula "20") (term "1,0,0"))
(rule "mul_literals" (formula "20") (term "1,1,0,0"))
(rule "add_zero_right" (formula "20") (term "1,0,0"))
(rule "inEqSimp_ltToLeq" (formula "20") (term "1,0,0,1"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0,0,1,0,0,1"))
(rule "inEqSimp_commuteLeq" (formula "20") (term "0,0,0,1"))
(rule "inEqSimp_commuteLeq" (formula "20") (term "0,0,0"))
(rule "inEqSimp_sepPosMonomial0" (formula "20") (term "1,0,0,1"))
(rule "polySimp_mulComm0" (formula "20") (term "1,1,0,0,1"))
(rule "polySimp_rightDist" (formula "20") (term "1,1,0,0,1"))
(rule "mul_literals" (formula "20") (term "0,1,1,0,0,1"))
(rule "polySimp_mulLiterals" (formula "20") (term "1,1,1,0,0,1"))
(rule "polySimp_elimOne" (formula "20") (term "1,1,1,0,0,1"))
(rule "getOfSeqDefEQ" (formula "20") (term "1,1,0,1") (ifseqformula "13"))
(rule "castDel" (formula "20") (term "2,1,1,0,1"))
(rule "castDel" (formula "20") (term "1,1,1,0,1"))
(rule "add_zero_right" (formula "20") (term "0,2,1,1,1,0,1"))
(rule "eqSymm" (formula "20") (term "1,0,1"))
(rule "polySimp_elimSub" (formula "20") (term "1,1,0,0,1,0,1"))
(rule "times_zero_2" (formula "20") (term "1,1,1,0,0,1,0,1"))
(rule "add_zero_right" (formula "20") (term "1,1,0,0,1,0,1"))
(rule "inEqSimp_ltToLeq" (formula "20") (term "1,0,0,1,0,1"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0,0,1,0,0,1,0,1"))
(rule "inEqSimp_commuteLeq" (formula "20") (term "0,0,0,1,0,1"))
(rule "inEqSimp_sepPosMonomial0" (formula "20") (term "1,0,0,1,0,1"))
(rule "polySimp_mulComm0" (formula "20") (term "1,1,0,0,1,0,1"))
(rule "polySimp_rightDist" (formula "20") (term "1,1,0,0,1,0,1"))
(rule "polySimp_mulLiterals" (formula "20") (term "1,1,1,0,0,1,0,1"))
(rule "mul_literals" (formula "20") (term "0,1,1,0,0,1,0,1"))
(rule "polySimp_elimOne" (formula "20") (term "1,1,1,0,0,1,0,1"))
(rule "nnf_imp2or" (formula "20") (term "0,1"))
(rule "nnf_notAnd" (formula "20") (term "0,0,1"))
(rule "inEqSimp_notLeq" (formula "20") (term "1,0,0,1"))
(rule "polySimp_rightDist" (formula "20") (term "1,0,0,1,0,0,1"))
(rule "mul_literals" (formula "20") (term "0,1,0,0,1,0,0,1"))
(rule "polySimp_addAssoc" (formula "20") (term "0,0,1,0,0,1"))
(rule "add_literals" (formula "20") (term "0,0,0,1,0,0,1"))
(rule "add_zero_left" (formula "20") (term "0,0,1,0,0,1"))
(rule "inEqSimp_sepPosMonomial1" (formula "20") (term "1,0,0,1"))
(rule "polySimp_mulLiterals" (formula "20") (term "1,1,0,0,1"))
(rule "polySimp_elimOne" (formula "20") (term "1,1,0,0,1"))
(rule "inEqSimp_notGeq" (formula "20") (term "0,0,0,1"))
(rule "times_zero_1" (formula "20") (term "1,0,0,0,0,0,1"))
(rule "add_literals" (formula "20") (term "0,0,0,0,0,1"))
(rule "inEqSimp_sepPosMonomial0" (formula "20") (term "0,0,0,1"))
(rule "mul_literals" (formula "20") (term "1,0,0,0,1"))
(rule "ifthenelse_split" (formula "20") (term "0,0"))
(branch "result_0.length >= 0 TRUE"
(rule "eqSymm" (formula "21") (term "0"))
(rule "cut_direct" (formula "4") (term "0"))
(branch "CUT: org.hyperledger.fabric.shim.Chaincode.Response.Status.SUCCESS = null TRUE"
(builtin "One Step Simplification" (formula "5"))
(rule "true_left" (formula "5"))
(rule "cut_direct" (formula "5") (term "0,0"))
(branch "CUT: strPool(\"Yay\"). = TRUE TRUE"
(builtin "One Step Simplification" (formula "6"))
(rule "true_left" (formula "6"))
(rule "equalityToSeqGetAndSeqLenLeft" (formula "20") (inst "iv=iv"))
(rule "andLeft" (formula "20"))
(rule "lenOfSeqConcat" (formula "20") (term "1"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_addComm0" (formula "20") (term "1"))
(rule "inEqSimp_ltToLeq" (formula "21") (term "1,0,0"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,0,1,0,0"))
(rule "inEqSimp_commuteLeq" (formula "21") (term "0,0,0"))
(rule "applyEq" (formula "20") (term "0,0") (ifseqformula "22"))
(rule "lenOfSeqConcat" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_homoEq" (formula "20"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0"))
(rule "polySimp_addComm0" (formula "20") (term "1,1,0"))
(rule "polySimp_rightDist" (formula "20") (term "1,0"))
(rule "mul_literals" (formula "20") (term "0,1,0"))
(rule "polySimp_addAssoc" (formula "20") (term "0"))
(rule "polySimp_addComm1" (formula "20") (term "0,0"))
(rule "add_literals" (formula "20") (term "0,0,0"))
(rule "add_zero_left" (formula "20") (term "0,0"))
(rule "polySimp_pullOutFactor1" (formula "20") (term "0"))
(rule "add_literals" (formula "20") (term "1,0"))
(rule "times_zero_1" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "applyEq" (formula "20") (term "0,0,1,0,0,1,0,0") (ifseqformula "21"))
(rule "lenOfSeqConcat" (formula "20") (term "0,1,0,0,1,0,0"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0,0,1,0,0"))
(rule "polySimp_addComm0" (formula "20") (term "1,1,0,0,1,0,0"))
(rule "polySimp_rightDist" (formula "20") (term "1,0,0,1,0,0"))
(rule "mul_literals" (formula "20") (term "0,1,0,0,1,0,0"))
(rule "polySimp_addAssoc" (formula "20") (term "0,0,1,0,0"))
(rule "add_literals" (formula "20") (term "0,0,0,1,0,0"))
(rule "add_zero_left" (formula "20") (term "0,0,1,0,0"))
(rule "applyEq" (formula "20") (term "0,0,1,0") (ifseqformula "21"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "lenNonNegative" (formula "2") (term "0"))
(rule "inEqSimp_commuteLeq" (formula "2"))
(rule "applyEq" (formula "2") (term "0") (ifseqformula "3"))
(rule "qeq_literals" (formula "2"))
(rule "closeFalse" (formula "2"))
)
(branch "CUT: strPool(\"Yay\"). = TRUE FALSE"
(builtin "One Step Simplification" (formula "5"))
(rule "equalityToSeqGetAndSeqLenLeft" (formula "20") (inst "iv=iv"))
(rule "andLeft" (formula "20"))
(rule "lenOfSeqConcat" (formula "20") (term "1"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_addComm0" (formula "20") (term "1"))
(rule "inEqSimp_ltToLeq" (formula "21") (term "1,0,0"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,0,1,0,0"))
(rule "inEqSimp_commuteLeq" (formula "21") (term "0,0,0"))
(rule "applyEq" (formula "21") (term "0,0,1,0,0,1,0,0") (ifseqformula "22"))
(rule "lenOfSeqConcat" (formula "21") (term "0,1,0,0,1,0,0"))
(builtin "One Step Simplification" (formula "21"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,0,1,0,0"))
(rule "polySimp_addComm0" (formula "21") (term "1,1,0,0,1,0,0"))
(rule "polySimp_rightDist" (formula "21") (term "1,0,0,1,0,0"))
(rule "mul_literals" (formula "21") (term "0,1,0,0,1,0,0"))
(rule "polySimp_addAssoc" (formula "21") (term "0,0,1,0,0"))
(rule "add_literals" (formula "21") (term "0,0,0,1,0,0"))
(rule "add_zero_left" (formula "21") (term "0,0,1,0,0"))
(rule "applyEq" (formula "20") (term "0,0") (ifseqformula "22"))
(rule "lenOfSeqConcat" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_homoEq" (formula "20"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0"))
(rule "polySimp_addComm0" (formula "20") (term "1,1,0"))
(rule "polySimp_rightDist" (formula "20") (term "1,0"))
(rule "mul_literals" (formula "20") (term "0,1,0"))
(rule "polySimp_addAssoc" (formula "20") (term "0"))
(rule "polySimp_addComm1" (formula "20") (term "0,0"))
(rule "add_literals" (formula "20") (term "0,0,0"))
(rule "add_zero_left" (formula "20") (term "0,0"))
(rule "polySimp_pullOutFactor1" (formula "20") (term "0"))
(rule "add_literals" (formula "20") (term "1,0"))
(rule "times_zero_1" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "applyEq" (formula "20") (term "0,0,1,0") (ifseqformula "21"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "lenNonNegative" (formula "2") (term "0"))
(rule "inEqSimp_commuteLeq" (formula "2"))
(rule "applyEq" (formula "2") (term "0") (ifseqformula "3"))
(rule "qeq_literals" (formula "2"))
(rule "closeFalse" (formula "2"))
)
)
(branch "CUT: org.hyperledger.fabric.shim.Chaincode.Response.Status.SUCCESS = null FALSE"
(builtin "One Step Simplification" (formula "4"))
(rule "cut_direct" (formula "5") (term "0,0"))
(branch "CUT: strPool(\"Yay\"). = TRUE TRUE"
(builtin "One Step Simplification" (formula "6"))
(rule "true_left" (formula "6"))
(rule "equalityToSeqGetAndSeqLenLeft" (formula "20") (inst "iv=iv"))
(rule "andLeft" (formula "20"))
(rule "lenOfSeqConcat" (formula "20") (term "1"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_addComm0" (formula "20") (term "1"))
(rule "inEqSimp_ltToLeq" (formula "21") (term "1,0,0"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,0,1,0,0"))
(rule "inEqSimp_commuteLeq" (formula "21") (term "0,0,0"))
(rule "applyEq" (formula "21") (term "0,0,1,0,0,1,0,0") (ifseqformula "22"))
(rule "lenOfSeqConcat" (formula "21") (term "0,1,0,0,1,0,0"))
(builtin "One Step Simplification" (formula "21"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,0,1,0,0"))
(rule "polySimp_addComm0" (formula "21") (term "1,1,0,0,1,0,0"))
(rule "polySimp_rightDist" (formula "21") (term "1,0,0,1,0,0"))
(rule "mul_literals" (formula "21") (term "0,1,0,0,1,0,0"))
(rule "polySimp_addAssoc" (formula "21") (term "0,0,1,0,0"))
(rule "add_literals" (formula "21") (term "0,0,0,1,0,0"))
(rule "add_zero_left" (formula "21") (term "0,0,1,0,0"))
(rule "applyEq" (formula "20") (term "0,0") (ifseqformula "22"))
(rule "lenOfSeqConcat" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_homoEq" (formula "20"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0"))
(rule "polySimp_addComm0" (formula "20") (term "1,1,0"))
(rule "polySimp_rightDist" (formula "20") (term "1,0"))
(rule "mul_literals" (formula "20") (term "0,1,0"))
(rule "polySimp_addAssoc" (formula "20") (term "0"))
(rule "polySimp_addComm1" (formula "20") (term "0,0"))
(rule "add_literals" (formula "20") (term "0,0,0"))
(rule "add_zero_left" (formula "20") (term "0,0"))
(rule "polySimp_pullOutFactor1" (formula "20") (term "0"))
(rule "add_literals" (formula "20") (term "1,0"))
(rule "times_zero_1" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "applyEq" (formula "20") (term "0,0,1,0") (ifseqformula "21"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "lenNonNegative" (formula "2") (term "0"))
(rule "inEqSimp_commuteLeq" (formula "2"))
(rule "applyEq" (formula "2") (term "0") (ifseqformula "3"))
(rule "qeq_literals" (formula "2"))
(rule "closeFalse" (formula "2"))
)
(branch "CUT: strPool(\"Yay\"). = TRUE FALSE"
(builtin "One Step Simplification" (formula "5"))
(rule "equalityToSeqGetAndSeqLenLeft" (formula "20") (inst "iv=iv"))
(rule "andLeft" (formula "20"))
(rule "lenOfSeqConcat" (formula "20") (term "1"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_addComm0" (formula "20") (term "1"))
(rule "inEqSimp_ltToLeq" (formula "21") (term "1,0,0"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,0,1,0,0"))
(rule "inEqSimp_commuteLeq" (formula "21") (term "0,0,0"))
(rule "applyEq" (formula "20") (term "0,0") (ifseqformula "22"))
(rule "lenOfSeqConcat" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_homoEq" (formula "20"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0"))
(rule "polySimp_addComm0" (formula "20") (term "1,1,0"))
(rule "polySimp_rightDist" (formula "20") (term "1,0"))
(rule "mul_literals" (formula "20") (term "0,1,0"))
(rule "polySimp_addAssoc" (formula "20") (term "0"))
(rule "polySimp_addComm1" (formula "20") (term "0,0"))
(rule "add_literals" (formula "20") (term "0,0,0"))
(rule "add_zero_left" (formula "20") (term "0,0"))
(rule "polySimp_pullOutFactor1" (formula "20") (term "0"))
(rule "add_literals" (formula "20") (term "1,0"))
(rule "times_zero_1" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "applyEq" (formula "20") (term "0,0,1,0,0,1,0,0") (ifseqformula "21"))
(rule "lenOfSeqConcat" (formula "20") (term "0,1,0,0,1,0,0"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0,0,1,0,0"))
(rule "polySimp_addComm0" (formula "20") (term "1,1,0,0,1,0,0"))
(rule "polySimp_rightDist" (formula "20") (term "1,0,0,1,0,0"))
(rule "mul_literals" (formula "20") (term "0,1,0,0,1,0,0"))
(rule "polySimp_addAssoc" (formula "20") (term "0,0,1,0,0"))
(rule "add_literals" (formula "20") (term "0,0,0,1,0,0"))
(rule "add_zero_left" (formula "20") (term "0,0,1,0,0"))
(rule "applyEq" (formula "20") (term "0,0,1,0") (ifseqformula "21"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "lenNonNegative" (formula "2") (term "0"))
(rule "inEqSimp_commuteLeq" (formula "2"))
(rule "applyEq" (formula "2") (term "0") (ifseqformula "3"))
(rule "qeq_literals" (formula "2"))
(rule "closeFalse" (formula "2"))
)
)
)
(branch "result_0.length >= 0 FALSE"
(rule "eqSymm" (formula "21") (term "0"))
(rule "inEqSimp_geqRight" (formula "20"))
(rule "mul_literals" (formula "1") (term "1,0,0"))
(rule "add_literals" (formula "1") (term "0,0"))
(rule "inEqSimp_sepPosMonomial0" (formula "1"))
(rule "mul_literals" (formula "1") (term "1"))
(rule "cut_direct" (formula "4") (term "0"))
(branch "CUT: org.hyperledger.fabric.shim.Chaincode.Response.Status.SUCCESS = null TRUE"
(builtin "One Step Simplification" (formula "5"))
(rule "true_left" (formula "5"))
(rule "cut_direct" (formula "5") (term "0,0"))
(branch "CUT: strPool(\"Yay\"). = TRUE TRUE"
(builtin "One Step Simplification" (formula "6"))
(rule "true_left" (formula "6"))
(rule "equalityToSeqGetAndSeqLenLeft" (formula "20") (inst "iv=iv"))
(rule "andLeft" (formula "20"))
(rule "lenOfSeqConcat" (formula "20") (term "1"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_addComm0" (formula "20") (term "1"))
(rule "inEqSimp_ltToLeq" (formula "21") (term "1,0,0"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,0,1,0,0"))
(rule "inEqSimp_commuteLeq" (formula "21") (term "0,0,0"))
(rule "applyEq" (formula "21") (term "0,0,1,0,0,1,0,0") (ifseqformula "22"))
(rule "lenOfSeqConcat" (formula "21") (term "0,1,0,0,1,0,0"))
(builtin "One Step Simplification" (formula "21"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,0,1,0,0"))
(rule "polySimp_addComm0" (formula "21") (term "1,1,0,0,1,0,0"))
(rule "polySimp_rightDist" (formula "21") (term "1,0,0,1,0,0"))
(rule "mul_literals" (formula "21") (term "0,1,0,0,1,0,0"))
(rule "polySimp_addAssoc" (formula "21") (term "0,0,1,0,0"))
(rule "add_literals" (formula "21") (term "0,0,0,1,0,0"))
(rule "add_zero_left" (formula "21") (term "0,0,1,0,0"))
(rule "applyEq" (formula "20") (term "0,0") (ifseqformula "22"))
(rule "lenOfSeqConcat" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_homoEq" (formula "20"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0"))
(rule "polySimp_addComm0" (formula "20") (term "1,1,0"))
(rule "polySimp_rightDist" (formula "20") (term "1,0"))
(rule "mul_literals" (formula "20") (term "0,1,0"))
(rule "polySimp_addAssoc" (formula "20") (term "0"))
(rule "polySimp_addComm1" (formula "20") (term "0,0"))
(rule "add_literals" (formula "20") (term "0,0,0"))
(rule "add_zero_left" (formula "20") (term "0,0"))
(rule "polySimp_pullOutFactor1" (formula "20") (term "0"))
(rule "add_literals" (formula "20") (term "1,0"))
(rule "times_zero_1" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "applyEq" (formula "20") (term "0,0,1,0") (ifseqformula "21"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "lenNonNegative" (formula "2") (term "0"))
(rule "inEqSimp_commuteLeq" (formula "2"))
(rule "applyEq" (formula "2") (term "0") (ifseqformula "3"))
(rule "qeq_literals" (formula "2"))
(rule "closeFalse" (formula "2"))
)
(branch "CUT: strPool(\"Yay\"). = TRUE FALSE"
(builtin "One Step Simplification" (formula "5"))
(rule "equalityToSeqGetAndSeqLenLeft" (formula "20") (inst "iv=iv"))
(rule "andLeft" (formula "20"))
(rule "lenOfSeqConcat" (formula "20") (term "1"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_addComm0" (formula "20") (term "1"))
(rule "inEqSimp_ltToLeq" (formula "21") (term "1,0,0"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,0,1,0,0"))
(rule "inEqSimp_commuteLeq" (formula "21") (term "0,0,0"))
(rule "applyEq" (formula "21") (term "0,0,1,0,0,1,0,0") (ifseqformula "22"))
(rule "lenOfSeqConcat" (formula "21") (term "0,1,0,0,1,0,0"))
(builtin "One Step Simplification" (formula "21"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,0,1,0,0"))
(rule "polySimp_addComm0" (formula "21") (term "1,1,0,0,1,0,0"))
(rule "polySimp_rightDist" (formula "21") (term "1,0,0,1,0,0"))
(rule "mul_literals" (formula "21") (term "0,1,0,0,1,0,0"))
(rule "polySimp_addAssoc" (formula "21") (term "0,0,1,0,0"))
(rule "add_literals" (formula "21") (term "0,0,0,1,0,0"))
(rule "add_zero_left" (formula "21") (term "0,0,1,0,0"))
(rule "applyEq" (formula "20") (term "0,0") (ifseqformula "22"))
(rule "lenOfSeqConcat" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_homoEq" (formula "20"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0"))
(rule "polySimp_addComm0" (formula "20") (term "1,1,0"))
(rule "polySimp_rightDist" (formula "20") (term "1,0"))
(rule "mul_literals" (formula "20") (term "0,1,0"))
(rule "polySimp_addAssoc" (formula "20") (term "0"))
(rule "polySimp_addComm1" (formula "20") (term "0,0"))
(rule "add_literals" (formula "20") (term "0,0,0"))
(rule "add_zero_left" (formula "20") (term "0,0"))
(rule "polySimp_pullOutFactor1" (formula "20") (term "0"))
(rule "add_literals" (formula "20") (term "1,0"))
(rule "times_zero_1" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "applyEq" (formula "20") (term "0,0,1,0") (ifseqformula "21"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "lenNonNegative" (formula "2") (term "0"))
(rule "inEqSimp_commuteLeq" (formula "2"))
(rule "applyEq" (formula "2") (term "0") (ifseqformula "3"))
(rule "qeq_literals" (formula "2"))
(rule "closeFalse" (formula "2"))
)
)
(branch "CUT: org.hyperledger.fabric.shim.Chaincode.Response.Status.SUCCESS = null FALSE"
(builtin "One Step Simplification" (formula "4"))
(rule "cut_direct" (formula "5") (term "0,0"))
(branch "CUT: strPool(\"Yay\"). = TRUE TRUE"
(builtin "One Step Simplification" (formula "6"))
(rule "true_left" (formula "6"))
(rule "equalityToSeqGetAndSeqLenLeft" (formula "20") (inst "iv=iv"))
(rule "andLeft" (formula "20"))
(rule "lenOfSeqConcat" (formula "20") (term "1"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_addComm0" (formula "20") (term "1"))
(rule "inEqSimp_ltToLeq" (formula "21") (term "1,0,0"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,0,1,0,0"))
(rule "inEqSimp_commuteLeq" (formula "21") (term "0,0,0"))
(rule "applyEq" (formula "21") (term "0,0,1,0,0,1,0,0") (ifseqformula "22"))
(rule "lenOfSeqConcat" (formula "21") (term "0,1,0,0,1,0,0"))
(builtin "One Step Simplification" (formula "21"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,0,1,0,0"))
(rule "polySimp_addComm0" (formula "21") (term "1,1,0,0,1,0,0"))
(rule "polySimp_rightDist" (formula "21") (term "1,0,0,1,0,0"))
(rule "mul_literals" (formula "21") (term "0,1,0,0,1,0,0"))
(rule "polySimp_addAssoc" (formula "21") (term "0,0,1,0,0"))
(rule "add_literals" (formula "21") (term "0,0,0,1,0,0"))
(rule "add_zero_left" (formula "21") (term "0,0,1,0,0"))
(rule "applyEq" (formula "20") (term "0,0") (ifseqformula "22"))
(rule "lenOfSeqConcat" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_homoEq" (formula "20"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0"))
(rule "polySimp_addComm0" (formula "20") (term "1,1,0"))
(rule "polySimp_rightDist" (formula "20") (term "1,0"))
(rule "mul_literals" (formula "20") (term "0,1,0"))
(rule "polySimp_addAssoc" (formula "20") (term "0"))
(rule "polySimp_addComm1" (formula "20") (term "0,0"))
(rule "add_literals" (formula "20") (term "0,0,0"))
(rule "add_zero_left" (formula "20") (term "0,0"))
(rule "polySimp_pullOutFactor1" (formula "20") (term "0"))
(rule "add_literals" (formula "20") (term "1,0"))
(rule "times_zero_1" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "applyEq" (formula "20") (term "0,0,1,0") (ifseqformula "21"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "lenNonNegative" (formula "2") (term "0"))
(rule "inEqSimp_commuteLeq" (formula "2"))
(rule "applyEq" (formula "2") (term "0") (ifseqformula "3"))
(rule "qeq_literals" (formula "2"))
(rule "closeFalse" (formula "2"))
)
(branch "CUT: strPool(\"Yay\"). = TRUE FALSE"
(builtin "One Step Simplification" (formula "5"))
(rule "equalityToSeqGetAndSeqLenLeft" (formula "20") (inst "iv=iv"))
(rule "andLeft" (formula "20"))
(rule "lenOfSeqConcat" (formula "20") (term "1"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_addComm0" (formula "20") (term "1"))
(rule "inEqSimp_ltToLeq" (formula "21") (term "1,0,0"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,0,1,0,0"))
(rule "inEqSimp_commuteLeq" (formula "21") (term "0,0,0"))
(rule "applyEq" (formula "20") (term "0,0") (ifseqformula "22"))
(rule "lenOfSeqConcat" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_homoEq" (formula "20"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0"))
(rule "polySimp_addComm0" (formula "20") (term "1,1,0"))
(rule "polySimp_rightDist" (formula "20") (term "1,0"))
(rule "mul_literals" (formula "20") (term "0,1,0"))
(rule "polySimp_addAssoc" (formula "20") (term "0"))
(rule "polySimp_addComm1" (formula "20") (term "0,0"))
(rule "add_literals" (formula "20") (term "0,0,0"))
(rule "add_zero_left" (formula "20") (term "0,0"))
(rule "polySimp_pullOutFactor1" (formula "20") (term "0"))
(rule "add_literals" (formula "20") (term "1,0"))
(rule "times_zero_1" (formula "20") (term "0"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "applyEq" (formula "20") (term "0,0,1,0") (ifseqformula "21"))
(builtin "One Step Simplification" (formula "20"))
(rule "true_left" (formula "20"))
(rule "lenNonNegative" (formula "2") (term "0"))
(rule "inEqSimp_commuteLeq" (formula "2"))
(rule "applyEq" (formula "2") (term "0") (ifseqformula "3"))
(rule "qeq_literals" (formula "2"))
(rule "closeFalse" (formula "2"))
)
)
)
)
(branch " stub.transactionLog@anon_heap_putState<>.length = 0 FALSE"
(rule "eqSymm" (formula "21") (term "0,0,0,0"))
(rule "polySimp_elimSub" (formula "21") (term "2,0,2,0,0,0"))
(rule "mul_literals" (formula "21") (term "1,2,0,2,0,0,0"))
(rule "polySimp_elimSub" (formula "21") (term "1,1,0,0,0"))
(rule "mul_literals" (formula "21") (term "1,1,1,0,0,0"))
(rule "polySimp_elimSub" (formula "21") (term "1,0,0,0,0,0,0"))
(rule "mul_literals" (formula "21") (term "1,1,0,0,0,0,0,0"))
(rule "polySimp_addComm0" (formula "21") (term "2,0,2,0,0,0"))
(rule "polySimp_addComm0" (formula "21") (term "1,1,0,0,0"))
(rule "polySimp_addComm0" (formula "21") (term "1,0,0,0,0,0,0"))
(rule "elementOfSingleton" (formula "1") (term "0"))
(builtin "One Step Simplification" (formula "1"))
(rule "true_left" (formula "1"))
(rule "applyEq" (formula "20") (term "0,1,1,1,0,0,0") (ifseqformula "18"))
(rule "lenOfSeqConcat" (formula "20") (term "1,1,1,0,0,0"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_addComm0" (formula "20") (term "1,1,1,0,0,0"))
(rule "polySimp_addAssoc" (formula "20") (term "1,1,0,0,0"))
(rule "add_literals" (formula "20") (term "0,1,1,0,0,0"))
(rule "add_zero_left" (formula "20") (term "1,1,0,0,0"))
(rule "applyEq" (formula "12") (term "0") (ifseqformula "13"))
(rule "eqSymm" (formula "12"))
(rule "applyEq" (formula "19") (term "0,0") (ifseqformula "18"))
(rule "lenOfSeqConcat" (formula "19") (term "0"))
(builtin "One Step Simplification" (formula "19"))
(rule "polySimp_addComm0" (formula "19") (term "0"))
(rule "applyEq" (formula "18") (term "1,0,1,1") (ifseqformula "12"))
(rule "applyEq" (formula "20") (term "1") (ifseqformula "12"))
(rule "applyEq" (formula "20") (term "0,0,2,0,0,0") (ifseqformula "18"))
(rule "applyEq" (formula "20") (term "0,1,1,0,0,0,0,0,0") (ifseqformula "18"))
(rule "lenOfSeqConcat" (formula "20") (term "1,1,0,0,0,0,0,0"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_addComm0" (formula "20") (term "1,1,0,0,0,0,0,0"))
(rule "polySimp_addAssoc" (formula "20") (term "1,0,0,0,0,0,0"))
(rule "add_literals" (formula "20") (term "0,1,0,0,0,0,0,0"))
(rule "add_zero_left" (formula "20") (term "1,0,0,0,0,0,0"))
(rule "applyEq" (formula "20") (term "0,0,0,0,0,0,0") (ifseqformula "18"))
(rule "applyEq" (formula "20") (term "0,1,0,0,0") (ifseqformula "18"))
(rule "applyEq" (formula "20") (term "0,1,2,0,2,0,0,0") (ifseqformula "18"))
(rule "lenOfSeqConcat" (formula "20") (term "1,2,0,2,0,0,0"))
(builtin "One Step Simplification" (formula "20"))
(rule "polySimp_addComm0" (formula "20") (term "1,2,0,2,0,0,0"))
(rule "polySimp_addAssoc" (formula "20") (term "2,0,2,0,0,0"))
(rule "add_literals" (formula "20") (term "0,2,0,2,0,0,0"))
(rule "add_zero_left" (formula "20") (term "2,0,2,0,0,0"))
(rule "polySimp_sepPosMonomial" (formula "19"))
(rule "mul_literals" (formula "19") (term "1"))
(rule "array2seqDef" (formula "13") (term "0") (inst "u=u"))
(rule "array2seqDef" (formula "12") (term "0") (inst "u=u"))
(rule "getOfSeqConcat" (formula "20") (term "0,0,0,0,0,0"))
(rule "polySimp_elimSub" (formula "20") (term "1,2,0,0,0,0,0,0"))
(rule "polySimp_pullOutFactor1" (formula "20") (term "1,2,0,0,0,0,0,0"))
(rule "add_literals" (formula "20") (term "1,1,2,0,0,0,0,0,0"))
(rule "times_zero_1" (formula "20") (term "1,2,0,0,0,0,0,0"))
(builtin "One Step Simplification" (formula "20"))
(rule "castDel" (formula "20") (term "2,0,0,0,0,0,0"))
(rule "inEqSimp_ltToLeq" (formula "20") (term "0,0,0,0,0,0,0"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0,0,0,0,0,0,0,0,0"))
(rule "polySimp_pullOutFactor2b" (formula "20") (term "0,0,0,0,0,0,0,0"))
(rule "add_literals" (formula "20") (term "1,1,0,0,0,0,0,0,0,0"))
(rule "times_zero_1" (formula "20") (term "1,0,0,0,0,0,0,0,0"))
(rule "add_literals" (formula "20") (term "0,0,0,0,0,0,0,0"))
(rule "leq_literals" (formula "20") (term "0,0,0,0,0,0,0"))
(builtin "One Step Simplification" (formula "20"))
(rule "keyOfNewEntry" (formula "20") (term "0,0,0,0,0"))
(builtin "One Step Simplification" (formula "20"))
(rule "equalityToSeqGetAndSeqLenRight" (formula "20") (inst "iv=iv"))
(rule "lenOfSeqDefEQ" (formula "20") (term "1,0") (ifseqformula "12"))
(rule "eqSymm" (formula "20") (term "0"))
(rule "polySimp_elimSub" (formula "20") (term "1,0,0"))
(rule "times_zero_2" (formula "20") (term "1,1,0,0"))
(rule "add_zero_right" (formula "20") (term "1,0,0"))
(rule "inEqSimp_ltToLeq" (formula "20") (term "1,0,0,1"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0,0,1,0,0,1"))
(rule "inEqSimp_commuteLeq" (formula "20") (term "0,0,0,1"))
(rule "inEqSimp_commuteLeq" (formula "20") (term "0,0,0"))
(rule "inEqSimp_sepPosMonomial0" (formula "20") (term "1,0,0,1"))
(rule "polySimp_mulComm0" (formula "20") (term "1,1,0,0,1"))
(rule "polySimp_rightDist" (formula "20") (term "1,1,0,0,1"))
(rule "polySimp_mulLiterals" (formula "20") (term "1,1,1,0,0,1"))
(rule "mul_literals" (formula "20") (term "0,1,1,0,0,1"))
(rule "polySimp_elimOne" (formula "20") (term "1,1,1,0,0,1"))
(rule "getOfSeqConcat" (formula "20") (term "0,0,0,0,1,0,1"))
(rule "polySimp_elimSub" (formula "20") (term "1,2,0,0,0,0,1,0,1"))
(rule "polySimp_pullOutFactor1" (formula "20") (term "1,2,0,0,0,0,1,0,1"))
(rule "add_literals" (formula "20") (term "1,1,2,0,0,0,0,1,0,1"))
(rule "times_zero_1" (formula "20") (term "1,2,0,0,0,0,1,0,1"))
(builtin "One Step Simplification" (formula "20"))
(rule "castDel" (formula "20") (term "2,0,0,0,0,1,0,1"))
(rule "inEqSimp_ltToLeq" (formula "20") (term "0,0,0,0,0,1,0,1"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0,0,0,0,0,0,0,1,0,1"))
(rule "polySimp_pullOutFactor2b" (formula "20") (term "0,0,0,0,0,0,1,0,1"))
(rule "add_literals" (formula "20") (term "1,1,0,0,0,0,0,0,1,0,1"))
(rule "times_zero_1" (formula "20") (term "1,0,0,0,0,0,0,1,0,1"))
(rule "add_literals" (formula "20") (term "0,0,0,0,0,0,1,0,1"))
(rule "leq_literals" (formula "20") (term "0,0,0,0,0,1,0,1"))
(builtin "One Step Simplification" (formula "20"))
(rule "valueOfNewEntry" (formula "20") (term "0,0,0,1,0,1"))
(rule "castDel" (formula "20") (term "0,0,1,0,1"))
(builtin "One Step Simplification" (formula "20"))
(rule "getOfSeqConcat" (formula "20") (term "0,0,0,1"))
(rule "eqSymm" (formula "20"))
(rule "polySimp_elimSub" (formula "20") (term "1,2,0,0,0,0"))
(rule "polySimp_pullOutFactor1" (formula "20") (term "1,2,0,0,0,0"))
(rule "add_literals" (formula "20") (term "1,1,2,0,0,0,0"))
(rule "times_zero_1" (formula "20") (term "1,2,0,0,0,0"))
(builtin "One Step Simplification" (formula "20"))
(rule "castDel" (formula "20") (term "2,0,0,0,0"))
(rule "inEqSimp_ltToLeq" (formula "20") (term "0,0,0,0,0"))
(rule "polySimp_mulComm0" (formula "20") (term "1,0,0,0,0,0,0,0"))
(rule "polySimp_pullOutFactor2b" (formula "20") (term "0,0,0,0,0,0"))
(rule "add_literals" (formula "20") (term "1,1,0,0,0,0,0,0"))
(rule "times_zero_1" (formula "20") (term "1,0,0,0,0,0,0"))
(rule "add_zero_right" (formula "20") (term "0,0,0,0,0,0"))
(rule "leq_literals" (formula "20") (term "0,0,0,0,0"))
(builtin "One Step Simplification" (formula "20"))
(rule "eqSymm" (formula "20"))
(rule "valueOfNewEntry" (formula "20") (term "0,0,1"))
(rule "castDel" (formula "20") (term "0,1"))
(rule "lenOfSeqDefEQ" (formula "20") (term "1") (ifseqformula "13"))
(rule "eqSymm" (formula "20"))
(rule "polySimp_elimSub" (formula "20") (term "1,0"))
(rule "times_zero_2" (formula "20") (term "1,1,0"))
(rule "add_zero_right" (formula "20") (term "1,0"))
(rule "inEqSimp_commuteLeq" (formula "20") (term "0,0"))
(builtin "One Step Simplification" (formula "20"))
(rule "closeTrue" (formula "20"))
)
)
)
(branch "Assume array2seq(heapAfter_serialize, result_0) != array2seq(heapAfter_putState, result_0)"
(rule "notLeft" (formula "13"))
(rule "elementOfSingleton" (formula "1") (term "0"))
(builtin "One Step Simplification" (formula "1"))
(rule "true_left" (formula "1"))
(rule "applyEq" (formula "18") (term "0") (ifseqformula "12"))
(rule "eqSymm" (formula "18"))
(rule "applyEq" (formula "30") (term "0,0,0,0,0,0") (ifseqformula "17"))
(rule "array2seqDef" (formula "17") (term "1,0,1,1") (inst "u=u"))
(rule "eqSymm" (formula "17"))
(rule "array2seqDef" (formula "12") (term "0") (inst "u=u"))
(rule "equalityToSeqGetAndSeqLenRight" (formula "18") (inst "iv=iv"))
(rule "lenOfSeqDefEQ" (formula "18") (term "1,0") (ifseqformula "12"))
(rule "eqSymm" (formula "18") (term "0"))
(rule "polySimp_elimSub" (formula "18") (term "1,0,0"))
(rule "times_zero_2" (formula "18") (term "1,1,0,0"))
(rule "add_zero_right" (formula "18") (term "1,0,0"))
(rule "inEqSimp_ltToLeq" (formula "18") (term "1,0,0,1"))
(rule "polySimp_mulComm0" (formula "18") (term "1,0,0,1,0,0,1"))
(rule "inEqSimp_commuteLeq" (formula "18") (term "0,0,0,1"))
(rule "inEqSimp_commuteLeq" (formula "18") (term "0,0,0"))
(rule "inEqSimp_sepPosMonomial0" (formula "18") (term "1,0,0,1"))
(rule "polySimp_mulComm0" (formula "18") (term "1,1,0,0,1"))
(rule "polySimp_rightDist" (formula "18") (term "1,1,0,0,1"))
(rule "mul_literals" (formula "18") (term "0,1,1,0,0,1"))
(rule "polySimp_mulLiterals" (formula "18") (term "1,1,1,0,0,1"))
(rule "polySimp_elimOne" (formula "18") (term "1,1,1,0,0,1"))
(rule "array2seqDef" (formula "30") (term "1,0,1,0,0,0,0,0,0") (inst "u=u"))
(rule "array2seqDef" (formula "18") (term "0,0,1,0,1") (inst "u=u"))
(rule "getOfSeqDef" (formula "18") (term "0,1,0,1"))
(rule "castDel" (formula "18") (term "2,0,1,0,1"))
(rule "castDel" (formula "18") (term "1,0,1,0,1"))
(rule "add_zero_right" (formula "18") (term "0,2,1,0,1,0,1"))
(rule "polySimp_elimSub" (formula "18") (term "1,1,0,0,1,0,1"))
(rule "times_zero_2" (formula "18") (term "1,1,1,0,0,1,0,1"))
(rule "add_zero_right" (formula "18") (term "1,1,0,0,1,0,1"))
(rule "inEqSimp_ltToLeq" (formula "18") (term "1,0,0,1,0,1"))
(rule "polySimp_mulComm0" (formula "18") (term "1,0,0,1,0,0,1,0,1"))
(rule "inEqSimp_commuteLeq" (formula "18") (term "0,0,0,1,0,1"))
(rule "inEqSimp_sepPosMonomial0" (formula "18") (term "1,0,0,1,0,1"))
(rule "polySimp_mulComm0" (formula "18") (term "1,1,0,0,1,0,1"))
(rule "polySimp_rightDist" (formula "18") (term "1,1,0,0,1,0,1"))
(rule "polySimp_mulLiterals" (formula "18") (term "1,1,1,0,0,1,0,1"))
(rule "mul_literals" (formula "18") (term "0,1,1,0,0,1,0,1"))
(rule "polySimp_elimOne" (formula "18") (term "1,1,1,0,0,1,0,1"))
(rule "array2seqDef" (formula "18") (term "0,1,0") (inst "u=u"))
(rule "eqSymm" (formula "18") (term "0"))
(rule "lenOfSeqDef" (formula "18") (term "0,0"))
(rule "polySimp_elimSub" (formula "18") (term "1,0,0"))
(rule "times_zero_2" (formula "18") (term "1,1,0,0"))
(rule "add_zero_right" (formula "18") (term "1,0,0"))
(rule "inEqSimp_ltToLeq" (formula "18") (term "0,0,0"))
(rule "add_zero_right" (formula "18") (term "0,0,0,0"))
(rule "polySimp_mulComm0" (formula "18") (term "1,0,0,0,0"))
(rule "inEqSimp_sepNegMonomial0" (formula "18") (term "0,0,0"))
(rule "polySimp_mulLiterals" (formula "18") (term "0,0,0,0"))
(rule "polySimp_elimOne" (formula "18") (term "0,0,0,0"))
(rule "array2seqDef" (formula "18") (term "0,1,1,1,0,0,1") (inst "u=u"))
(rule "lenOfSeqDef" (formula "18") (term "1,1,1,0,0,1"))
(rule "polySimp_elimSub" (formula "18") (term "1,1,1,1,0,0,1"))
(rule "times_zero_2" (formula "18") (term "1,1,1,1,1,0,0,1"))
(rule "add_zero_right" (formula "18") (term "1,1,1,1,0,0,1"))
(rule "inEqSimp_ltToLeq" (formula "18") (term "0,1,1,1,0,0,1"))
(rule "add_zero_right" (formula "18") (term "0,0,1,1,1,0,0,1"))
(rule "polySimp_mulComm0" (formula "18") (term "1,0,0,1,1,1,0,0,1"))
(rule "inEqSimp_sepNegMonomial0" (formula "18") (term "0,1,1,1,0,0,1"))
(rule "polySimp_mulLiterals" (formula "18") (term "0,0,1,1,1,0,0,1"))
(rule "polySimp_elimOne" (formula "18") (term "0,0,1,1,1,0,0,1"))
(rule "getOfSeqDefEQ" (formula "18") (term "1,1,0,1") (ifseqformula "12"))
(rule "castDel" (formula "18") (term "1,1,1,0,1"))
(rule "castDel" (formula "18") (term "2,1,1,0,1"))
(rule "add_zero_right" (formula "18") (term "0,2,1,1,1,0,1"))
(rule "eqSymm" (formula "18") (term "1,0,1"))
(rule "polySimp_elimSub" (formula "18") (term "1,1,0,0,1,0,1"))
(rule "times_zero_2" (formula "18") (term "1,1,1,0,0,1,0,1"))
(rule "add_zero_right" (formula "18") (term "1,1,0,0,1,0,1"))
(rule "inEqSimp_ltToLeq" (formula "18") (term "1,0,0,1,0,1"))
(rule "polySimp_mulComm0" (formula "18") (term "1,0,0,1,0,0,1,0,1"))
(rule "inEqSimp_commuteLeq" (formula "18") (term "0,0,0,1,0,1"))
(rule "inEqSimp_sepPosMonomial0" (formula "18") (term "1,0,0,1,0,1"))
(rule "polySimp_mulComm0" (formula "18") (term "1,1,0,0,1,0,1"))
(rule "polySimp_rightDist" (formula "18") (term "1,1,0,0,1,0,1"))
(rule "polySimp_mulLiterals" (formula "18") (term "1,1,1,0,0,1,0,1"))
(rule "mul_literals" (formula "18") (term "0,1,1,0,0,1,0,1"))
(rule "polySimp_elimOne" (formula "18") (term "1,1,1,0,0,1,0,1"))
(rule "nnf_imp2or" (formula "18") (term "0,1"))
(rule "nnf_notAnd" (formula "18") (term "0,0,1"))
(rule "inEqSimp_notGeq" (formula "18") (term "0,0,0,1"))
(rule "mul_literals" (formula "18") (term "1,0,0,0,0,0,1"))
(rule "add_literals" (formula "18") (term "0,0,0,0,0,1"))
(rule "inEqSimp_sepPosMonomial0" (formula "18") (term "0,0,0,1"))
(rule "mul_literals" (formula "18") (term "1,0,0,0,1"))
(rule "inEqSimp_notLeq" (formula "18") (term "1,0,0,1"))
(rule "polySimp_rightDist" (formula "18") (term "1,0,0,1,0,0,1"))
(rule "mul_literals" (formula "18") (term "0,1,0,0,1,0,0,1"))
(rule "polySimp_addAssoc" (formula "18") (term "0,0,1,0,0,1"))
(rule "add_literals" (formula "18") (term "0,0,0,1,0,0,1"))
(rule "add_zero_left" (formula "18") (term "0,0,1,0,0,1"))
(rule "inEqSimp_sepPosMonomial1" (formula "18") (term "1,0,0,1"))
(rule "polySimp_mulLiterals" (formula "18") (term "1,1,0,0,1"))
(rule "polySimp_elimOne" (formula "18") (term "1,1,0,0,1"))
(rule "ifthenelse_split" (formula "18") (term "1,0"))
(branch "result_0.length >= 0 TRUE"
(builtin "One Step Simplification" (formula "19"))
(rule "eqSymm" (formula "19") (term "1,0"))
(rule "commute_or" (formula "19") (term "0"))
(rule "inEqSimp_or_weaken1" (formula "19") (term "0"))
(rule "add_zero_right" (formula "19") (term "1,0,0"))
(builtin "One Step Simplification" (formula "19") (ifInst "" (formula "1")))
(rule "allRight" (formula "19") (inst "sk=iv_0"))
(rule "orRight" (formula "19"))
(rule "orRight" (formula "19"))
(rule "inEqSimp_leqRight" (formula "19"))
(rule "mul_literals" (formula "1") (term "1,0,0"))
(rule "add_literals" (formula "1") (term "0,0"))
(rule "add_zero_left" (formula "1") (term "0"))
(rule "replace_known_left" (formula "21") (term "0,0,0") (ifseqformula "1"))
(builtin "One Step Simplification" (formula "21") (ifInst "" (formula "1")))
(rule "inEqSimp_geqRight" (formula "20"))
(rule "polySimp_mulComm0" (formula "1") (term "1,0,0"))
(rule "polySimp_addComm1" (formula "1") (term "0"))
(rule "inEqSimp_homoInEq0" (formula "21") (term "0,0"))
(rule "eqSymm" (formula "21"))
(rule "polySimp_addComm1" (formula "21") (term "0,0,1"))
(rule "inEqSimp_homoInEq0" (formula "21") (term "0,0"))
(rule "polySimp_addComm1" (formula "21") (term "0,0,0"))
(rule "eqSymm" (formula "21"))
(rule "inEqSimp_sepNegMonomial0" (formula "1"))
(rule "polySimp_mulLiterals" (formula "1") (term "0"))
(rule "polySimp_elimOne" (formula "1") (term "0"))
(rule "inEqSimp_sepPosMonomial1" (formula "21") (term "0,0"))
(rule "eqSymm" (formula "21"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,1"))
(rule "polySimp_rightDist" (formula "21") (term "1,0,1"))
(rule "mul_literals" (formula "21") (term "0,1,0,1"))
(rule "polySimp_mulLiterals" (formula "21") (term "1,1,0,1"))
(rule "polySimp_elimOne" (formula "21") (term "1,1,0,1"))
(rule "inEqSimp_sepPosMonomial1" (formula "21") (term "0,0"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,0"))
(rule "polySimp_rightDist" (formula "21") (term "1,0,0"))
(rule "mul_literals" (formula "21") (term "0,1,0,0"))
(rule "polySimp_mulLiterals" (formula "21") (term "1,1,0,0"))
(rule "polySimp_elimOne" (formula "21") (term "1,1,0,0"))
(rule "eqSymm" (formula "21"))
(rule "pullOutSelect" (formula "21") (term "1,1") (inst "selectSK=arr_0"))
(rule "simplifySelectOfAnonEQ" (formula "1") (ifseqformula "19"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "28")))
(rule "selectCreatedOfAnonAsFormulaEQ" (formula "1") (term "0,1,0,0") (ifseqformula "14"))
(rule "replace_known_left" (formula "1") (term "1,0,1,0,0") (ifseqformula "15"))
(builtin "One Step Simplification" (formula "1"))
(rule "elementOfSingleton" (formula "1") (term "0,0"))
(builtin "One Step Simplification" (formula "1"))
(rule "applyEq" (formula "22") (term "1,0") (ifseqformula "1"))
(builtin "One Step Simplification" (formula "22"))
(rule "closeTrue" (formula "22"))
)
(branch "result_0.length >= 0 FALSE"
(builtin "One Step Simplification" (formula "19"))
(rule "inEqSimp_geqRight" (formula "18"))
(rule "times_zero_1" (formula "1") (term "1,0,0"))
(rule "add_literals" (formula "1") (term "0,0"))
(rule "inEqSimp_sepPosMonomial0" (formula "1"))
(rule "mul_literals" (formula "1") (term "1"))
(rule "inEqSimp_contradEq3" (formula "19") (term "1,0") (ifseqformula "1"))
(rule "times_zero_1" (formula "19") (term "1,0,0,1,0"))
(rule "add_zero_right" (formula "19") (term "0,0,1,0"))
(rule "qeq_literals" (formula "19") (term "0,1,0"))
(builtin "One Step Simplification" (formula "19"))
(rule "inEqSimp_contradInEq0" (formula "19") (term "0,0") (ifseqformula "1"))
(rule "qeq_literals" (formula "19") (term "0,0,0"))
(builtin "One Step Simplification" (formula "19"))
(rule "allRight" (formula "19") (inst "sk=iv_0"))
(rule "orRight" (formula "19"))
(rule "orRight" (formula "19"))
(rule "inEqSimp_geqRight" (formula "20"))
(rule "polySimp_mulComm0" (formula "1") (term "1,0,0"))
(rule "polySimp_addComm1" (formula "1") (term "0"))
(rule "inEqSimp_leqRight" (formula "20"))
(rule "mul_literals" (formula "1") (term "1,0,0"))
(rule "add_literals" (formula "1") (term "0,0"))
(rule "add_zero_left" (formula "1") (term "0"))
(rule "replace_known_left" (formula "21") (term "0,0,0") (ifseqformula "1"))
(builtin "One Step Simplification" (formula "21") (ifInst "" (formula "1")))
(rule "inEqSimp_homoInEq0" (formula "21") (term "0,0"))
(rule "eqSymm" (formula "21"))
(rule "polySimp_addComm1" (formula "21") (term "0,0,1"))
(rule "inEqSimp_homoInEq0" (formula "21") (term "0,0"))
(rule "polySimp_addComm1" (formula "21") (term "0,0,0"))
(rule "eqSymm" (formula "21"))
(rule "inEqSimp_sepNegMonomial0" (formula "2"))
(rule "polySimp_mulLiterals" (formula "2") (term "0"))
(rule "polySimp_elimOne" (formula "2") (term "0"))
(rule "inEqSimp_sepPosMonomial1" (formula "21") (term "0,0"))
(rule "eqSymm" (formula "21"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,1"))
(rule "polySimp_rightDist" (formula "21") (term "1,0,1"))
(rule "mul_literals" (formula "21") (term "0,1,0,1"))
(rule "polySimp_mulLiterals" (formula "21") (term "1,1,0,1"))
(rule "polySimp_elimOne" (formula "21") (term "1,1,0,1"))
(rule "inEqSimp_sepPosMonomial1" (formula "21") (term "0,0"))
(rule "polySimp_mulComm0" (formula "21") (term "1,0,0"))
(rule "polySimp_rightDist" (formula "21") (term "1,0,0"))
(rule "mul_literals" (formula "21") (term "0,1,0,0"))
(rule "polySimp_mulLiterals" (formula "21") (term "1,1,0,0"))
(rule "polySimp_elimOne" (formula "21") (term "1,1,0,0"))
(rule "eqSymm" (formula "21"))
(rule "inEqSimp_contradInEq0" (formula "2") (term "0,0") (ifseqformula "3"))
(rule "qeq_literals" (formula "2") (term "0,0,0"))
(builtin "One Step Simplification" (formula "2"))
(rule "inEqSimp_homoInEq1" (formula "2"))
(rule "times_zero_2" (formula "2") (term "1,0"))
(rule "add_zero_right" (formula "2") (term "0"))
(rule "inEqSimp_sepPosMonomial0" (formula "2"))
(rule "mul_literals" (formula "2") (term "1"))
(rule "inEqSimp_contradInEq1" (formula "2") (ifseqformula "1"))
(rule "qeq_literals" (formula "2") (term "0"))
(builtin "One Step Simplification" (formula "2"))
(rule "closeFalse" (formula "2"))
)
)
)
(branch " (stub, org.hyperledger.fabric.shim.ChaincodeStub::$transactionLog) in {(stub, org.hyperledger.fabric.shim.ChaincodeStub::$transactionLog)} | !( stub.@heap[create(p_3)] [p_3.id := pid] [p_3.name := name] [p_3. := TRUE] = TRUE | stub.@anon_heap_serialize<> = TRUE) FALSE"
(rule "castDel" (formula "30") (term "1,0,0,0,0,0,0,0,0"))
(builtin "One Step Simplification" (formula "30") (ifInst "" (formula "6")))
(rule "orRight" (formula "29"))
(rule "notRight" (formula "30"))
(rule "elementOfSingleton" (formula "30"))
(builtin "One Step Simplification" (formula "30"))
(rule "closeTrue" (formula "30"))
)
)
(branch "Case 2"
(builtin "One Step Simplification" (formula "29") (ifInst "" (formula "21")))
(rule "closeTrue" (formula "29"))
)
)
)
(branch "Case 2"
(builtin "One Step Simplification" (formula "29"))
(rule "closeTrue" (formula "29"))
)
)
(branch "Null Reference (r_5 = null)"
(rule "false_right" (formula "30"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "22")))
(rule "closeFalse" (formula "1"))
)
)
(branch "Exceptional Post (putState)"
(builtin "One Step Simplification" (formula "19"))
(builtin "One Step Simplification" (formula "12"))
(rule "andLeft" (formula "12"))
(rule "selectCreatedOfAnonAsFormulaEQ" (formula "13") (term "1,0") (ifseqformula "12"))
(rule "selectCreatedOfAnonAsFormulaEQ" (formula "13") (term "0,1,0") (ifseqformula "7"))
(rule "andLeft" (formula "13"))
(rule "andLeft" (formula "14"))
(rule "andLeft" (formula "13"))
(rule "notLeft" (formula "13"))
(rule "close" (formula "16") (ifseqformula "15"))
)
(branch "Pre (putState)"
(builtin "One Step Simplification" (formula "17") (ifInst "" (formula "11")) (ifInst "" (formula "11")))
(rule "wellFormedAnonEQ" (formula "17") (term "0") (ifseqformula "7"))
(rule "selectCreatedOfAnonAsFormulaEQ" (formula "17") (term "1") (ifseqformula "7"))
(rule "wellFormedStorePrimitive" (formula "17") (term "0,0"))
(rule "replace_known_left" (formula "17") (term "1,1") (ifseqformula "8"))
(builtin "One Step Simplification" (formula "17") (ifInst "" (formula "6")))
(rule "array2seqDef" (formula "9") (term "0") (inst "u=u"))
(rule "wellFormedStoreObject" (formula "17"))
(builtin "One Step Simplification" (formula "17") (ifInst "" (formula "16")))
(rule "dismissNonSelectedField" (formula "17") (term "0"))
(rule "pullOutSelect" (formula "17") (term "0") (inst "selectSK=java_lang_Object_created__1"))
(rule "simplifySelectOfCreate" (formula "1"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "15")))
(rule "castDel" (formula "1") (term "1,0"))
(rule "sortsDisjointModuloNull" (formula "1") (term "0,0"))
(rule "replace_known_right" (formula "1") (term "1,0,0") (ifseqformula "17"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "15")))
(rule "applyEqReverse" (formula "18") (term "0") (ifseqformula "1"))
(rule "close" (formula "18") (ifseqformula "5"))
)
(branch "Null reference (var_2 = null)"
(builtin "One Step Simplification" (formula "17") (ifInst "" (formula "15")))
(rule "closeTrue" (formula "17"))
)
)
(branch "Exceptional Post (serialize)"
(builtin "One Step Simplification" (formula "12"))
(builtin "One Step Simplification" (formula "7"))
(rule "andLeft" (formula "7"))
(rule "selectCreatedOfAnonAsFormulaEQ" (formula "8") (term "1,0") (ifseqformula "7"))
(rule "andLeft" (formula "8"))
(rule "andLeft" (formula "9"))
(rule "andLeft" (formula "8"))
(rule "andLeft" (formula "10"))
(rule "notLeft" (formula "8"))
(rule "close" (formula "12") (ifseqformula "11"))
)
(branch "Pre (serialize)"
(builtin "One Step Simplification" (formula "10"))
(rule "wellFormedStorePrimitive" (formula "10"))
(rule "wellFormedStoreObject" (formula "10"))
(builtin "One Step Simplification" (formula "10") (ifInst "" (formula "9")))
(rule "dismissNonSelectedField" (formula "10") (term "0"))
(rule "pullOutSelect" (formula "10") (term "0") (inst "selectSK=java_lang_Object_created__0"))
(rule "simplifySelectOfCreate" (formula "1"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "8")))
(rule "castDel" (formula "1") (term "1,0"))
(rule "sortsDisjointModuloNull" (formula "1") (term "0,0"))
(rule "replace_known_right" (formula "1") (term "0,0,0") (ifseqformula "8"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "10")))
(rule "applyEqReverse" (formula "11") (term "0") (ifseqformula "1"))
(rule "close" (formula "11") (ifseqformula "5"))
)
(branch "Null reference (p = null)"
(builtin "One Step Simplification" (formula "10") (ifInst "" (formula "7")))
(rule "closeTrue" (formula "10"))
)
)
(branch "Null Reference (p_1 = null)"
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "8")))
(rule "closeFalse" (formula "1"))
)
)
}