\profile "Java Profile";
\settings {
"#Proof-Settings-Config-File
#Tue Jan 31 15:48:48 CET 2017
[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]LOOP_OPTIONS_KEY=LOOP_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_NONE
[SMTSettings]instantiateHierarchyAssumptions=true
[StrategyProperty]AUTO_INDUCTION_OPTIONS_KEY=AUTO_INDUCTION_OFF
[StrategyProperty]DEP_OPTIONS_KEY=DEP_ON
[StrategyProperty]BLOCK_OPTIONS_KEY=BLOCK_CONTRACT
[StrategyProperty]CLASS_AXIOM_OPTIONS_KEY=CLASS_AXIOM_FREE
[StrategyProperty]QUERY_NEW_OPTIONS_KEY=QUERY_OFF
[Strategy]Timeout=-1
[Strategy]MaximumNumberOfAutomaticApplications=10000
[SMTSettings]integersMaximum=2147483645
[Choice]DefaultChoices=assertions-assertions\\:safe , initialisation-initialisation\\:disableStaticInitialisation , intRules-intRules\\:arithmeticSemanticsIgnoringOF , programRules-programRules\\:Java , runtimeExceptions-runtimeExceptions\\:ban , JavaCard-JavaCard\\:on , Strings-Strings\\:on , modelFields-modelFields\\:showSatisfiability , bigint-bigint\\:on , sequences-sequences\\:on , reach-reach\\:on , integerSimplificationRules-integerSimplificationRules\\:full , wdOperator-wdOperator\\:L , wdChecks-wdChecks\\:off , moreSeqRules-moreSeqRules\\:on , permissions-permissions\\:off , joinGenerateIsWeakeningGoal-joinGenerateIsWeakeningGoal\\: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
"
}
\javaSource "";
\proofObligation "#Proof Obligation Settings
#Tue Jan 31 15:48:48 CET 2017
name=PostInc[PostInc\\:\\:postinc()].JML normal_behavior operation contract.0
contract=PostInc[PostInc\\:\\:postinc()].JML normal_behavior operation contract.0
class=de.uka.ilkd.key.proof.init.FunctionalOperationContractPO
";
\proof {
(keyLog "0" (keyUser "pschmitt" ) (keyVersion "3b928241d3c6497f2bf3626bad48a3118b304db1"))
(autoModeTime "1350")
(branch "dummy ID"
(builtin "One Step Simplification" (formula "1") (newnames "self,exc,heapAtPre,o,f"))
(rule "translateJavaAddInt" (formula "1") (term "1,1,0,0,0,1,1"))
(rule "impRight" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "andLeft" (formula "1"))
(rule "notLeft" (formula "2"))
(rule "eqSymm" (formula "7") (term "0,0,0,0,1"))
(rule "polySimp_homoEq" (formula "7") (term "1,0,0,0,1"))
(rule "polySimp_addComm0" (formula "7") (term "0,0,1,0,0,0,1"))
(rule "polySimp_addComm1" (formula "7") (term "0,1,0,0,0,1"))
(rule "assignment" (formula "7") (term "1"))
(builtin "One Step Simplification" (formula "7"))
(rule "polySimp_sepPosMonomial" (formula "7") (term "1,0,0,0,1"))
(rule "polySimp_mulComm0" (formula "7") (term "1,1,0,0,0,1"))
(rule "polySimp_rightDist" (formula "7") (term "1,1,0,0,0,1"))
(rule "polySimp_mulLiterals" (formula "7") (term "1,1,1,0,0,0,1"))
(rule "mul_literals" (formula "7") (term "0,1,1,0,0,0,1"))
(rule "polySimp_elimOne" (formula "7") (term "1,1,1,0,0,0,1"))
(rule "Class_invariant_axiom_for_PostInc" (formula "5") (inst "sk=sk_0") (ifseqformula "3"))
(branch "Use Axiom"
(rule "andLeft" (formula "5"))
(rule "andLeft" (formula "6"))
(rule "notLeft" (formula "5"))
(rule "applyEq_and_gen0" (formula "9") (term "0,0,0,1"))
(rule "polySimp_homoEq" (formula "9") (term "0,0,0,0,1"))
(rule "polySimp_mulComm0" (formula "9") (term "1,0,0,0,0,0,1"))
(rule "polySimp_rightDist" (formula "9") (term "1,0,0,0,0,0,1"))
(rule "mul_literals" (formula "9") (term "0,1,0,0,0,0,0,1"))
(rule "polySimp_addAssoc" (formula "9") (term "0,0,0,0,0,1"))
(rule "polySimp_addComm0" (formula "9") (term "0,0,0,0,0,0,1"))
(rule "polySimp_sepNegMonomial" (formula "9") (term "0,0,0,0,1"))
(rule "polySimp_mulLiterals" (formula "9") (term "0,0,0,0,0,1"))
(rule "polySimp_elimOne" (formula "9") (term "0,0,0,0,0,1"))
(rule "methodBodyExpand" (formula "9") (term "1") (newnames "heapBefore_postinc,savedHeapBefore_postinc"))
(builtin "One Step Simplification" (formula "9"))
(rule "eval_order_access1" (formula "9") (term "1") (inst "#v0=p"))
(rule "variableDeclarationAssign" (formula "9") (term "1"))
(rule "variableDeclaration" (formula "9") (term "1") (newnames "p"))
(rule "assignment_read_attribute_this" (formula "9"))
(builtin "One Step Simplification" (formula "9"))
(rule "eval_order_access4" (formula "9") (term "1") (inst "#v1=x") (inst "#v0=p_1"))
(rule "variableDeclarationAssign" (formula "9") (term "1"))
(rule "variableDeclaration" (formula "9") (term "1") (newnames "p_1"))
(rule "assignment" (formula "9") (term "1"))
(builtin "One Step Simplification" (formula "9"))
(rule "variableDeclarationAssign" (formula "9") (term "1"))
(rule "variableDeclaration" (formula "9") (term "1") (newnames "x"))
(rule "postincrement_assignment_attribute" (formula "9") (term "1") (inst "#v1=x_1") (inst "#v=p_2"))
(rule "variableDeclarationAssign" (formula "9") (term "1"))
(rule "variableDeclaration" (formula "9") (term "1") (newnames "p_2"))
(rule "assignment_read_attribute_this" (formula "9"))
(builtin "One Step Simplification" (formula "9"))
(rule "variableDeclarationAssign" (formula "9") (term "1"))
(rule "variableDeclaration" (formula "9") (term "1") (newnames "x_1"))
(rule "assignment_read_attribute" (formula "9"))
(branch "Normal Execution (p_2 != null)"
(builtin "One Step Simplification" (formula "9"))
(rule "eval_order_access4" (formula "9") (term "1") (inst "#v1=x_2") (inst "#v0=p_3"))
(rule "variableDeclarationAssign" (formula "9") (term "1"))
(rule "variableDeclaration" (formula "9") (term "1") (newnames "p_3"))
(rule "assignment" (formula "9") (term "1"))
(builtin "One Step Simplification" (formula "9"))
(rule "variableDeclarationAssign" (formula "9") (term "1"))
(rule "variableDeclaration" (formula "9") (term "1") (newnames "x_2"))
(rule "compound_int_cast_expression" (formula "9") (term "1") (inst "#v=x_3"))
(rule "variableDeclarationAssign" (formula "9") (term "1"))
(rule "variableDeclaration" (formula "9") (term "1") (newnames "x_3"))
(rule "remove_parentheses_right" (formula "9") (term "1"))
(rule "compound_addition_1" (formula "9") (term "1") (inst "#v=x_4"))
(rule "variableDeclarationAssign" (formula "9") (term "1"))
(rule "variableDeclaration" (formula "9") (term "1") (newnames "x_4"))
(rule "assignment_read_attribute" (formula "9"))
(branch "Normal Execution (p_2 != null)"
(builtin "One Step Simplification" (formula "9"))
(rule "assignmentAdditionInt" (formula "9") (term "1"))
(builtin "One Step Simplification" (formula "9"))
(rule "translateJavaAddInt" (formula "9") (term "0,1,0"))
(rule "polySimp_addComm0" (formula "9") (term "0,1,0"))
(rule "widening_identity_cast_5" (formula "9") (term "1"))
(rule "assignment" (formula "9") (term "1"))
(builtin "One Step Simplification" (formula "9"))
(rule "assignment_write_attribute" (formula "9"))
(branch "Normal Execution (p_3 != null)"
(builtin "One Step Simplification" (formula "9"))
(rule "assignment" (formula "9") (term "1"))
(builtin "One Step Simplification" (formula "9"))
(rule "assignment_write_attribute" (formula "9"))
(branch "Normal Execution (p_1 != null)"
(builtin "One Step Simplification" (formula "9"))
(rule "methodCallEmpty" (formula "9") (term "1"))
(rule "tryEmpty" (formula "9") (term "1"))
(rule "emptyModality" (formula "9") (term "1"))
(builtin "One Step Simplification" (formula "9"))
(rule "polySimp_homoEq" (formula "9") (term "1,0"))
(rule "polySimp_addComm1" (formula "9") (term "0,1,0"))
(rule "dismissNonSelectedField" (formula "9") (term "1,1,1,0,0"))
(rule "dismissNonSelectedField" (formula "9") (term "1,0,0,0"))
(rule "dismissNonSelectedField" (formula "9") (term "1,1,0,1,0"))
(rule "dismissNonSelectedField" (formula "9") (term "1,1,1,0,0"))
(rule "dismissNonSelectedField" (formula "9") (term "1,0,0,0"))
(rule "dismissNonSelectedField" (formula "9") (term "1,0,1,0"))
(rule "dismissNonSelectedField" (formula "9") (term "0,0,0"))
(rule "polySimp_homoEq" (formula "9") (term "0,0"))
(rule "polySimp_addComm1" (formula "9") (term "0,0,0"))
(rule "dismissNonSelectedField" (formula "9") (term "1,1,0,1,0"))
(rule "polySimp_sepPosMonomial" (formula "9") (term "0,0"))
(rule "polySimp_mulComm0" (formula "9") (term "1,0,0"))
(rule "polySimp_rightDist" (formula "9") (term "1,0,0"))
(rule "mul_literals" (formula "9") (term "0,1,0,0"))
(rule "polySimp_mulLiterals" (formula "9") (term "1,1,0,0"))
(rule "polySimp_elimOne" (formula "9") (term "1,1,0,0"))
(rule "polySimp_sepPosMonomial" (formula "9") (term "1,0"))
(rule "polySimp_mulComm0" (formula "9") (term "1,1,0"))
(rule "polySimp_rightDist" (formula "9") (term "1,1,0"))
(rule "mul_literals" (formula "9") (term "0,1,1,0"))
(rule "polySimp_mulLiterals" (formula "9") (term "1,1,1,0"))
(rule "polySimp_elimOne" (formula "9") (term "1,1,1,0"))
(rule "pullOutSelect" (formula "9") (term "0,0,0") (inst "selectSK=PostInc_x_0"))
(rule "simplifySelectOfStore" (formula "1"))
(builtin "One Step Simplification" (formula "1"))
(rule "castDel" (formula "1") (term "0"))
(rule "applyEqReverse" (formula "10") (term "0,0,0") (ifseqformula "1"))
(rule "hideAuxiliaryEq" (formula "1"))
(rule "polySimp_homoEq" (formula "9") (term "0,0"))
(rule "polySimp_addComm1" (formula "9") (term "0,0,0"))
(rule "polySimp_sepPosMonomial" (formula "9") (term "0,0"))
(rule "polySimp_mulComm0" (formula "9") (term "1,0,0"))
(rule "polySimp_rightDist" (formula "9") (term "1,0,0"))
(rule "mul_literals" (formula "9") (term "0,1,0,0"))
(rule "polySimp_mulLiterals" (formula "9") (term "1,1,0,0"))
(rule "polySimp_elimOne" (formula "9") (term "1,1,0,0"))
(builtin "One Step Simplification" (formula "9"))
(rule "pullOutSelect" (formula "9") (term "0,0") (inst "selectSK=PostInc_y_0"))
(rule "simplifySelectOfStore" (formula "1"))
(builtin "One Step Simplification" (formula "1"))
(rule "castDel" (formula "1") (term "0"))
(rule "applyEqReverse" (formula "10") (term "0,0") (ifseqformula "1"))
(builtin "One Step Simplification" (formula "10"))
(rule "hideAuxiliaryEq" (formula "1"))
(rule "Class_invariant_axiom_for_PostInc" (formula "9") (inst "sk=sk_1") (ifseqformula "3"))
(branch "Use Axiom"
(rule "dismissNonSelectedField" (formula "9") (term "1,0,1,1"))
(rule "dismissNonSelectedField" (formula "9") (term "0,0,0"))
(rule "dismissNonSelectedField" (formula "9") (term "1,0,0,1"))
(rule "dismissNonSelectedField" (formula "9") (term "0,1,1"))
(rule "dismissNonSelectedField" (formula "9") (term "0,0,0"))
(rule "replace_known_right" (formula "9") (term "0,0") (ifseqformula "7"))
(builtin "One Step Simplification" (formula "9"))
(rule "dismissNonSelectedField" (formula "9") (term "1,0,1"))
(rule "replaceKnownSelect_taclet00000_2" (formula "9") (term "0,1"))
(rule "replaceKnownAuxiliaryConstant_taclet00000_3" (formula "9") (term "0,1"))
(rule "dismissNonSelectedField" (formula "9") (term "1,0,0"))
(rule "replaceKnownSelect_taclet00000_0" (formula "9") (term "0,0"))
(rule "replaceKnownAuxiliaryConstant_taclet00000_1" (formula "9") (term "0,0"))
(rule "replace_known_left" (formula "9") (term "0") (ifseqformula "6"))
(builtin "One Step Simplification" (formula "9"))
(rule "inEqSimp_geqRight" (formula "9"))
(rule "times_zero_1" (formula "1") (term "1,0,0"))
(rule "add_zero_right" (formula "1") (term "0,0"))
(rule "polySimp_addAssoc" (formula "1") (term "0"))
(rule "add_literals" (formula "1") (term "0,0"))
(rule "inEqSimp_sepPosMonomial0" (formula "1"))
(rule "mul_literals" (formula "1") (term "1"))
(rule "inEqSimp_contradInEq1" (formula "1") (ifseqformula "7"))
(rule "qeq_literals" (formula "1") (term "0"))
(builtin "One Step Simplification" (formula "1"))
(rule "closeFalse" (formula "1"))
)
(branch "Show Axiom Satisfiability"
(builtin "One Step Simplification" (formula "9"))
(rule "closeTrue" (formula "9"))
)
)
(branch "Null Reference (p_1 = null)"
(rule "false_right" (formula "10"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "8")))
(rule "closeFalse" (formula "1"))
)
)
(branch "Null Reference (p_3 = null)"
(rule "false_right" (formula "10"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "8")))
(rule "closeFalse" (formula "1"))
)
)
(branch "Null Reference (p_2 = null)"
(builtin "One Step Simplification" (formula "10"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "8")))
(rule "closeFalse" (formula "1"))
)
)
(branch "Null Reference (p_2 = null)"
(rule "false_right" (formula "10"))
(builtin "One Step Simplification" (formula "1") (ifInst "" (formula "8")))
(rule "closeFalse" (formula "1"))
)
)
(branch "Show Axiom Satisfiability"
(builtin "One Step Simplification" (formula "6"))
(rule "closeTrue" (formula "6"))
)
)
}