JavaCard Strings assertions bigint floatRules initialisation intRules integerSimplificationRules javaLoopTreatment mergeGenerateIsWeakeningGoal methodExpansion modelFields moreSeqRules permissions programRules reach runtimeExceptions sequences soundDefaultContracts wdChecks wdOperator

JavaCard:off JavaCard:on Strings:off Strings:on assertions:off assertions:on assertions:safe bigint:off bigint:on floatRules:assumeStrictfp floatRules:strictfpOnly initialisation:disableStaticInitialisation initialisation:enableStaticInitialisation intRules:arithmeticSemanticsCheckingOF intRules:arithmeticSemanticsIgnoringOF intRules:javaSemantics integerSimplificationRules:full integerSimplificationRules:minimal javaLoopTreatment:efficient javaLoopTreatment:teaching mergeGenerateIsWeakeningGoal:off mergeGenerateIsWeakeningGoal:on methodExpansion:modularOnly methodExpansion:noRestriction modelFields:showSatisfiability modelFields:treatAsAxiom moreSeqRules:off moreSeqRules:on permissions:off permissions:on programRules:Java programRules:None reach:off reach:on runtimeExceptions:allow runtimeExceptions:ban runtimeExceptions:ignore sequences:off sequences:on soundDefaultContracts:off soundDefaultContracts:on wdChecks:off wdChecks:on wdOperator:D wdOperator:L wdOperator:Y

C CSub E Field Free G G G G G G G G2 GOS GSub H H H H H Heap I J J K LocSet Map NonSingleton Pair Permission PermissionOwnerList RegEx S1 S1 S2 S2 SORT Seq alph alphSub alpha alpha alphaObj alphaObj alphaObj any bet beta beta betaObj betaObj boolean deltaObject double float fp gamma int java.io.Serializable java.lang.Cloneable java.lang.Math java.lang.Object numbers real subG

acc arrayStoreValid assignable checkPermissionOwner clContains clEndsWith clStartsWith createdInHeap disjoint doubleIsInfinite doubleIsNaN doubleIsNegative doubleIsNice doubleIsNormal doubleIsPositive doubleIsSubnormal doubleIsZero elementOf eqDouble eqFloat floatIsInfinite floatIsNaN floatIsNegative floatIsNice floatIsNormal floatIsPositive floatIsSubnormal floatIsZero geq geqDouble geqFloat gt gtDouble gtFloat inByte inChar inDomain inDomainImpliesCreated inInt inLong inRangeByte inRangeChar inRangeInt inRangeLong inRangeShort inShort isFinite leq leqDouble leqFloat lt ltDouble ltFloat match measuredBy measuredByCheck measuredByEmpty newObjectsIsomorphic newOnHeap nonEmptyPermission nonNull objectIsomorphic objectsIsomorphic permissionsFor prec reach readPermission readPermissionObject readPermissionOwe readPermissionOwe2 sameType sameTypes seqNPerm seqPerm ssubsort subset twoPermissions wellFormed wellOrderLeqInt writePermission writePermissionObject

# 0 1 2 3 4 5 6 7 8 9 C DFP FALSE FP TRUE Z absDouble absFloat acosDouble add addDouble addFloat addJint addJlong allElementsOfArray allElementsOfArrayLocsets allFields allLocs allObjects alph::ssort alpha::<classErroneous> alpha::<classInitializationInProgress> alpha::<classInitialized> alpha::<classPrepared> alpha::cast alpha::defaultValue alpha::exactInstance alpha::instance alpha::select alpha::seqGet alt andJint andJlong anon anySORT arr array2seq arrayRange asinDouble atan2Double atanDouble atom binaryAnd binaryOr binaryXOr bitwiseNegateJint bitwiseNegateJlong bprod bsum byte_HALFRANGE byte_MAX byte_MIN byte_RANGE char_MAX char_MIN char_RANGE checkedAddInt checkedAddLong checkedBitwiseAndInt checkedBitwiseAndLong checkedBitwiseNegateInt checkedBitwiseNegateLong checkedBitwiseOrInt checkedBitwiseOrLong checkedBitwiseXOrInt checkedBitwiseXOrLong checkedDivInt checkedDivLong checkedMulInt checkedMulLong checkedShiftLeftInt checkedShiftLeftLong checkedShiftRightInt checkedShiftRightLong checkedSubInt checkedSubLong checkedUnaryMinusInt checkedUnaryMinusLong checkedUnsignedShiftRightInt checkedUnsignedShiftRightLong clHashCode clIndexOfChar clIndexOfCl clLastIndexOfChar clLastIndexOfCl clRemoveZeros clReplace clTranslateInt consPermissionOwnerList cosDouble create currentThread div divDouble divFloat divJint divJlong empty emptyPermission emptyPermissionOwnerList expDouble first freshLocs index infiniteUnion initFullPermission insertPermissionOwner int_HALFRANGE int_MAX int_MIN int_RANGE intersect java.lang.Object::<created> java.lang.Object::<initialized> java.lang.Object::<transactionConditionallyUpdated> java.lang.Object::<transient> javaAddDouble javaAddDoubleForbiddenResult javaAddFloat javaAddFloatForbiddenResult javaAddInt javaAddIntOverFlow javaAddLong javaAddLongOverFlow javaBitwiseAndInt javaBitwiseAndLong javaBitwiseNegateInt javaBitwiseNegateLong javaBitwiseOrInt javaBitwiseOrIntOverFlow javaBitwiseOrLong javaBitwiseXOrInt javaBitwiseXOrLong javaCastByte javaCastByteOverFlow javaCastChar javaCastCharOverFlow javaCastInt javaCastIntOverFlow javaCastLong javaCastLongOverFlow javaCastShort javaCastShortOverFlow javaDivDouble javaDivDoubleForbiddenResult javaDivFloat javaDivFloatForbiddenResult javaDivInt javaDivIntOverFlow javaDivLong javaDivLongOverFlow javaMaxDouble javaMaxFloat javaMinDouble javaMinFloat javaMod javaModDouble javaModFloat javaModOverFlow javaMulDouble javaMulDoubleForbiddenResult javaMulFloat javaMulFloatForbiddenResult javaMulInt javaMulIntOverFlow javaMulLong javaMulLongOverFlow javaShiftLeftInt javaShiftLeftLong javaShiftRightInt javaShiftRightLong javaSubDouble javaSubDoubleForbiddenResult javaSubFloat javaSubFloatForbiddenResult javaSubInt javaSubIntOverFlow javaSubLong javaSubLongOverFlow javaUnaryMinusDouble javaUnaryMinusFloat javaUnaryMinusInt javaUnaryMinusIntOverFlow javaUnaryMinusLong javaUnaryMinusLongOverFlow javaUnsignedShiftRightInt javaUnsignedShiftRightLong javaUnsignedShiftRightOverFlow jdiv jmod length log long_HALFRANGE long_MAX long_MIN long_RANGE mapEmpty mapForeach mapGet mapOverride mapRemove mapSingleton mapSize mapUndef mapUpdate max memset min mod modJint modJlong moduloByte moduloChar moduloInt moduloLong moduloShort mul mulDouble mulFloat mulJint mulJlong neg negDouble negFloat neglit null opt orJint orJlong owner1 owner2 owner3 owner4 pair pow powDouble prod regEx regExConcat repeat repeatPlus repeatStar returnPermission returnPermissionOwner second seq2map seqConcat seqDef seqEmpty seqGetOutside seqIndexOf seqLen seqNPermInv seqRemove seqReverse seqSingleton seqSub seqSwap seqUpd seq_def_workaround seq_def_workaround2 setMinus shiftleft shiftleftJint shiftleftJlong shiftleftPositiveShift shiftright shiftrightJint shiftrightJlong shiftrightPositiveShift short_HALFRANGE short_MAX short_MIN short_RANGE sinDouble singleton slice slice1 slice2 sqrtDouble store sub subDouble subFloat subJint subJlong sum tanDouble transferPermission unaryMinusJint unaryMinusJlong undefinedLog undefinedPow union unsignedshift unsignedshiftrightJint unsignedshiftrightJlong values xorJint xorJlong

F T WD wd

alpha apply_auxiliary_eq apply_equations apply_equations_andOr apply_select_eq auto_induction auto_induction_lemma beta boolean_cases boxDiamondConv cast_deletion charLiteral_to_intLiteral classAxiom closure cnf_andAssoc cnf_andComm cnf_dist cnf_expandIfThenElse cnf_orAssoc cnf_orComm cnf_setComm comprehension_split comprehensions comprehensions_high_costs comprehensions_low_costs concrete confluence_restricted conjNormalForm cut cut_direct defOpsConcat defOpsReplace defOpsReplaceInline defOpsSeqEquality defOpsStartsEndsWith defOps_div defOps_divModPullOut defOps_expandJNumericOp defOps_expandModulo defOps_expandRanges defOps_jdiv defOps_jdiv_inline defOps_mod defOps_modHomoEq delayedExpansion delta delta distrQuantifier elimQuantifier elimQuantifierWithCast eval_literals evaluate_instanceof executeDoubleAssignment executeFloatAssignment executeIntegerAssignment find_term_not_in_assumes gamma gamma_destructive hide_auxiliary_eq hide_auxiliary_eq_const inEqSimp_andOr_subsumption inEqSimp_and_contradInEqs inEqSimp_and_subsumptionEq inEqSimp_antiSymm inEqSimp_balance inEqSimp_commute inEqSimp_contradEqs inEqSimp_contradInEqs inEqSimp_directInEquations inEqSimp_exactShadow inEqSimp_expand inEqSimp_forNormalisation inEqSimp_homo inEqSimp_makeNonStrict inEqSimp_moveLeft inEqSimp_nonLin inEqSimp_nonLin_divide inEqSimp_nonLin_multiply inEqSimp_nonLin_neg inEqSimp_nonLin_pos inEqSimp_nonNegSquares inEqSimp_normalise inEqSimp_or_antiSymm inEqSimp_or_tautInEqs inEqSimp_or_weaken inEqSimp_propagation inEqSimp_pullOutGcd inEqSimp_pullOutGcd_antec inEqSimp_pullOutGcd_geq inEqSimp_pullOutGcd_leq inEqSimp_saturate inEqSimp_signCases inEqSimp_special_nonLin inEqSimp_split_eq inEqSimp_strengthen inEqSimp_subsumption inReachableStateImplication induction_var information_flow_contract_appl insert_eq_nonrigid instanceof_to_exists int_arithmetic integerToString javaFloatSemantics javaIntegerSemantics limitObserver loopInvariant loop_expand loop_scope_expand loop_scope_inv_taclet merge_point method_expand modal_tautology moveQuantToLeft negationNormalForm no_self_application nonDuplicateAppCheckEq notHumanReadable obsolete order_terms partialInvAxiom polyDivision polySimp_addAssoc polySimp_addOrder polySimp_applyEq polySimp_applyEqPseudo polySimp_applyEqRigid polySimp_balance polySimp_critPair polySimp_directEquations polySimp_dist polySimp_elimOneLeft polySimp_elimOneRight polySimp_elimSubNeg polySimp_expand polySimp_homo polySimp_leftNonUnit polySimp_mulAssoc polySimp_mulOne polySimp_mulOrder polySimp_newSmallSym polySimp_newSym polySimp_normalise polySimp_pullOutFactor polySimp_pullOutGcd polySimp_saturate pullOutQuantifierAll pullOutQuantifierEx pullOutQuantifierUnifying pull_out_quantifier pull_out_select query_axiom replace_known_left replace_known_right semantics_blasting setEqualityBlastingRight simplify simplify_ENLARGING simplify_autoname simplify_boolean simplify_enlarging simplify_expression simplify_heap_high_costs simplify_instanceof_static simplify_int simplify_literals simplify_prog simplify_prog_subset simplify_select split_cond split_if std_taclets stringNormalisationReduce stringsConcatNotBothLiterals stringsContainsDefInline stringsExpandDefNormalOp stringsIntroduceNewSym stringsMoveReplaceInside stringsReduceConcat stringsReduceOrMoveOutsideConcat stringsReduceSubstring stringsSimplify swapQuantifiers system_invariant test_gen test_gen_empty_modality_hide test_gen_quan test_gen_quan_num triggered try_apply_subst type_hierarchy_def update_apply update_apply_on_update update_elim update_join userTaclets1 userTaclets2 userTaclets3

abortJavaCardTransactionAPI abortJavaCardTransactionBox abortJavaCardTransactionDiamond accDefinition acosIsNaN acosRange activeUseAddition activeUseAddition activeUseBitwiseAnd activeUseBitwiseAnd activeUseBitwiseNegation activeUseBitwiseNegation activeUseBitwiseOr activeUseBitwiseOr activeUseBitwiseXOr activeUseBitwiseXOr activeUseByteCast activeUseByteCast activeUseCharCast activeUseCharCast activeUseDivision activeUseDivision activeUseIntCast activeUseIntCast activeUseMinus activeUseModulo activeUseModulo activeUseMultiplication activeUseMultiplication activeUseShiftLeft activeUseShiftLeft activeUseShiftRight activeUseShiftRight activeUseShortCast activeUseShortCast activeUseStaticFieldReadAccess activeUseStaticFieldReadAccess activeUseStaticFieldReadAccess2 activeUseStaticFieldReadAccess2 activeUseStaticFieldWriteAccess activeUseStaticFieldWriteAccess activeUseStaticFieldWriteAccess2 activeUseStaticFieldWriteAccess2 activeUseStaticFieldWriteAccess3 activeUseStaticFieldWriteAccess3 activeUseStaticFieldWriteAccess4 activeUseStaticFieldWriteAccess4 activeUseStaticFieldWriteAccess5 activeUseStaticFieldWriteAccess5 activeUseStaticFieldWriteAccess6 activeUseStaticFieldWriteAccess6 activeUseSubtraction activeUseSubtraction activeUseUnaryMinus activeUseUnsignedShiftRight activeUseUnsignedShiftRight add_eq add_eq_back add_eq_back_2 add_eq_back_2_fst_comm add_eq_back_3 add_equations add_equations_right add_greater add_greatereq add_less add_less_back add_less_back_zero_1 add_less_back_zero_1_comm add_less_back_zero_2 add_less_back_zero_2_comm add_lesseq add_literals add_non_neg_square add_sub_elim_left add_sub_elim_right add_sub_step add_two_inequations_1 add_two_inequations_2 add_zero_left add_zero_right addition_associative allFieldsEq allFieldsSubsetOf allFieldsUnfold allLeft allLeftHide allObjectsAssignment allRight all_bool all_pull_out0 all_pull_out1 all_pull_out2 all_pull_out3 all_pull_out4 all_unused allocateInstance allocateInstance allocateInstanceWithLength allocateInstanceWithLength altAxiom andJIntDef andLeft andRight applyEq applyEqReverse applyEqRigid applyEq_and_gen0 applyEq_and_gen1 applyEq_and_gen2 applyEq_and_gen3 applyEq_and_int0 applyEq_and_int1 applyEq_and_int2 applyEq_and_int3 applyEq_and_int4 applyEq_and_int5 applyEq_and_int6 applyEq_and_int7 applyEq_or_gen0 applyEq_or_gen1 applyEq_or_gen2 applyEq_or_gen3 applyEq_or_int0 applyEq_or_int1 applyEq_or_int2 applyEq_or_int3 applyEq_or_int4 applyEq_or_int5 applyEq_or_int6 applyEq_or_int7 applyOnElementary applyOnPV applyOnParallel applyOnRigidFormula applyOnRigidTerm applyOnSkip applySkip1 applySkip2 applySkip3 apply_eq_boolean apply_eq_boolean_2 apply_eq_boolean_rigid apply_eq_boolean_rigid_2 apply_eq_monomials apply_eq_monomials_rigid apply_eq_pseudo_eq apply_eq_pseudo_geq apply_eq_pseudo_leq apply_subst apply_subst_for array2seqDef arrayCreation arrayCreationWithInitializers arrayInitialisation arrayLengthIsAShort arrayLengthIsAnInt arrayLengthNotNegative array_post_declaration array_self_reference array_self_reference_eq array_store_known_dynamic_array_type asinIsNaN asineIsZero asineRange assert assertSafe assertSafeWithMessage assertWithPrimitiveMessage assertWithReferenceMessage assertWithReferenceMessageNull assignableDefinition assignment assignmentAdditionBigint1 assignmentAdditionBigint2 assignmentAdditionDouble assignmentAdditionDoubleStrictFP assignmentAdditionFloat assignmentAdditionFloatStrictFP assignmentAdditionInt assignmentAdditionLong assignmentAdditionLong2 assignmentAdditionLong3 assignmentBitwiseAndInt assignmentBitwiseAndLong assignmentBitwiseAndLong2 assignmentBitwiseAndLong3 assignmentBitwiseOrInt assignmentBitwiseOrLong assignmentBitwiseOrLong2 assignmentBitwiseOrLong3 assignmentBitwiseXOrInt assignmentBitwiseXOrLong assignmentBitwiseXOrLong2 assignmentBitwiseXOrLong3 assignmentDivisionBigint1 assignmentDivisionBigint1 assignmentDivisionBigint1 assignmentDivisionBigint2 assignmentDivisionBigint2 assignmentDivisionBigint2 assignmentDivisionDouble assignmentDivisionDoubleStrictFP assignmentDivisionFloat assignmentDivisionFloatStrictFP assignmentDivisionInt assignmentDivisionInt assignmentDivisionInt assignmentDivisionLong assignmentDivisionLong assignmentDivisionLong assignmentDivisionLong2 assignmentDivisionLong2 assignmentDivisionLong2 assignmentModDouble assignmentModFloat assignmentModulo assignmentModulo assignmentModulo assignmentModuloBigint1 assignmentModuloBigint1 assignmentModuloBigint1 assignmentModuloBigint2 assignmentModuloBigint2 assignmentModuloBigint2 assignmentMultiplicationBigint1 assignmentMultiplicationBigint2 assignmentMultiplicationDouble assignmentMultiplicationDoubleStrictFP assignmentMultiplicationFloat assignmentMultiplicationFloatStrictFP assignmentMultiplicationInt assignmentMultiplicationLong assignmentMultiplicationLong2 assignmentMultiplicationLong3 assignmentShiftLeftInt assignmentShiftLeftLong assignmentShiftRightInt assignmentShiftRightLong assignmentSubtractionBigint1 assignmentSubtractionBigint2 assignmentSubtractionDouble assignmentSubtractionDoubleStrictFP assignmentSubtractionFloat assignmentSubtractionFloatStrictFP assignmentSubtractionInt assignmentSubtractionLong assignmentSubtractionLong2 assignmentSubtractionLong3 assignmentUnsignedShiftRightInt assignmentUnsignedShiftRightLong assignment_array2 assignment_array2 assignment_array2 assignment_read_attribute assignment_read_attribute assignment_read_attribute assignment_read_attribute_this assignment_read_attribute_this assignment_read_attribute_this assignment_read_length assignment_read_length assignment_read_length assignment_read_length_this assignment_read_static_attribute assignment_read_static_attribute_with_variable_prefix assignment_to_primitive_array_component assignment_to_primitive_array_component assignment_to_primitive_array_component assignment_to_primitive_array_component_transaction assignment_to_primitive_array_component_transaction assignment_to_primitive_array_component_transaction assignment_to_reference_array_component assignment_to_reference_array_component assignment_to_reference_array_component assignment_to_reference_array_component_transaction assignment_to_reference_array_component_transaction assignment_to_reference_array_component_transaction assignment_write_array_this_access_normalassign assignment_write_array_this_access_normalassign assignment_write_attribute assignment_write_attribute assignment_write_attribute assignment_write_attribute_this assignment_write_attribute_this assignment_write_static_attribute assignment_write_static_attribute_with_variable_prefix associativeLawIntersect associativeLawUnion atan2IsNaN atan2Range atanIsNaN atanIsZero atanRange autoInductGEQ_Lemma_1 autoInductGEQ_Lemma_2 autoInductGEQ_Lemma_3 autoInductGEQ_Lemma_5 autoInductGEQ_Lemma_6 autoInductGT_Lemma_1 autoInductGT_Lemma_2 autoInductGT_Lemma_3 autoInductGT_Lemma_5 autoInductGT_Lemma_6 autoInduct_Lemma auto_int_induction_geqZero auto_int_induction_geqZeroLeft auto_int_induction_geq_1 auto_int_induction_geq_2 auto_int_induction_geq_3 auto_int_induction_geq_5 auto_int_induction_geq_6 auto_int_induction_geq_Left1 auto_int_induction_geq_Left2 auto_int_induction_gt_1 auto_int_induction_gt_2 auto_int_induction_gt_3 auto_int_induction_gt_5 auto_int_induction_gt_6 auto_int_induction_gt_Left1 auto_int_induction_gt_Left2 beginJavaCardTransactionAPI beginJavaCardTransactionBox beginJavaCardTransactionDiamond binaryAndOne binaryAndSymm binaryAndZeroLeft binaryAndZeroRight binaryAnd_literals binaryOrGte binaryOrInInt binaryOrNeutralLeft binaryOrNeutralRight binaryOrSign binaryOr_literals binaryXOr_literals bitwiseNegateJIntDefinition bitwiseNegateJlongDefinition bitwiseNegationInt bitwiseNegationLong blockBreak blockBreakLabel blockBreakLabeled blockBreakNoLabel blockContinue blockContinueLabeled blockEmpty blockEmptyLabel blockReturn blockReturnLabel1 blockReturnLabel2 blockReturnNoValue blockThrow boolean_equal boolean_equal_2 boolean_false_commute boolean_not_equal_1 boolean_not_equal_2 boolean_true_commute boxToDiamond boxToDiamondTransaction box_and_left box_and_right box_or_left box_or_right box_true bprod_all_positive bprod_commutative_associative bprod_empty bprod_equal_one_right bprod_equal_zero_right bprod_find bprod_induction_lower bprod_induction_lower_concrete bprod_induction_upper bprod_induction_upper_concrete bprod_invert_index bprod_invert_index_concrete bprod_lower_equals_upper bprod_one bprod_one_factor bprod_one_factor_concrete1 bprod_one_factor_concrete2 bprod_shift_index bprod_split bprod_zero break bsum_add bsum_add_concrete bsum_commutative_associative bsum_def bsum_distributive bsum_empty bsum_equal_except_one_index bsum_equal_split1 bsum_equal_split2 bsum_equal_split3 bsum_equal_split4 bsum_induction_lower bsum_induction_lower2 bsum_induction_lower2_concrete bsum_induction_lower_concrete bsum_induction_upper bsum_induction_upper2 bsum_induction_upper2_concrete bsum_induction_upper_concrete bsum_induction_upper_concrete_2 bsum_invert_index bsum_invert_index_concrete bsum_less_same_index bsum_lower_bound bsum_lower_equals_upper bsum_num_of_bounds bsum_num_of_bounds2 bsum_num_of_gt0 bsum_num_of_gt0_alt bsum_num_of_is_max bsum_num_of_is_max2 bsum_num_of_is_max3 bsum_num_of_is_max4 bsum_num_of_lt_max bsum_num_of_lt_max2 bsum_num_of_lt_max3 bsum_num_of_lt_max4 bsum_one_summand bsum_one_summand_concrete1 bsum_one_summand_concrete2 bsum_positive bsum_positive1 bsum_positive2 bsum_positive_lower_bound_element bsum_same_summand bsum_shift_index bsum_split bsum_split_in_three bsum_sub_same_index bsum_upper_bound bsum_zero bsum_zero_right cancel_equation cancel_gtNeg cancel_gtPos case_distinction_l case_distinction_r castAdd castAdd2 castDel castDel2 castLongToFloatAddition2 castToBoolean castTrueImpliesOriginalTrue castType castType2 castedGetAny charLiteral_to_int checkPermissionOwner_empty checkPermissionOwner_nonempty class_being_initialized_is_prepared class_erroneous_excludes_class_in_init class_initialized_excludes_class_init_in_progress close closeAntec closeFalse closeTrue closeType closeTypeSwitched close_by_lt_leq cnf_eqv cnf_rightDist collect_same_terms_1 collect_same_terms_2 collect_same_terms_3 commitJavaCardTransactionAPI commitJavaCardTransactionBox commitJavaCardTransactionDiamond commuteDisjoint commuteIntersection commuteIntersection_2 commuteUnion commuteUnion_2 commute_and commute_and_2 commute_or commute_or_2 compound_addition_1 compound_addition_2 compound_assignment_1_new compound_assignment_2 compound_assignment_3_mixed compound_assignment_3_nonsimple compound_assignment_3_simple compound_assignment_4_nonsimple compound_assignment_4_simple compound_assignment_5_mixed compound_assignment_5_nonsimple compound_assignment_5_simple compound_assignment_6_nonsimple compound_assignment_6_simple compound_assignment_op_and compound_assignment_op_and_array compound_assignment_op_and_attr compound_assignment_op_div compound_assignment_op_div_array compound_assignment_op_div_attr compound_assignment_op_minus compound_assignment_op_minus_array compound_assignment_op_minus_attr compound_assignment_op_mod compound_assignment_op_mod_array compound_assignment_op_mod_attr compound_assignment_op_mul compound_assignment_op_mul_array compound_assignment_op_mul_attr compound_assignment_op_or compound_assignment_op_or_array compound_assignment_op_or_attr compound_assignment_op_plus compound_assignment_op_plus_array compound_assignment_op_plus_attr compound_assignment_op_shiftleft compound_assignment_op_shiftleft_array compound_assignment_op_shiftleft_attr compound_assignment_op_shiftright compound_assignment_op_shiftright_array compound_assignment_op_shiftright_attr compound_assignment_op_unsigned_shiftright compound_assignment_op_unsigned_shiftright_array compound_assignment_op_unsigned_shiftright_attr compound_assignment_op_xor compound_assignment_op_xor_array compound_assignment_op_xor_attr compound_assignment_xor_nonsimple compound_assignment_xor_simple compound_binary_AND_1 compound_binary_AND_2 compound_binary_OR_1 compound_binary_OR_2 compound_binary_XOR_1 compound_binary_XOR_2 compound_binary_neg compound_byte_cast_expression compound_division_1 compound_division_2 compound_double_cast_expression compound_equality_comparison_1 compound_equality_comparison_2 compound_float_cast_expression compound_greater_equal_than_comparison_1 compound_greater_equal_than_comparison_2 compound_greater_than_comparison_1 compound_greater_than_comparison_2 compound_inequality_comparison_1 compound_inequality_comparison_2 compound_int_cast_expression compound_invert_bits compound_less_equal_than_comparison_1 compound_less_equal_than_comparison_2 compound_less_than_comparison_1 compound_less_than_comparison_2 compound_long_cast_expression compound_modulo_1 compound_modulo_2 compound_multiplication_1 compound_multiplication_2 compound_reference_cast_expression compound_reference_cast_expression_primitive compound_shiftleft_1 compound_shiftleft_2 compound_shiftright_1 compound_shiftright_2 compound_short_cast_expression compound_subtraction_1 compound_subtraction_2 compound_unary_minus_eval compound_unary_plus_assignment compound_unsigned_shiftright_1 compound_unsigned_shiftright_2 concatRepeatContraction1 concatRepeatContraction2 concatRepeatContraction2Sym concatRepeatContraction3 concatRepeatContraction3Sym concrete_and_1 concrete_and_2 concrete_and_3 concrete_and_4 concrete_eq_1 concrete_eq_2 concrete_eq_3 concrete_eq_4 concrete_impl_1 concrete_impl_2 concrete_impl_3 concrete_impl_4 concrete_not_1 concrete_not_2 concrete_or_1 concrete_or_2 concrete_or_3 concrete_or_4 concrete_or_5 condition condition_not_simple condition_simple contains containsAxiomAntec containsAxiomSucc cosIsNaN cosIsNaNAlt cosIsNotNaN cosRange cosRange2 cosRangeAlt createdInHeapToElementOf createdInHeapWithAllFields createdInHeapWithAllFieldsEQ createdInHeapWithArrayRange createdInHeapWithArrayRangeEQ createdInHeapWithEmpty createdInHeapWithObserver createdInHeapWithObserverEQ createdInHeapWithSelect createdInHeapWithSelectEQ createdInHeapWithSetMinusFreshLocs createdInHeapWithSetMinusFreshLocsEQ createdInHeapWithSingleton createdInHeapWithSingletonEQ createdInHeapWithUnion createdInHeapWithUnionEQ createdOnHeapImpliesCreatedOnPermissions crossInst cut cutUpperBound cut_direct cut_direct_l cut_direct_r defInDomainImpliesCreated defIsFinite defMapEmpty defMapEquality defMapOverride defMapRemove defMapSingleton defMapUpdate defOfEmpty defOfSeqConcat defOfSeqNPermInv defOfSeqRemove defOfSeqReverse defOfSeqSingleton defOfSeqSub defOfSeqSwap defOfSeqUpd defSeq2Map def_wellOrderLeqInt definitionAllElementsOfArray definitionAllElementsOfArray2 definitionAllElementsOfArrayLocsets definitionOfNewObjectsIsomorphic definitionOfNewOnHeap definitionOfObjectIsomorphic definitionOfObjectsIsomorphic definitionOfSameTypes definitionSeqdefWorkaround definitionSeqdefWorkaround2 deleteMergePoint delete_unnecessary_cast diamondToBox diamondToBoxTransaction diamond_and_left diamond_and_right diamond_false diamond_or_left diamond_or_right diamond_split_termination disjointAllFields disjointAllFields_2 disjointAllObjects disjointAndSubset1 disjointAndSubset2 disjointAndSubset_3 disjointAndSubset_4 disjointAndSubset_5 disjointAndSubset_6 disjointArrayRangeAllFields1 disjointArrayRangeAllFields2 disjointArrayRanges disjointDefinition disjointInfiniteUnion disjointInfiniteUnion_2 disjointNotInOtherLocset1 disjointNotInOtherLocset2 disjointToElementOf disjointWithEmpty disjointWithSingleton1 disjointWithSingleton2 dismissNonSelectedField dismissNonSelectedFieldEQ distr_existsAnd1 distr_existsAnd2 distr_existsOr distr_forallAnd distr_forallOr1 distr_forallOr2 distributeIntersection distributeIntersection_2 divAddMultDenom divGreatestDNeg divGreatestDPos divIncreasingNeg divIncreasingPos divLeastDNeg divLeastDPos divMinus divMinusDenom divResOne1 divResOne2 divResZero1 divResZero2 div_axiom div_cancel1 div_cancel2 div_exists div_literals div_one div_unique1 div_unique2 div_zero divide_eq0 divide_eq1 divide_eq2 divide_eq3 divide_eq4 divide_eq5 divide_eq6 divide_eq7 divide_equation divide_geq divide_inEq0 divide_inEq1 divide_inEq2 divide_inEq3 divide_inEq4 divide_inEq5 divide_inEq6 divide_inEq7 divide_leq doWhileUnwind doubleAcos doubleAsin doubleAtan doubleAtan2 doubleCos doubleExp doubleImpLeft doublePow doubleSin doubleSqrt doubleTan double_not double_unary_minus_literal dropEffectlessStores elementOfAllFields elementOfAllLocs elementOfAllObjects elementOfArrayRange elementOfArrayRangeConcrete elementOfArrayRangeEQ elementOfEmpty elementOfFreshLocs elementOfGuardedSet elementOfInfiniteUnion elementOfInfiniteUnion2Vars elementOfInfiniteUnion2VarsEQ elementOfInfiniteUnionEQ elementOfIntersect elementOfIntersectEQ elementOfSetMinus elementOfSetMinusEQ elementOfSingleton elementOfSubsetImpliesElementOfSuperset elementOfSubsetOfUnion1 elementOfSubsetOfUnion2 elementOfUnion elementOfUnionEQ elimGcdEq elimGcdGeq elimGcdGeq_antec elimGcdLeq elimGcdLeq_antec elim_double_block elim_double_block_2 elim_double_block_3 elim_double_block_4 elim_double_block_5 elim_double_block_6 elim_double_block_7 elim_double_block_8 elim_double_block_9 elim_exists0 elim_exists1 elim_exists2 elim_exists3 elim_exists4 elim_exists5 elim_exists6 elim_exists7 elim_exists_leq elim_exists_nonSingleton0 elim_exists_nonSingleton1 elim_exists_nonSingleton2 elim_exists_nonSingleton3 elim_exists_nonSingleton4 elim_exists_nonSingleton5 elim_exists_sub_1 elim_exists_sub_1_and_phi elim_exists_sub_1_or_phi elim_forall0 elim_forall1 elim_forall10 elim_forall11 elim_forall12 elim_forall13 elim_forall14 elim_forall15 elim_forall16 elim_forall17 elim_forall18 elim_forall19 elim_forall2 elim_forall3 elim_forall4 elim_forall5 elim_forall6 elim_forall7 elim_forall8 elim_forall9 elim_forall_eqSet_imp_phi elim_forall_leq elim_forall_nonSingleton0 elim_forall_nonSingleton1 elim_forall_nonSingleton2 elim_forall_nonSingleton3 elim_forall_nonSingleton4 elim_forall_nonSingleton5 elim_forall_subOfAll elim_forall_subOfAll_and_phi elim_forall_superOfAll elim_forall_superOfAll_and_phi emptyEqualsSingleton emptyModality emptyModalityBoxTransaction emptyModalityDiamondTransaction emptyStatement endsWith enhancedfor_iterable eqClose eqSameSeq eqSeqConcat eqSeqConcat2 eqSeqConcat2EQ eqSeqConcat3 eqSeqConcat3EQ eqSeqConcat4 eqSeqConcat4EQ eqSeqConcat5 eqSeqConcat5EQ eqSeqConcatEQ eqSeqDef eqSeqDef2 eqSeqEmpty eqSeqReverse eqSeqReverse2 eqSeqSingleton eqSeqSingleton2 eqSymm eqTermCut eq_add_iff1 eq_add_iff2 eq_and eq_and_2 eq_eq eq_imp eq_or eq_or_2 eq_sides equalCharacters equalRegEx equalUnique equal_add equal_add_one equal_bprod1 equal_bprod2 equal_bprod3 equal_bprod5 equal_bprod_perm1 equal_bprod_perm2 equal_bsum1 equal_bsum2 equal_bsum3 equal_bsum5 equal_bsum_perm1 equal_bsum_perm2 equal_bsum_zero_cut equal_literals equalityToElementOf equalityToElementOfRight equalityToSelect equalityToSeqGetAndSeqLen equalityToSeqGetAndSeqLenLeft equalityToSeqGetAndSeqLenRight equality_comparison_double equality_comparison_new equality_comparison_simple equality_comparison_simple_float equivAllRight equiv_left equiv_right erroneous_class_has_no_initialized_sub_class eval_array_this_access eval_order_access1 eval_order_access2 eval_order_access4 eval_order_access4_this eval_order_array_access1 eval_order_array_access2 eval_order_array_access3 eval_order_array_access3 eval_order_array_access4 eval_order_array_access5 eval_order_array_access6 eval_order_iterated_assignments_0_0 eval_order_iterated_assignments_0_1 eval_order_iterated_assignments_10_0 eval_order_iterated_assignments_10_1 eval_order_iterated_assignments_11_0 eval_order_iterated_assignments_11_1 eval_order_iterated_assignments_1_0 eval_order_iterated_assignments_1_1 eval_order_iterated_assignments_2_0 eval_order_iterated_assignments_2_1 eval_order_iterated_assignments_3_0 eval_order_iterated_assignments_3_1 eval_order_iterated_assignments_4_0 eval_order_iterated_assignments_4_1 eval_order_iterated_assignments_5_0 eval_order_iterated_assignments_5_1 eval_order_iterated_assignments_6_0 eval_order_iterated_assignments_6_1 eval_order_iterated_assignments_7_0 eval_order_iterated_assignments_7_1 eval_order_iterated_assignments_8_0 eval_order_iterated_assignments_8_1 eval_order_iterated_assignments_9_0 eval_order_iterated_assignments_9_1 evaluateAssertCondition_1 evaluateAssertCondition_2 evaluateAssertMessage exLeft exRight exRightHide ex_bool ex_pull_out0 ex_pull_out1 ex_pull_out2 ex_pull_out3 ex_pull_out4 ex_unused exact_instance_definition_boolean exact_instance_definition_int exact_instance_definition_null exact_instance_for_interfaces_or_abstract_classes exact_instance_known_dynamic_type execBreak execBreakEliminateBreakLabel execBreakEliminateBreakLabelWildcard execBreakEliminateContinue execBreakEliminateContinueLabel execBreakEliminateContinueLabelWildcard execBreakEliminateExcCcatch execBreakEliminateReturn execBreakEliminateReturnVal execBreakLabelEliminateBreak execBreakLabelEliminateBreakLabelNoMatch execBreakLabelEliminateContinue execBreakLabelEliminateContinueLabel execBreakLabelEliminateContinueLabelWildcard execBreakLabelEliminateExcCcatch execBreakLabelEliminateReturn execBreakLabelEliminateReturnVal execBreakLabelMatch execBreakLabelWildcard execCatchThrow execContinue execContinueEliminateBreak execContinueEliminateBreakLabel execContinueEliminateBreakLabelWildcard execContinueEliminateExcCcatch execContinueEliminateReturn execContinueEliminateReturnVal execContinueLabelEliminateBreak execContinueLabelEliminateBreakLabel execContinueLabelEliminateBreakLabelWildcard execContinueLabelEliminateContinue execContinueLabelEliminateContinueLabelNoMatch execContinueLabelEliminateExcCcatch execContinueLabelEliminateReturn execContinueLabelEliminateReturnVal execContinueLabelMatch execContinueLabelWildcard execEmpty execMultipleCatchThrow execNoCcatch execReturn execReturnEliminateBreak execReturnEliminateBreakLabel execReturnEliminateBreakLabelWildcard execReturnEliminateContinue execReturnEliminateContinueLabel execReturnEliminateContinueLabelWildcard execReturnEliminateExcCcatch execReturnEliminateReturnVal execReturnVal execReturnValEliminateBreak execReturnValEliminateBreakLabel execReturnValEliminateBreakLabelWildcard execReturnValEliminateContinue execReturnValEliminateContinueLabel execReturnValEliminateContinueLabelWildcard execReturnValEliminateExcCcatch execReturnValEliminateReturn execReturnValNonMatchingType execThrowEliminateBreak execThrowEliminateBreakLabel execThrowEliminateBreakLabelWildcard execThrowEliminateContinue execThrowEliminateContinueLabel execThrowEliminateContinueLabelWildcard execThrowEliminateReturn execThrowEliminateReturnVal expIsInfinite expIsNaN expIsZero expandInByte expandInByte expandInChar expandInChar expandInInt expandInInt expandInLong expandInLong expandInRangeByte expandInRangeChar expandInRangeInt expandInRangeLong expandInRangeShort expandInShort expandInShort expand_addJint expand_addJlong expand_divJint expand_divJlong expand_modJint expand_modJlong expand_moduloByte expand_moduloChar expand_moduloInteger expand_moduloLong expand_moduloShort expand_mulJint expand_mulJlong expand_subJint expand_subJlong expand_unaryMinusJint expand_unaryMinusJlong false_right false_to_not_true finishJavaCardTransactionBox finishJavaCardTransactionDiamond firstOfPair forInitUnfold for_to_while geq_add geq_add_one geq_diff_1 geq_to_leq geq_to_lt geq_to_lt_alt getAnyOfArray2seq getAnyOfNPermInv getJavaCardTransient getOfArray2seq getOfMapEmpty getOfMapForeach getOfMapOverride getOfMapRemove getOfMapSingleton getOfMapUpdate getOfNPermInv getOfRemoveAny getOfRemoveAnyConcrete1 getOfRemoveAnyConcrete2 getOfRemoveInt getOfSeq2Map getOfSeqConcat getOfSeqConcatEQ getOfSeqDef getOfSeqDefEQ getOfSeqReverse getOfSeqReverseEQ getOfSeqSingleton getOfSeqSingletonConcrete getOfSeqSingletonEQ getOfSeqSub getOfSeqSubEQ getOfSeqUpd getOfSwap greater greater_add greater_add_one greater_equal_than_comparison_new greater_equal_than_comparison_simple greater_equal_than_comparison_simple_double greater_equal_than_comparison_simple_float greater_literals greater_than_comparison_new greater_than_comparison_simple greater_than_comparison_simple_double greater_than_comparison_simple_float gt_diff_1 gt_to_lt hashCodeBase hideAuxiliaryEq hideAuxiliaryEqConcrete hideAuxiliaryEqConcrete2 hide_left hide_right i_minus_i_is_zero identityCastDouble identityCastFloat if ifElse ifElseFalse ifElseSkipElse ifElseSkipElseConditionInBlock ifElseSkipThen ifElseSkipThenConditionInBlock ifElseSplit ifElseSplitLeft ifElseTrue ifElseUnfold ifEnterThen ifEnterThenConditionInBlock ifEqualsInteger ifEqualsNull ifEqualsTRUE ifExthenelse1_eq ifExthenelse1_eq2 ifExthenelse1_eq2_for ifExthenelse1_eq2_for_phi ifExthenelse1_eq2_phi ifExthenelse1_eq_for ifExthenelse1_eq_for_phi ifExthenelse1_eq_phi ifExthenelse1_false ifExthenelse1_false_for ifExthenelse1_min ifExthenelse1_min_for ifExthenelse1_solve ifExthenelse1_solve_for ifExthenelse1_split ifExthenelse1_split_for ifExthenelse1_unused_var ifExthenelse1_unused_var_for ifFalse ifSkipThen ifSkipThenConditionInBlock ifSplit ifSplitLeft ifTrue ifUnfold ifthenelse_concrete ifthenelse_concrete2 ifthenelse_concrete3 ifthenelse_concrete4 ifthenelse_equals ifthenelse_equals_1 ifthenelse_equals_2 ifthenelse_false ifthenelse_false_for ifthenelse_negated ifthenelse_negated_for ifthenelse_same_branches ifthenelse_same_branches_for ifthenelse_split ifthenelse_split_for ifthenelse_to_or_for ifthenelse_to_or_for2 ifthenelse_to_or_left ifthenelse_to_or_left2 ifthenelse_to_or_right ifthenelse_to_or_right2 ifthenelse_true ifthenelse_true_for impLeft impRight inDomainConcrete inDomainOfMapEmpty inDomainOfMapForeach inDomainOfMapOverride inDomainOfMapRemove inDomainOfMapSingleton inDomainOfMapUpdate inDomainOfSeq2Map inEqSimp_and_antiSymm0 inEqSimp_and_antiSymm1 inEqSimp_and_contradInEq0 inEqSimp_and_contradInEq1 inEqSimp_and_strengthen0 inEqSimp_and_strengthen1 inEqSimp_and_strengthen2 inEqSimp_and_strengthen3 inEqSimp_and_subsumption0 inEqSimp_and_subsumption1 inEqSimp_and_subsumption2 inEqSimp_and_subsumption3 inEqSimp_and_subsumption4 inEqSimp_and_subsumption5 inEqSimp_and_subsumption6 inEqSimp_and_subsumption7 inEqSimp_antiSymm inEqSimp_commuteGeq inEqSimp_commuteLeq inEqSimp_contradEq3 inEqSimp_contradEq7 inEqSimp_contradInEq0 inEqSimp_contradInEq1 inEqSimp_contradInEq2 inEqSimp_contradInEq3 inEqSimp_contradInEq4 inEqSimp_contradInEq5 inEqSimp_exactShadow0 inEqSimp_exactShadow1 inEqSimp_exactShadow2 inEqSimp_exactShadow3 inEqSimp_geqRight inEqSimp_gtRight inEqSimp_gtToGeq inEqSimp_homoInEq0 inEqSimp_homoInEq1 inEqSimp_invertInEq0 inEqSimp_invertInEq1 inEqSimp_leqRight inEqSimp_ltRight inEqSimp_ltToLeq inEqSimp_notGeq inEqSimp_notLeq inEqSimp_or_antiSymm0 inEqSimp_or_antiSymm1 inEqSimp_or_subsumption0 inEqSimp_or_subsumption1 inEqSimp_or_subsumption2 inEqSimp_or_subsumption3 inEqSimp_or_subsumption4 inEqSimp_or_subsumption5 inEqSimp_or_subsumption6 inEqSimp_or_subsumption7 inEqSimp_or_tautInEq0 inEqSimp_or_tautInEq1 inEqSimp_or_tautInEq2 inEqSimp_or_tautInEq3 inEqSimp_or_weaken0 inEqSimp_or_weaken1 inEqSimp_or_weaken2 inEqSimp_or_weaken3 inEqSimp_sepNegMonomial0 inEqSimp_sepNegMonomial1 inEqSimp_sepPosMonomial0 inEqSimp_sepPosMonomial1 inEqSimp_strengthen0 inEqSimp_strengthen1 inEqSimp_subsumption0 inEqSimp_subsumption1 inEqSimp_subsumption2 inEqSimp_subsumption4 inEqSimp_subsumption5 inEqSimp_subsumption6 indexOf indexOfSeqConcatFirst indexOfSeqConcatSecond indexOfSeqSingleton indexOfSeqSub indexOfStr ineffectiveCast ineffectiveCast2 ineffectiveCast3 inequality_comparison_new inequality_comparison_simple inequality_comparison_simple_double inequality_comparison_simple_float infiniteUnionUnused initFullPermission initialized_class_is_not_erroneous initialized_class_is_prepared insertPermissionOwner insert_constant_value insert_eq_all insert_eqv_lr insert_eqv_once_lr insert_eqv_once_rl insert_eqv_rl instAll instEx instanceCreation instanceCreationAssignment instanceCreationAssignmentUnfoldArguments instanceCreationUnfoldArguments instanceof_eval instanceof_known_dynamic_type instanceof_known_dynamic_type_2 instanceof_not_compatible instanceof_not_compatible_2 instanceof_not_compatible_3 instanceof_not_compatible_4 instanceof_not_compatible_5 instanceof_static_type instanceof_static_type_2 intDivRem intLongToFloatAddition1 intToFloatAddition int_diff_minus_eq int_induction intersectAllFieldsFreshLocs intersectWithAllLocs intersectWithAllLocsRight intersectWithEmpty intersectWithEmptyRight intersectWithItself intersectWithSingleton intersectionSetMinusItself intersectionSetMinusItself_2 introduceAxiom irrflConcrete1 irrflConcrete2 isFiniteOfMapEmpty isFiniteOfMapRemove isFiniteOfMapSingleton isFiniteOfMapUpdate isFiniteOfSeq2Map iterated_assignments_0 iterated_assignments_1 iterated_assignments_10 iterated_assignments_11 iterated_assignments_2 iterated_assignments_3 iterated_assignments_4 iterated_assignments_5 iterated_assignments_6 iterated_assignments_7 iterated_assignments_8 iterated_assignments_9 javaShiftLeftIntDef javaShiftLeftLongDef javaShiftRightIntDef javaShiftRightLongDef jdivAddMultDenom jdivMultDenom1 jdivMultDenom2 jdivPulloutMinusDenom jdivPulloutMinusNum jdiv_axiom jdiv_axiom_inline jdiv_one jdiv_uniqueNegNeg jdiv_uniqueNegPos jdiv_uniquePosNeg jdiv_uniquePosPos jdiv_zero jmodAddMultDenomZero jmodAltZero jmodDivisible jmodDivisibleRep jmodNumZero jmodUnique1 jmodUnique2 jmod_NumNeg jmod_NumPos jmod_axiom jmod_geZero jmod_pulloutminusDenom jmod_pulloutminusNum jmodjmod lastIndexOf lastIndexOfStr le1_add1_eq_le left_add_mult_distrib lenNonNegative lenOfArray2seq lenOfNPermInv lenOfRemove lenOfRemoveConcrete1 lenOfRemoveConcrete2 lenOfSeqConcat lenOfSeqConcatEQ lenOfSeqDef lenOfSeqDefEQ lenOfSeqEmpty lenOfSeqEmptyEQ lenOfSeqReverse lenOfSeqReverseEQ lenOfSeqSingleton lenOfSeqSingletonEQ lenOfSeqSub lenOfSeqSubEQ lenOfSeqUpd lenOfSwap lengthReplace lengthReplaceEQ leq_add leq_add_iff1 leq_add_iff2 leq_add_one leq_diff1_eq leq_diff_1 leq_iff_diff_leq_0 leq_literals leq_to_geq leq_to_gt leq_to_gt_alt leq_trans less_1_mult less_add less_add_iff1 less_add_iff2 less_add_one less_base less_equal_than_comparison_new less_equal_than_comparison_simple less_equal_than_comparison_simple_double less_equal_than_comparison_simple_float less_iff_diff_less_0 less_is_alternative_1 less_is_alternative_2 less_is_total less_is_total_heu less_literals less_neg less_plus less_sub less_than_comparison_new less_than_comparison_simple less_than_comparison_simple_double less_than_comparison_simple_float less_trans less_zero_is_total local_cut log1Concrete logDefinition logLessThanPow logLessThanPowConcrete logMono logMonoConcrete logPositive logPositiveConcrete logPowIdentity logPowIdentityConcrete logProdIdentity logProdIdentityConcrete logProduct logSelfConcrete logSqueeze logTimesBaseConcrete loopScopeInvBox loopScopeInvDia loopUnwind lsBreak lsContinue lsLblBreak lsLblContinueMatch lsLblContinueNoMatch1 lsLblContinueNoMatch2 lsReturnNonVoid lsReturnVoid lsThrow lt_diff_1 lt_to_gt lt_to_leq_1 lt_to_leq_2 make_insert_eq make_insert_eq_nonrigid mapEqualityRight mapRemoveUnchanged mapRemoveUnchanged2 mapSizeNotNegativeForFiniteMaps mapUpdateUnchanged mapUpdateUnchanged2 maxAxiom measuredByCheck measuredByCheckEmpty memsetEmpty methodBodyExpand methodCall methodCall methodCall methodCallEmpty methodCallEmptyNoreturnBox methodCallEmptyReturn methodCallParamThrow methodCallReturn methodCallReturnIgnoreResult methodCallSuper methodCallThrow methodCallUnfoldArguments methodCallUnfoldTarget methodCallWithAssignment methodCallWithAssignment methodCallWithAssignment methodCallWithAssignmentSuper methodCallWithAssignmentUnfoldArguments methodCallWithAssignmentUnfoldTarget methodCallWithAssignmentWithinClass methodCallWithAssignmentWithinClass methodCallWithinClass methodCallWithinClass minAxiom minus_distribute_1 minus_distribute_2 mod_axiom mod_geZero mod_homoEq mod_lessDenom moduloByteFixpoint moduloByteFixpointInline moduloByteIsInByte moduloByteIsInRangeByte moduloCharFixpoint moduloCharFixpointInline moduloCharIsInChar moduloCharIsInRangeChar moduloIntFixpoint moduloIntFixpointInline moduloIntIsInInt moduloIntIsInRangeInt moduloLongFixpoint moduloLongFixpointInline moduloLongIsInLong moduloLongIsInRangeLong moduloShortFixpoint moduloShortFixpointInline moduloShortIsInRangeShort moduloShortIsInShort mul_assoc mul_comm mul_distribute_4 mul_distribute_5 mul_literals mult_eq_1_iff mult_eq_self_iff mult_leq_0_iff mult_less_0_iff mult_neg mult_pos mult_pos_neg multiply_2_inEq0 multiply_2_inEq1 multiply_2_inEq2 multiply_2_inEq3 multiply_distribute_1 multiply_distribute_2 multiply_distribute_3 multiply_eq multiply_inEq0 multiply_inEq1 narrowSelectArrayType narrowSelectType narrowingByteCastBigint narrowingByteCastInt narrowingByteCastLong narrowingByteCastShort narrowingCastFloatToInt narrowingCastFloatToLong narrowingCharCastBigint narrowingCharCastByte narrowingCharCastInt narrowingCharCastLong narrowingCharCastShort narrowingIntCastBigint narrowingIntCastLong narrowingLongCastBigint narrowingShortCastBigint narrowingShortCastInt narrowingShortCastLong neg_literal neq_and neq_and_2 neq_and_3 neq_and_4 neq_or neq_or_2 neq_or_3 neq_or_4 newSym_eq niceDouble niceFloat nnf_ex2all nnf_imp2or nnf_notAll nnf_notAnd nnf_notEqv nnf_notEx nnf_notOr noElementOfSupersetImpliesNoElementOfSubset nonEmptyPermission nonNull nonNullZero notInDomain notLeft notRight nullCreated nullIsNotNonNull null_can_always_be_stored_in_a_reference_type_array observerDependency observerDependencyEQ observerDependencyEquiv observerDependencyFormula onlyCreatedObjectsAreInLocSets onlyCreatedObjectsAreInLocSetsEQ onlyCreatedObjectsAreObserved onlyCreatedObjectsAreObservedInLocSets onlyCreatedObjectsAreObservedInLocSetsEQ onlyCreatedObjectsAreReferenced only_created_objects_are_reachable optAxiom optEmpty orJIntDef orJintInInt orLeft orRight parallelWithSkip1 parallelWithSkip2 partition_inequation passiveMethodCallStatic passiveMethodCallStaticWithAssignment passiveMethodCallWithAssignmentWithinClass passiveMethodCallWithinClass permOwner1 permOwner2 permOwner3 permOwner4 permSlice1 permSlice2 permissionDefaultValue permissionTransferReturnIdentity permissionTransferReturnIdentityEQ polyDiv_pullOut polyDiv_zero polyMod_ltdivDenom polyMod_pullOut polyMod_zero polySimp_addAssoc polySimp_addComm0 polySimp_addComm1 polySimp_addLiterals polySimp_critPair polySimp_elimNeg polySimp_elimOne polySimp_elimOneLeft0 polySimp_elimOneLeft1 polySimp_elimSub polySimp_homoEq polySimp_invertEq polySimp_mulAssoc polySimp_mulComm0 polySimp_mulComm1 polySimp_mulLiterals polySimp_pullOutFactor0 polySimp_pullOutFactor0b polySimp_pullOutFactor1 polySimp_pullOutFactor1b polySimp_pullOutFactor2 polySimp_pullOutFactor2b polySimp_pullOutFactor3 polySimp_pullOutFactor3b polySimp_rightDist polySimp_sepNegMonomial polySimp_sepPosMonomial pos_mult_eq_1_iff postdecrement postdecrement_array postdecrement_assignment postdecrement_assignment_array postdecrement_assignment_attribute postdecrement_attribute postincrement postincrement_array postincrement_assignment postincrement_assignment_array postincrement_assignment_attribute postincrement_attribute pow2InIntLower pow2InIntUpper powAdd powConcrete0 powConcrete1 powDef powGeq1Concrete powIsInfinite1 powIsInfinite2 powIsNaN1 powIsNaN2 powIsNaN3 powIsNotNaN powIsOne powIsZero1 powIsZero2 powLogLess powLogMore2 powMono powMonoConcrete powMonoConcreteRight powPositive powPositiveConcrete powSplitFactor pow_literals precOfDouble precOfFloat precOfInt precOfIntPair precOfPair precOfPairInt precOfSeq predecrement predecrement_array predecrement_assignment predecrement_assignment_array predecrement_assignment_attribute predecrement_attribute preincrement preincrement_array preincrement_assignment preincrement_assignment_array preincrement_assignment_attribute preincrement_attribute prod_empty prod_one pullOut pullOutSelect pullOutbsum1 pullOutbsum2 pull_out_neg_1 pull_out_neg_2 qeq_literals reachAddOne reachAddOne2 reachDefinition reachDependenciesAnon reachDependenciesAnonCoarse reachDependenciesStore reachDependenciesStoreEQ reachDependenciesStoreSimple reachDependenciesStoreSimpleEQ reachDoesNotDependOnCreatedness reachEndOfUniquePath reachEndOfUniquePath2 reachNull reachNull2 reachOne reachUniquePathSameSteps reachZero reach_does_not_depend_on_fresh_locs reach_does_not_depend_on_fresh_locs_EQ readPermission readPermissionAfterTransferRead readPermissionAfterTransferReadEQ readPermissionAfterTransferWrite readPermissionAfterTransferWriteEQ readPermissionEmpty readPermissionObject readPermissionOwe readPermissionOwe2 readPermissionSlice reference_type_cast reference_type_cast reference_type_cast referencedObjectIsCreatedRight referencedObjectIsCreatedRightEQ regExAxiom regExConcatAltLeft regExConcatAltRight regExConcatAxiom regExConcatConcreteStringLeft regExConcatConcreteStringRight regExConcatOptLeft regExConcatOptRight regExConcatRepeatLeft regExConcatRepeatRight removeZeros remove_parentheses_attribute_left remove_parentheses_lhs_left remove_parentheses_right repeatAxiom repeatMatchEmpty repeatOnce repeatPlusAxiom repeatRepeatContraction repeatStarAxiom repeatZero replaceConcat replaceCons replaceDef replaceEmpty replaceSingleton replaceSubstring replace_byte_HALFRANGE replace_byte_MAX replace_byte_MIN replace_byte_RANGE replace_char_MAX replace_char_MIN replace_char_RANGE replace_int_HALFRANGE replace_int_MAX replace_int_MIN replace_int_RANGE replace_known_left replace_known_right replace_long_HALFRANGE replace_long_MAX replace_long_MIN replace_long_RANGE replace_short_HALFRANGE replace_short_MAX replace_short_MIN replace_short_RANGE returnPermissionOwner returnPermission_empty returnPermission_slice returnPermission_slice_split returnUnfold rotate_and rotate_or rotate_params sameTypeFalse sameTypeTrue same_boxes_left same_boxes_right same_diamonds_left same_diamonds_right schiffl_lemma_2 schiffl_thm_1 secondOfPair selectCreatedOfAnon selectCreatedOfAnonAsFormula selectCreatedOfAnonAsFormulaEQ selectCreatedOfAnonEQ selectOfAnon selectOfAnonEQ selectOfCreate selectOfCreateEQ selectOfMemset selectOfMemsetEQ selectOfStore selectOfStoreEQ seqConcatUnfoldLeft seqConcatUnfoldRight seqConcatWithSeqEmpty1 seqConcatWithSeqEmpty2 seqDefOfSeq seqDef_empty seqDef_induction_lower seqDef_induction_lower_concrete seqDef_induction_upper seqDef_induction_upper_concrete seqDef_lower_equals_upper seqDef_one_summand seqDef_split seqDef_split_in_three seqGetAlphaCast seqGetSInvS seqGetUnfoldLeft seqGetUnfoldRight seqIndexOf seqIndexOfUnfoldLeft seqIndexOfUnfoldRight seqLengthUnfold seqNPermComp seqNPermDefLeft seqNPermDefReplace seqNPermEmpty seqNPermInjective seqNPermInvNPermLeft seqNPermInvNPermReplace seqNPermRange seqNPermRight seqNPermSingleton seqNPermSingletonConrete seqNPermSwapNPerm seqOutsideValue seqPermConcatBW seqPermConcatFW seqPermCountsInt seqPermDef seqPermDefLeft seqPermEmpty1 seqPermEmpty2 seqPermExists seqPermForall seqPermFromSwap seqPermRefl seqPermSplit seqPermSym seqPermTrans seqPermTransAlt0 seqPermTransAlt1 seqPermTransAlt2 seqPermTransAlt3 seqReverseOfSeqEmpty seqReverseUnfold seqSelfDefinition seqSelfDefinitionEQ2 seqSingletonUnfold seqSubUnfoldLeft seqSubUnfoldMiddle seqSubUnfoldRight seqSwapPreservesSeqPerm seqSwapPreservesSeqPermEQ seqnormalizeDef sequentialToParallel1 sequentialToParallel2 sequentialToParallel3 setIntersectUnfoldLeft setIntersectUnfoldRight setJavaCardTransient setMinusItself setMinusOfUnion setMinusOfUnionEQ setMinusSingleton setMinusUnfoldLeft setMinusUnfoldRight setMinusWithAllLocs setMinusWithEmpty1 setMinusWithEmpty2 setUnionUnfoldLeft setUnionUnfoldRight shiftLeftDef shiftLeftPositiveShiftDef shiftRightDef shiftRightPositiveShiftDef shift_paren_and shift_paren_or shiftleft_literals shiftright_literals sign_case_distinction simplifyIfThenElseUpdate1 simplifyIfThenElseUpdate2 simplifyIfThenElseUpdate3 simplifyIfThenElseUpdate4 simplifySelectOfAnon simplifySelectOfAnonEQ simplifySelectOfCreate simplifySelectOfCreateEQ simplifySelectOfMemset simplifySelectOfMemsetEQ simplifySelectOfStore simplifySelectOfStoreEQ simplifyUpdate1 simplifyUpdate2 simplifyUpdate3 sinIsNaN sinIsNotNaN sinRange2 sinRange3 sineIsNaNAlt sineIsZero sineRange sineRangeAlt singletonAssignment singletonEqualsEmpty singletonUnfold sizeOfMapEmpty sizeOfMapRemove sizeOfMapSingleton sizeOfMapUpdate sizeOfSeq2Map skipAssert skipAssert_2 sortsDisjoint1 sortsDisjoint2 sortsDisjointModuloNull special_constructor_call splitEquation splitEquationSucc split_or_strong sqrtIsInfinite sqrtIsNaN sqrtIsNotNaN sqrtIsSmaller sqrtIsZero square_nonneg ssubsortDirect ssubsortSup ssubsortTop startsWith staticMethodCall staticMethodCall staticMethodCallStaticViaTypereference staticMethodCallStaticViaTypereference staticMethodCallStaticWithAssignmentViaTypereference staticMethodCallStaticWithAssignmentViaTypereference staticMethodCallWithAssignment staticMethodCallWithAssignment sub subSeqComplete subSeqCompleteSeqDef subSeqCompleteSeqDefEQ subSeqConcat subSeqConcatEQ subSeqEmpty subSeqHeadSeqDef subSeqHeadSeqDefEQ subSeqSingleton subSeqSingleton2 subSeqSingleton2EQ subSeqSingletonEQ subSeqTailEQL subSeqTailEQR subSeqTailL subSeqTailR sub_equations_left sub_equations_right sub_literals sub_sub_elim sub_zero_1 sub_zero_2 subsetOfEmpty subsetOfIntersectWithItSelf1 subsetOfIntersectWithItSelf2 subsetOfIntersectWithItSelfEQ1 subsetOfIntersectWithItSelfEQ2 subsetOfItself subsetOfUnionWithItSelf1 subsetOfUnionWithItSelf2 subsetOfUnionWithItSelfEQ1 subsetOfUnionWithItSelfEQ2 subsetSingletonLeft subsetSingletonLeftEQ subsetSingletonRight subsetSingletonRightEQ subsetToElementOf subsetToElementOfRight subsetUnionLeft subsetUnionLeftEQ subsetWithAllLocs subsetWithAllLocs2 subsetWithEmpty subsetWithSetMinusLeft subsetWithSetMinusLeftEQ subsortTrans subst_to_eq subst_to_eq_for substringSubstring substringSubstring2 sum_empty sum_zero superclasses_of_initialized_classes_are_initialized superclasses_of_initialized_classes_are_prepared swapQuantifiersAll swapQuantifiersEx switch switch_brackets switch_params synchronizedBlockEmpty synchronizedBlockEmpty synchronizedBlockEmpty synchronizedBlockEmpty2 synchronizedBlockEvalSync tanIsNaN tanIsZero theorem_of_archimedes threeBranchLoopScopeInvRuleBox threeBranchLoopScopeInvRuleDia throwBox throwDiamond throwLabel throwLabelBlock throwNull throwUnfold throwUnfoldMore times_minus_one_1 times_minus_one_2 times_one_1 times_one_2 times_zero_1 times_zero_2 transferPermission_empty transferPermission_slice translate# translate0 translate1 translate2 translate3 translate4 translate5 translate6 translate7 translate8 translate9 translateCheckedAddInt translateCheckedAddLong translateCheckedBitwiseAndInt translateCheckedBitwiseAndLong translateCheckedBitwiseNegateInt translateCheckedBitwiseNegateLong translateCheckedBitwiseOrInt translateCheckedBitwiseOrLong translateCheckedBitwiseXOrInt translateCheckedBitwiseXOrLong translateCheckedDivInt translateCheckedDivLong translateCheckedMulInt translateCheckedMulLong translateCheckedShiftLeftInt translateCheckedShiftLeftLong translateCheckedShiftRightInt translateCheckedShiftRightLong translateCheckedSubInt translateCheckedSubLong translateCheckedUnaryMinusInt translateCheckedUnaryMinusLong translateJavaAddDouble translateJavaAddFloat translateJavaAddInt translateJavaAddInt translateJavaAddLong translateJavaAddLong translateJavaBitwiseAndInt translateJavaBitwiseAndInt translateJavaBitwiseAndLong translateJavaBitwiseAndLong translateJavaBitwiseOrInt translateJavaBitwiseOrInt translateJavaBitwiseOrLong translateJavaBitwiseOrLong translateJavaBitwiseXOrInt translateJavaBitwiseXOrInt translateJavaBitwiseXOrLong translateJavaBitwiseXOrLong translateJavaCastByte translateJavaCastByte translateJavaCastChar translateJavaCastChar translateJavaCastInt translateJavaCastInt translateJavaCastLong translateJavaCastLong translateJavaCastShort translateJavaCastShort translateJavaDivDouble translateJavaDivFloat translateJavaDivInt translateJavaDivInt translateJavaDivLong translateJavaDivLong translateJavaMod translateJavaMod translateJavaMulDouble translateJavaMulFloat translateJavaMulInt translateJavaMulInt translateJavaMulLong translateJavaMulLong translateJavaShiftLeftInt translateJavaShiftLeftInt translateJavaShiftLeftLong translateJavaShiftLeftLong translateJavaShiftRightInt translateJavaShiftRightInt translateJavaShiftRightLong translateJavaShiftRightLong translateJavaSubDouble translateJavaSubFloat translateJavaSubInt translateJavaSubInt translateJavaSubLong translateJavaSubLong translateJavaUnaryMinusInt translateJavaUnaryMinusInt translateJavaUnaryMinusLong translateJavaUnaryMinusLong translateJavaUnsignedShiftRightInt translateJavaUnsignedShiftRightLong translateNegLit translatejavaBitwiseNegateInt translatejavaBitwiseNegateInt translatejavaBitwiseNegateLong translatejavaBitwiseNegateLong true_left true_to_not_false tryBreak tryBreakLabel tryCatchFinallyThrow tryCatchThrow tryEmpty tryFinallyBreak tryFinallyBreakLabel tryFinallyEmpty tryFinallyReturn tryFinallyReturnNoValue tryFinallyThrow tryMultipleCatchThrow tryReturn tryReturnNoValue try_continue_1 try_continue_2 try_finally_continue_1 try_finally_continue_2 twoPermissions typeEq typeEqDerived typeEqDerived2 typeStatic unaryMinusBigint unaryMinusDouble unaryMinusFloat unaryMinusInt unaryMinusLong unionEqualsEmpty unionEqualsEmptyEQ unionIntersectItself unionIntersectItself_2 unionIntersectItself_3 unionIntersectItself_4 unionIntersectItself_5 unionIntersectItself_6 unionWithAllLocs unionWithAllLocsRight unionWithEmpty unionWithEmptyRight unionWithItself unionWithSingletonEqualsUnionWithSingleton unionWithSingletonEqualsUnionWithSingleton_2 unsignedShiftRightJintDef unusedLabel unwindLoopScope variableDeclaration variableDeclarationAssign variableDeclarationFinal variableDeclarationFinalAssign variableDeclarationGhost variableDeclarationGhostAssign variableDeclarationMult wd_Constant_Formula wd_Constant_Term wd_Equality_Pred wd_F_Logical_Op_And wd_F_Logical_Op_Cond_Form wd_F_Logical_Op_Eqv wd_F_Logical_Op_ExCond_Form wd_F_Logical_Op_Imp wd_F_Logical_Op_Neg wd_F_Logical_Op_Or wd_F_Logical_Quant_All wd_F_Logical_Quant_Exist wd_F_Resolve wd_F_Subst_Formula wd_Heap_Anon wd_Heap_ArrLength wd_Heap_Create wd_Heap_Memset wd_Heap_Pred_ArrStoreValid wd_Heap_Pred_NonNull wd_Heap_Pred_WellFormed wd_Heap_Reference wd_Heap_Reference_Array wd_Heap_Reference_Created wd_Heap_Reference_Static wd_Heap_Store wd_LocSet_AllElemsArr wd_LocSet_AllElemsArrLocsets wd_LocSet_AllFields wd_LocSet_AllFieldsArr wd_LocSet_AllObjects wd_LocSet_ArrRange wd_LocSet_Diff wd_LocSet_FreshLocs wd_LocSet_InfiniteUnion wd_LocSet_InfiniteUnion2 wd_LocSet_Intersect wd_LocSet_Pred_Disjoint wd_LocSet_Pred_ElementOf wd_LocSet_Pred_ElementOf_Static wd_LocSet_Pred_InHeap wd_LocSet_Pred_Subset wd_LocSet_Singleton wd_LocSet_Singleton_Arr wd_LocSet_Singleton_Quant wd_LocSet_Singleton_Static wd_LocSet_Union wd_Logical_Op_And wd_Logical_Op_And wd_Logical_Op_AndSC wd_Logical_Op_Cond_Expr wd_Logical_Op_Cond_Expr wd_Logical_Op_Cond_Expr wd_Logical_Op_Cond_Form wd_Logical_Op_Cond_Form wd_Logical_Op_Eqv wd_Logical_Op_Eqv wd_Logical_Op_ExCond_Expr wd_Logical_Op_ExCond_Expr wd_Logical_Op_ExCond_Expr wd_Logical_Op_ExCond_Form wd_Logical_Op_ExCond_Form wd_Logical_Op_Imp wd_Logical_Op_Imp wd_Logical_Op_Neg wd_Logical_Op_Neg wd_Logical_Op_Or wd_Logical_Op_Or wd_Logical_Op_OrSC wd_Logical_Quant_All wd_Logical_Quant_All wd_Logical_Quant_Exist wd_Logical_Quant_Exist wd_Numerical_Cast_Byte wd_Numerical_Cast_ByteOverFlow wd_Numerical_Cast_Char wd_Numerical_Cast_CharOverFlow wd_Numerical_Cast_Int wd_Numerical_Cast_IntOverFlow wd_Numerical_Cast_Long wd_Numerical_Cast_LongOverFlow wd_Numerical_Cast_Short wd_Numerical_Cast_ShortOverFlow wd_Numerical_Const wd_Numerical_Const_C wd_Numerical_Const_Z wd_Numerical_Mod_Byte wd_Numerical_Mod_Char wd_Numerical_Mod_Int wd_Numerical_Mod_Long wd_Numerical_Mod_Short wd_Numerical_Op_Add wd_Numerical_Op_AddInt wd_Numerical_Op_AddIntOverFlow wd_Numerical_Op_AddJInt wd_Numerical_Op_AddJLong wd_Numerical_Op_AddLong wd_Numerical_Op_AddLongOverFlow wd_Numerical_Op_AndJInt wd_Numerical_Op_AndJLong wd_Numerical_Op_BitAndInt wd_Numerical_Op_BitAndLong wd_Numerical_Op_BitNegInt wd_Numerical_Op_BitNegLong wd_Numerical_Op_BitOrInt wd_Numerical_Op_BitOrLong wd_Numerical_Op_BitXOrInt wd_Numerical_Op_BitXOrLong wd_Numerical_Op_CheckedAddInt wd_Numerical_Op_CheckedAddLong wd_Numerical_Op_CheckedBitNegInt wd_Numerical_Op_CheckedBitNegLong wd_Numerical_Op_CheckedBitwiseAndInt wd_Numerical_Op_CheckedBitwiseOrInt wd_Numerical_Op_CheckedBitwiseOrLong wd_Numerical_Op_CheckedBitwiseXOrInt wd_Numerical_Op_CheckedBitwiseXOrLong wd_Numerical_Op_CheckedDivInt wd_Numerical_Op_CheckedDivLong wd_Numerical_Op_CheckedMinusInt wd_Numerical_Op_CheckedMinusLong wd_Numerical_Op_CheckedMulInt wd_Numerical_Op_CheckedMulLong wd_Numerical_Op_CheckedShiftLeftInt wd_Numerical_Op_CheckedShiftLeftLong wd_Numerical_Op_CheckedShiftRightInt wd_Numerical_Op_CheckedShiftRightLong wd_Numerical_Op_CheckedSubInt wd_Numerical_Op_CheckedSubLong wd_Numerical_Op_CheckedUShiftRightInt wd_Numerical_Op_CheckedUShiftRightLong wd_Numerical_Op_Div wd_Numerical_Op_DivInt wd_Numerical_Op_DivIntOverFlow wd_Numerical_Op_DivJInt wd_Numerical_Op_DivJLong wd_Numerical_Op_DivLong wd_Numerical_Op_DivLongOverFlow wd_Numerical_Op_JDiv wd_Numerical_Op_JMod wd_Numerical_Op_JavaMod wd_Numerical_Op_JavaModOverFlow wd_Numerical_Op_JavaShiftLeftInt wd_Numerical_Op_JavaShiftLeftLong wd_Numerical_Op_JavaShiftRightInt wd_Numerical_Op_JavaShiftRightLong wd_Numerical_Op_JavaUnsignedShiftRightInt wd_Numerical_Op_JavaUnsignedShiftRightLong wd_Numerical_Op_MinusInt wd_Numerical_Op_MinusIntOverFlow wd_Numerical_Op_MinusJInt wd_Numerical_Op_MinusJLong wd_Numerical_Op_MinusLong wd_Numerical_Op_MinusLongOverFlow wd_Numerical_Op_Mod wd_Numerical_Op_ModJInt wd_Numerical_Op_ModJLong wd_Numerical_Op_Mul wd_Numerical_Op_MulInt wd_Numerical_Op_MulIntOverFlow wd_Numerical_Op_MulJInt wd_Numerical_Op_MulJLong wd_Numerical_Op_MulLong wd_Numerical_Op_MulLongOverFlow wd_Numerical_Op_Neg wd_Numerical_Op_OrJInt wd_Numerical_Op_OrJLong wd_Numerical_Op_ShiftLeftInt wd_Numerical_Op_ShiftLeftLong wd_Numerical_Op_ShiftRightInt wd_Numerical_Op_ShiftRightLong wd_Numerical_Op_Sub wd_Numerical_Op_SubInt wd_Numerical_Op_SubIntOverFlow wd_Numerical_Op_SubJInt wd_Numerical_Op_SubJLong wd_Numerical_Op_SubLong wd_Numerical_Op_SubLongOverFlow wd_Numerical_Op_UShiftRightInt wd_Numerical_Op_UShiftRightLong wd_Numerical_Op_XorJInt wd_Numerical_Op_XorJLong wd_Numerical_Op_checkedBitwiseAndLong wd_Numerical_Pred_Geq wd_Numerical_Pred_Gt wd_Numerical_Pred_InByte wd_Numerical_Pred_InChar wd_Numerical_Pred_InInt wd_Numerical_Pred_InLong wd_Numerical_Pred_InShort wd_Numerical_Pred_Leq wd_Numerical_Pred_Lt wd_Numerical_Pred_WellOrdered wd_Numerical_Pred_inRangeByte wd_Numerical_Pred_inRangeChar wd_Numerical_Pred_inRangeInt wd_Numerical_Pred_inRangeLong wd_Numerical_Pred_inRangeShort wd_Numerical_Quant_Bprod wd_Numerical_Quant_Bsum wd_Numerical_Quant_Max wd_Numerical_Quant_Min wd_Numerical_Quant_Prod wd_Numerical_Quant_Sum wd_Pair wd_Reach_Pred_Acc wd_Reach_Pred_Reach wd_RegEx wd_RegEx_Alt wd_RegEx_Concat wd_RegEx_Opt wd_RegEx_Plus wd_RegEx_Pred_Match wd_RegEx_Repeat wd_RegEx_Star wd_Seq_Concat wd_Seq_Def wd_Seq_Get wd_Seq_IndexOf wd_Seq_Length wd_Seq_NPermInv wd_Seq_Pred_NPerm wd_Seq_Pred_Perm wd_Seq_Remove wd_Seq_Reverse wd_Seq_Singleton wd_Seq_Sub wd_Seq_Swap wd_String_Hash wd_String_IndexOfChar wd_String_IndexOfStr wd_String_LastIndexOfChar wd_String_LastIndexOfStr wd_String_Pred_Contains wd_String_Pred_EndsWith wd_String_Pred_StartsWith wd_String_Replace wd_String_RmvZeros wd_String_Translate wd_Subst_Formula wd_Subst_Term wd_T_Logical_Op_And wd_T_Logical_Op_Cond_Form wd_T_Logical_Op_Eqv wd_T_Logical_Op_ExCond_Form wd_T_Logical_Op_Imp wd_T_Logical_Op_Neg wd_T_Logical_Op_Or wd_T_Logical_Quant_All wd_T_Logical_Quant_Exist wd_T_Resolve wd_T_Subst_Formula wd_Type_Cast wd_Type_ExactInstance wd_Type_Instance wd_Undef_Formula wd_Undef_Term wd_Y_Split wellFormedAnon wellFormedAnonEQ wellFormedCreate wellFormedMemsetArrayObject wellFormedMemsetArrayPrimitive wellFormedStoreArray wellFormedStoreLocSet wellFormedStoreLocSetEQ wellFormedStoreObject wellFormedStoreObjectEQ wellFormedStorePrimitive wellFormedStorePrimitiveArray wellFormedStorePrimitiveEQ wideningCastIntToFloat wideningCastLongToFloat widening_identity_cast_1 widening_identity_cast_10 widening_identity_cast_11 widening_identity_cast_12 widening_identity_cast_13 widening_identity_cast_2 widening_identity_cast_3 widening_identity_cast_4 widening_identity_cast_5 widening_identity_cast_bigint writePermission writePermissionAfterFullTransfer writePermissionAfterFullTransferEQ writePermissionAfterReturn writePermissionAfterReturnEQ writePermissionEmpty writePermissionImpliesReadPermission writePermissionObject writePermissionOtherNoPermissionCurrentRead writePermissionOtherNoPermissionCurrentWrite writePermissionSlice xorJIntDef zadd_left_cancel0 zero_leq_mult_iff zero_less_mult_iff

activeUse adtProgramDecompositionRules assertions bigint binaryAxioms binaryLemmas boolean booleanRules bprod bsum charListHeader charListRules epsilon execRules firstOrderRules floatAssignment2UpdateRules floatHeader floatRules floatRulesAssumeStrictfp floatRulesCommon floatRulesVerifyNormal forLoopRules formulaNormalisationRules freeADT genericRules heap heapRules ifThenElseRules infFlow instanceAllocation intDiv intPow intRules intRulesCheckedSemantics intRulesJavaSemantics intRulesUncheckedSemantics integerAssignment2UpdateRules integerHeader integerRulesCommon integerSimplificationRules java5 javaHeader javaRules ldt locSets locSetsRules loopInvariantRules loopRules loopScopeRules map mapSize optionsDeclarations permission permissionRules precRules propRule reach reachRules regExAxioms regExHeader regExLemma regExLemmaProven regExTheory ruleSetsDeclarations seq seqCoreRules seqEq seqPerm seqPerm2 seqRules soundDefaultContracts standardRules types updateRules wd wdFormulaRules wdGeneralRules wdHeader wdHeapRules wdLocSetRules wdNumericalRules wdReachRules wdRegExRules wdSeqRules wdStringRules wellfound

ABSTRACT ADD ADDPROGVARS ADDRULES ANTECEDENTPOLARITY APPLY_UPDATE_ON_RIGID ASSIGN ASSUMES AT AVOID AXIOMS BOOTCLASSPATH CHOOSECONTRACT CLASSPATH CLOSEGOAL COLON COMMA CONTAINERTYPE CONTAINS_ASSIGNMENT CONTRACTS DATATYPES DEPENDINGON DIFFERENT DIFFERENTFIELDS DISJOINTMODULONULL DISPLAYNAME DOC_COMMENT DOT DOUBLECOLON DROP_EFFECTLESS_ELEMENTARIES DROP_EFFECTLESS_STORES ELEMSORT ELSE ENUM_CONST EQUALS EQUAL_UNIQUE EXP EXTENDS FALSE FIELDTYPE FINAL FIND FORMULA FREE FREELABELIN FUNCTIONS GENERIC GET_FREE_INVARIANT GET_INVARIANT GET_VARIANT GREATER HASLABEL HASSORT HASSUBFORMULAS HAS_ELEMENTARY_SORT HAS_INVARIANT HELPTEXT HEURISTICS HEURISTICSDECL IF IFEX INCLUDE INCLUDELDTS INSEQUENTSTATE INSTANTIATE_GENERIC INVARIANTS IN_TYPE ISARRAY ISARRAYLENGTH ISCONSTANT ISENUMTYPE ISINDUCTVAR ISINSTRICTFP ISLOCALVARIABLE ISMODELFIELD ISOBSERVER ISREFERENCE ISREFERENCEARRAY ISSTATICFIELD ISSUBTYPE ISTHISREFERENCE IS_ABSTRACT_OR_INTERFACE IS_LABELED JAVASOURCE KEYSETTINGS LBRACE LBRACKET LEMMA LESS LPAREN MAXEXPANDMETHOD METADISJOINT MINUS ML_COMMENT MODAILITYGENERIC1 MODAILITYGENERIC2 MODAILITYGENERIC3 MODAILITYGENERIC4 MODAILITYGENERIC5 MODAILITYGENERIC6 MODAILITYGENERIC7 MODALITYB MODALITYBB MODALITYBB_END MODALITYB_END MODALITYD MODALITYD_END MODALITYG_END MODALOPERATOR MODIFIABLE NEW NEWLABEL NEW_DEPENDING_ON NEW_TYPE_OF NODEFAULTCLASSES NONINTERACTIVE NOTFREEIN NOT_ ONEOF OPTIONSDECL PERCENT PLUS PREDICATES PROBLEM PROFILE PROGRAM PROGRAMVARIABLES PROOF PROOFOBLIGATION PROOFSCRIPT PROXY RBRACE RBRACKET REPLACEWITH RPAREN RULES SAME SAMEUPDATELEVEL SAME_OBSERVER SCHEMAVAR SCHEMAVARIABLES SEMI SIMPLIFY_IF_THEN_ELSE_UPDATE SKOLEMFORMULA SKOLEMTERM SLASH SORTS STAR STATIC STATICMETHODREFERENCE STORE_STMT_IN STORE_TERM_IN STRICT SUBST SUCCEDENTPOLARITY TERM TERMLABEL THEN TILDE TRANSFORMERS TRIGGER TRUE TYPEOF UNIQUE UPDATE VARCOND VARIABLE VARIABLES WITHOPTIONS