Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Overloaded Operators for KeY lang #3032

Draft
wants to merge 56 commits into
base: main
Choose a base branch
from
Draft

Commits on Feb 4, 2022

  1. allow multi-char operators

    wadoon committed Feb 4, 2022
    Configuration menu
    Copy the full SHA
    fac35af View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    9689360 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    2876402 View commit details
    Browse the repository at this point in the history
  4. change the loopup functions

    wadoon committed Feb 4, 2022
    Configuration menu
    Copy the full SHA
    a30b91e View commit details
    Browse the repository at this point in the history
  5. remove seq +, use annotation

    wadoon committed Feb 4, 2022
    Configuration menu
    Copy the full SHA
    58ab4f0 View commit details
    Browse the repository at this point in the history

Commits on Feb 6, 2022

  1. Configuration menu
    Copy the full SHA
    3790027 View commit details
    Browse the repository at this point in the history
  2. NotationInfo recognizes MixFitInfos

    more operators are allowed
    wadoon committed Feb 6, 2022
    Configuration menu
    Copy the full SHA
    6c4f1a6 View commit details
    Browse the repository at this point in the history
  3. fix clash with <->

    wadoon committed Feb 6, 2022
    Configuration menu
    Copy the full SHA
    d059b75 View commit details
    Browse the repository at this point in the history
  4. minors

    wadoon committed Feb 6, 2022
    Configuration menu
    Copy the full SHA
    eecbccf View commit details
    Browse the repository at this point in the history

Commits on Feb 8, 2022

  1. fixes failing tests

    * do not use relational operator name map
    * fix priorities in lexer (/** is not an operator)
    * requests for prefix/postfix operators in LDT
    wadoon committed Feb 8, 2022
    Configuration menu
    Copy the full SHA
    0222157 View commit details
    Browse the repository at this point in the history
  2. Merge branch 'master' into weigl/overop

    * master:
      Move functionality for relevant Java files from NodeInfo to new class ProofJavaSourceCollection
      fix error in logging formatting strings
      fix the collection of JUnit tests on jenkins
      also show message of the chained cause of the exception in IssueDialog
      allowing [] after parameter names in JML model methods
      Fix potential stack overflow in ExplorationStepsList
      allow arrays and general types in JML. (KeYProject#1681)
      fixes KeYProject#1682
      Add Task runWithProfiler to execute key.ui with the  Java Flight Recoder
      Fix symbex test cases
      Attempt to fix KeYProject#1679
    
    # Conflicts:
    #	key/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java
    wadoon committed Feb 8, 2022
    Configuration menu
    Copy the full SHA
    c3708ae View commit details
    Browse the repository at this point in the history

Commits on Feb 13, 2022

  1. remove prefix from neglit

    wadoon committed Feb 13, 2022
    Configuration menu
    Copy the full SHA
    9baeb5b View commit details
    Browse the repository at this point in the history
  2. Merge branch 'master' into weigl/overop

    * master:
      [floats] optimising float termination rules
      [floats] reconducting a proof
      [floats] missing rules for double assignments
      [floats] re-implementing a Z3FP solver.
      [floats] added missing unary minus
      repairing cast to integer in JML translation.
      [floats] repairing float-cast rules
      [floats] repairing cast to float
      [floats] nasty method call missing
      [floats] introducing overloaded operator handler
      [floats] missing functions in LDT lookup
      Set the interactive flag for builtin rule applications coming from BuiltInRuleMenuItem correctly
      [floats] adapted taclet option explanations
      fixes KeYProject#1627
    
    # Conflicts:
    #	key/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java
    #	key/key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java
    #	key/key.core/src/main/java/de/uka/ilkd/key/speclang/translation/JMLArithmeticHelper.java
    wadoon committed Feb 13, 2022
    Configuration menu
    Copy the full SHA
    fd4963a View commit details
    Browse the repository at this point in the history
  3. add prefix at negDouble

    wadoon committed Feb 13, 2022
    Configuration menu
    Copy the full SHA
    4ff4563 View commit details
    Browse the repository at this point in the history
  4. fix tests, add whitepsaces

    wadoon committed Feb 13, 2022
    Configuration menu
    Copy the full SHA
    b14b741 View commit details
    Browse the repository at this point in the history

Commits on Feb 16, 2022

  1. Merge branch 'master' into weigl/overop

    * master: (37 commits)
      missing NPE check in MasterHandlerTest
      Fix KeYProject#1696 (wrong hash for heapAtPre)
      a two-state method needs the invariant also at pre-state (try to fix KeYProject#1689)
      Fix KeYProject#1690
      Fix failing test case
      Fixed rule "wellFormedStoreObjectEQ"
      [floats] repairing JML interpretation of equality on floats and doubles.
      add comment to find AutoSuite
      fix NPE
      remove test filter
      fix, swap argument in assertEquals
      only recoder uses junit4
      translate the remaining Junit4 parts
      fix merge issues
      hopefully fixing gradle test filters
      new category "owntest" for tests with an own gradle task
      falsely marked as test
      migrate TestTacletEquality
      fix gradle settings, remove autosuite
      try to fix RAP
      ...
    
    # Conflicts:
    #	key/key.core/src/test/java/de/uka/ilkd/key/nparser/ExprTest.java
    wadoon committed Feb 16, 2022
    Configuration menu
    Copy the full SHA
    9b54c0b View commit details
    Browse the repository at this point in the history

Commits on Apr 17, 2022

  1. allow multi-char operators

    wadoon committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    dda6ea1 View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    b9fd5a6 View commit details
    Browse the repository at this point in the history
  3. Configuration menu
    Copy the full SHA
    ab2a6be View commit details
    Browse the repository at this point in the history
  4. change the loopup functions

    wadoon committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    2aa5097 View commit details
    Browse the repository at this point in the history
  5. remove seq +, use annotation

    wadoon committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    75efea8 View commit details
    Browse the repository at this point in the history
  6. Configuration menu
    Copy the full SHA
    36efc6b View commit details
    Browse the repository at this point in the history
  7. NotationInfo recognizes MixFitInfos

    more operators are allowed
    wadoon committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    e7d9172 View commit details
    Browse the repository at this point in the history
  8. fix clash with <->

    wadoon committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    e59b436 View commit details
    Browse the repository at this point in the history
  9. minors

    wadoon committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    c5abd20 View commit details
    Browse the repository at this point in the history
  10. fixes failing tests

    * do not use relational operator name map
    * fix priorities in lexer (/** is not an operator)
    * requests for prefix/postfix operators in LDT
    wadoon committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    241cd20 View commit details
    Browse the repository at this point in the history
  11. remove prefix from neglit

    wadoon committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    41c5fb6 View commit details
    Browse the repository at this point in the history
  12. add prefix at negDouble

    wadoon committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    b388f45 View commit details
    Browse the repository at this point in the history
  13. fix tests, add whitepsaces

    wadoon committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    0f2788b View commit details
    Browse the repository at this point in the history
  14. fix merge

    wadoon committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    dcdaf04 View commit details
    Browse the repository at this point in the history
  15. Merge remote-tracking branch 'origin/weigl/overop' into weigl/overop

    * origin/weigl/overop:
      fix tests, add whitepsaces
      add prefix at negDouble
      remove prefix from neglit
      fixes failing tests
      minors
      fix clash with <->
      NotationInfo recognizes MixFitInfos
      remove old lookup and add metadata
      remove seq +, use annotation
      change the loopup functions
      add MixFitInfo to capture information
      add metadata information to functions and predicates
      allow multi-char operators
    
    # Conflicts:
    #	key/key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java
    #	key/key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java
    wadoon committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    2e48d16 View commit details
    Browse the repository at this point in the history
  16. adts to KeY grammar

    wadoon committed Apr 17, 2022
    Configuration menu
    Copy the full SHA
    9188f0c View commit details
    Browse the repository at this point in the history

Commits on Apr 26, 2022

  1. wip

    wadoon committed Apr 26, 2022
    Configuration menu
    Copy the full SHA
    097994a View commit details
    Browse the repository at this point in the history

Commits on Jun 24, 2022

  1. Merge remote-tracking branch 'origin/master' into weigl/overop

    * origin/master: (112 commits)
      Use generic method correctly
      avoid creating proof obligations in ProofManagementDialog It is unnecessary to create proof obligations in most cases there and creating some proof obligations changes state shared with a large part of KeY (see KeYProject#1715).
      JavaDoc for changed methods + Doubles for timeout
      Checkstyle/SonarQube
      Avoid reopening popup menu when selection button is pressed
      Bug fixes from the IdentityHashMap case study
      Solve missing plugin in shadowJar by adding `mergeServiceFiles()`
      SonarQube
      Checkstyle
      mark JSpinner backgrounds correctly when an error occurs
      Deactivate SMT button when no proof is loaded
      Check formatting  with Spotless
      Add JavaDoc
      Modify problems using solver sockets
      Minor changes
      checkstyle
      Write comments
      Delete solvers.txt (automatically created during build)
      Load solvers.txt from everywhere on classpath
      Fix failing legacy solver test cases by setting different SMT logic
      ...
    wadoon committed Jun 24, 2022
    Configuration menu
    Copy the full SHA
    91abf3d View commit details
    Browse the repository at this point in the history

Commits on Feb 7, 2023

  1. spotless apply

    wadoon committed Feb 7, 2023
    Configuration menu
    Copy the full SHA
    62c5c50 View commit details
    Browse the repository at this point in the history

Commits on Feb 8, 2023

  1. Merge remote-tracking branch 'origin/main' into weigl/overop

    # By Julian Wiesler (149) and others
    # Via Wolfram Pfeifer (25) and others
    * origin/main: (338 commits)
      improving javadoc, removing old code.
      Throw exception with location information on invalid unicode escape sequence
      Move JavaCharStream to the correct folder on build
      Report location on error in constant evaluation
      applying spotless
      small fixes and improvements to proof scripts
      adding features to immutable lists
      Fix javadoc formatting
      Correctly handle unloading proofs
      Formatting and documentation
      ignore class output, add test case
      Javac issues extension: handle non-Java proofs
      Fix construction of Javac issue dialog
      fix typo
      Update tests.yml
      Fix javacc deprecation warning
      Fix branch name in Checkstyle script
      Update feature_request.md
      copy bug-report from gitlab to github
      Update dlsmt.sh
      ...
    
    # Conflicts:
    #	key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/po/TestProgramMethodPO.java
    #	key.core.symbolic_execution/src/test/java/de/uka/ilkd/key/symbolic_execution/testcase/util/TestSymbolicExecutionUtil.java
    #	key.core.testgen/src/main/java/de/uka/ilkd/key/settings/TestGenerationSettings.java
    #	key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ModelGenerator.java
    #	key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ProofInfo.java
    #	key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/ReflectionClassCreator.java
    #	key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/TestCaseGenerator.java
    #	key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleGenerator.java
    #	key.core.testgen/src/main/java/de/uka/ilkd/key/testgen/oracle/OracleMethod.java
    #	key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/TestCE.java
    #	key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/ce/TestCommons.java
    #	key.core.testgen/src/test/java/de/uka/ilkd/key/testcase/smt/testgen/TestTestgen.java
    #	key.core/rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLHandler.java
    #	key.core/rifl/src/main/java/de/uka/ilkd/key/util/rifl/RIFLTransformer.java
    #	key.core/rifl/src/main/java/de/uka/ilkd/key/util/rifl/SecurityLattice.java
    #	key.core/src/main/java/de/uka/ilkd/key/api/KeYApi.java
    #	key.core/src/main/java/de/uka/ilkd/key/api/Matcher.java
    #	key.core/src/main/java/de/uka/ilkd/key/api/ProofManagementApi.java
    #	key.core/src/main/java/de/uka/ilkd/key/api/ScriptApi.java
    #	key.core/src/main/java/de/uka/ilkd/key/api/VariableAssignments.java
    #	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/boollattice/BooleanLattice.java
    #	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/AbstractionPredicate.java
    #	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/ConjunctivePredicateAbstractionDomainElement.java
    #	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/ConjunctivePredicateAbstractionLattice.java
    #	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/DisjunctivePredicateAbstractionDomainElement.java
    #	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/DisjunctivePredicateAbstractionLattice.java
    #	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/SimplePredicateAbstractionDomainElement.java
    #	key.core/src/main/java/de/uka/ilkd/key/axiom_abstraction/predicateabstraction/SimplePredicateAbstractionLattice.java
    #	key.core/src/main/java/de/uka/ilkd/key/control/AbstractProofControl.java
    #	key.core/src/main/java/de/uka/ilkd/key/control/AbstractUserInterfaceControl.java
    #	key.core/src/main/java/de/uka/ilkd/key/control/TermLabelVisibilityManager.java
    #	key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletAssumesModel.java
    #	key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletFindModel.java
    #	key.core/src/main/java/de/uka/ilkd/key/control/instantiation_model/TacletInstantiationModel.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/AbstractFinishAuxiliaryComputationMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/AuxiliaryComputationAutoPilotMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/ExhaustiveProofMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/FinishAuxiliaryBlockComputationMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/FinishAuxiliaryComputationMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/FinishAuxiliaryLoopComputationMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/FullUseInformationFlowContractMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/SelfcompositionStateExpansionMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryBlockComputationMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryComputationMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryLoopComputationMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StartAuxiliaryMethodComputationMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/StateExpansionAndInfFlowContractApplicationMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/macros/UseInformationFlowContractMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/AbstractInfFlowPO.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/BlockExecutionPO.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/IFProofObligationVars.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowContractPO.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/InfFlowProofSymbols.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/LoopInvExecutionPO.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/SymbolicExecutionPO.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicBlockExecutionSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicDependsSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicFreeInvSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicFreePreSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicLoopExecutionSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicLoopInvariantSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicMbyAtPreDefSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicModifiesSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicPOSnippetFactoryImpl.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicPostconditionSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicPreconditionSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSelfCreatedSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSelfExactTypeSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSelfNotNullSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSnippetData.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BasicSymbolicExecutionSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/BlockCallPredicateSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/InfFlowInputOutputRelationSnippet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/InfFlowPOSnippetFactoryImpl.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/po/snippet/ReplaceAndRegisterMethod.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/proof/InfFlowCheckInfo.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/proof/init/StateVars.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/InfFlowContractAppTaclet.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/executor/InfFlowContractAppTacletExecutor.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowContractAppTacletBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowTacletBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/AbstractInfFlowUnfoldTacletBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/BlockInfFlowUnfoldTacletBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowBlockContractTacletBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowLoopInvariantTacletBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/InfFlowMethodContractTacletBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/LoopInfFlowUnfoldTacletBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/informationflow/rule/tacletbuilder/MethodInfFlowUnfoldTacletBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/ContextStatementBlock.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/CreateArrayMethodBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/JavaInfo.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/JavaNonTerminalProgramElement.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/JavaProgramElement.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/JavaReduxFileCollection.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/KeYProgModelInfo.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/Label.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/PrettyPrinter.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeY.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYConverter.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/Recoder2KeYTypeConverter.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeY.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/SchemaRecoder2KeYConverter.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/Services.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/TypeConverter.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/declaration/EnumClassDeclaration.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/declaration/FieldDeclaration.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/declaration/InterfaceDeclaration.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/declaration/MethodDeclaration.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/declaration/ParameterDeclaration.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/declaration/TypeDeclaration.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/declaration/VariableSpecification.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/expression/Operator.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/BinaryOperator.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/expression/operator/DLEmbeddedExpression.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CatchAllStatement.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/Ccatch.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ClassFileDeclarationBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ClassFileDeclarationManager.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ClassPreparationMethodBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ConstructorNormalformBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ContextStatementBlock.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CreateBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/CreateObjectBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/EnumClassBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/EnumClassDeclaration.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExecCtxtSVWrapper.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExecutionContext.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ExpressionSVWrapper.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/Ghost.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/ImplicitFieldAdder.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/InstanceAllocationMethodBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/JMLTransformer.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/KeYCrossReferenceNameInfo.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/LocalClassTransformation.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/MethodBodyStatement.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/MethodCallStatement.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/Model.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/PrepareObjectBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RKeYMetaConstruct.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RKeYMetaConstructExpression.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RKeYMetaConstructType.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RMethodBodyStatement.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RMethodCallStatement.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/RecoderModelTransformer.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SchemaJavaProgramFactory.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/SpecialReferenceWrapper.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/StatementSVWrapper.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/EmptySeqLiteral.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/EmptySetLiteral.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/recoderext/adt/SeqConcat.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/reference/MetaClassReference.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/reference/SchematicFieldReference.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/statement/Ccatch.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/statement/EnhancedFor.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/statement/For.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/statement/JavaStatement.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/statement/JmlAssert.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/statement/TransactionStatement.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/visitor/ContainsStatementVisitor.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/visitor/CreatingASTVisitor.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/visitor/FreeLabelFinder.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/visitor/JavaASTVisitor.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/visitor/OuterBreakContinueAndReturnReplacer.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgVarReplaceVisitor.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramContextAdder.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramReplaceVisitor.java
    #	key.core/src/main/java/de/uka/ilkd/key/java/visitor/ProgramVariableCollector.java
    #	key.core/src/main/java/de/uka/ilkd/key/ldt/DoubleLDT.java
    #	key.core/src/main/java/de/uka/ilkd/key/ldt/FloatLDT.java
    #	key.core/src/main/java/de/uka/ilkd/key/ldt/LDT.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/BoundVarsVisitor.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/DefaultVisitor.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/GenericTermReplacer.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/InnerVariableNamer.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/MethodStackInfo.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/Namespace.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/PosInProgram.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/PosInTerm.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/ProgramPrefix.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/Semisequent.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/Sequent.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/SingleRenamingTable.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/Term.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/TermBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/TermImpl.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/label/BlockContractValidityTermLabelFactory.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabel.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/label/OriginTermLabelFactory.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/label/SingletonLabelFactory.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/label/SymbolicExecutionTermLabelFactory.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/label/TermLabel.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/op/AbstractTermTransformer.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/op/ElementaryUpdate.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/op/LocationVariable.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/op/MixFitInfo.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramConstant.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramMethod.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/op/ProgramSV.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/op/SortDependingFunction.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/op/SubstOp.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/sort/AbstractSort.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/sort/ProgramSVSort.java
    #	key.core/src/main/java/de/uka/ilkd/key/logic/sort/Sort.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/AbstractProofMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/AbstractPropositionalExpansionMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/DoWhileFinallyMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/FinishSymbolicExecutionMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/FinishSymbolicExecutionUntilMergePointMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/FullAutoPilotProofMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/FullPropositionalExpansionMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/PrepareInfFlowContractPreBranchesMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroFinishedInfo.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/ProofMacroListener.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/PropositionalExpansionMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/PropositionalExpansionWithSimplificationMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/SMTPreparationMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/StrategyProofMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/TryCloseMacro.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssertCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AssumeCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AutoCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/AxiomCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/EngineState.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/HideCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/InstantiateCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/JavascriptCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/MacroCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ProofScriptEngine.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RewriteCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/RuleCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SMTCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SaveInstCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SaveNewNameCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptLineParser.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/ScriptNode.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SelectCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/SetCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/TryCloseCommand.java
    #	key.core/src/main/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjector.java
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/DebugKeyLexer.java
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/KeyAst.java
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/KeyIO.java
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/ParsingFacade.java
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/AbstractBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/BuilderHelpers.java
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ChoiceFinder.java
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DeclarationBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/DefaultBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FindProblemInformation.java
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/TacletPBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/varexp/ArgumentType.java
    #	key.core/src/main/java/de/uka/ilkd/key/parser/DefaultTermParser.java
    #	key.core/src/main/java/de/uka/ilkd/key/parser/KeYSemanticException.java
    #	key.core/src/main/java/de/uka/ilkd/key/parser/Location.java
    #	key.core/src/main/java/de/uka/ilkd/key/pp/AbbrevMap.java
    #	key.core/src/main/java/de/uka/ilkd/key/pp/LogicPrinter.java
    #	key.core/src/main/java/de/uka/ilkd/key/pp/PositionTable.java
    #	key.core/src/main/java/de/uka/ilkd/key/pp/SelectPrinter.java
    #	key.core/src/main/java/de/uka/ilkd/key/pp/SequentViewLogicPrinter.java
    #	key.core/src/main/java/de/uka/ilkd/key/pp/StorePrinter.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/Goal.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/InstantiationProposerCollection.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/MultiThreadedTacletIndex.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/Node.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/NodeInfo.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/NodeIterator.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/NullNewRuleListener.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/OpReplacer.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/PrefixTermTacletAppIndexCacheImpl.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/ProgVarReplacer.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/Proof.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/SingleThreadedTacletIndex.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/Statistics.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/SubtreeIterator.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/TermProgramVariableCollector.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/delayedcut/ApplicationCheck.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/delayedcut/DelayedCutProcessor.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractOperationPO.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/init/AbstractPO.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalBlockContractPO.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalLoopContractPO.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/init/FunctionalOperationContractPO.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/init/InitConfig.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/init/JavaProfile.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/init/KeYUserProblemFile.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/init/ProblemInitializer.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/init/ProofObligationVars.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/init/WellDefinednessPO.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/AbstractProblemLoader.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/AutoSaver.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/EnvInput.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/FileRuleSource.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/GZipFileRuleSource.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediatePresentationProofFileParser.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/IntermediateProofReplayer.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/KeYFile.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/OutputStreamProofSaver.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/ProofBundleSaver.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/RuleSourceFactory.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/UrlRuleSource.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/consistency/AbstractFileRepo.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/consistency/DiskFileRepo.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/AppNodeIntermediate.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/BranchNodeIntermediate.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/BuiltInAppIntermediate.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/MergeAppIntermediate.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/io/intermediate/MergePartnerAppIntermediate.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinIsApplicable.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/join/JoinProcessor.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/join/ProspectivePartner.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/mgt/AxiomJustification.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/mgt/ComplexRuleJustificationBySpec.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/mgt/RuleJustificationByAddRules.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/mgt/SpecificationRepository.java
    #	key.core/src/main/java/de/uka/ilkd/key/proof/rulefilter/AnyRuleSetTacletFilter.java
    #	key.core/src/main/java/de/uka/ilkd/key/prover/impl/AbstractProverCore.java
    #	key.core/src/main/java/de/uka/ilkd/key/prover/impl/ApplyStrategy.java
    #	key.core/src/main/java/de/uka/ilkd/key/prover/impl/DefaultTaskFinishedInfo.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractAuxiliaryContractRule.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractBuiltInRuleApp.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractBlockContractRule.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractContractRuleApp.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractBuiltInRuleApp.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopContractRule.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/AbstractLoopInvariantRule.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/AuxiliaryContractBuilders.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractExternalBuiltInRuleApp.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractExternalRule.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/BlockContractInternalRule.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstSeq.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/IfFormulaInstantiationCache.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/JmlAssertRule.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/LightweightSyntacticalReplaceVisitor.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/LoopApplyHeadRule.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractExternalRule.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractInternalBuiltInRuleApp.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/LoopContractInternalRule.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/MatchConditions.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/NoFindTaclet.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/QueryExpand.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/Rule.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/RuleApp.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/RuleSet.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/SVNameCorrespondenceCollector.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/SyntacticalReplaceVisitor.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/TacletAttributes.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractApp.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/UseDependencyContractRule.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/UseOperationContractRule.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/WhileInvariantRule.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/ContainsAssignmentCondition.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FieldTypeToSortCondition.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/FreeLabelInVariableCondition.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/HasLoopInvariantCondition.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LocalVariableCondition.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopFreeInvariantCondition.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/LoopInvariantCondition.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/MayExpandMethodCondition.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/SimplifyIfThenElseUpdateCondition.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeCondition.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/conditions/TypeResolver.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/AntecTacletExecutor.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/FindTacletExecutor.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/RewriteTacletExecutor.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/SuccTacletExecutor.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/executor/javadl/TacletExecutor.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/label/TermLabelRefactoring.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/match/TacletMatcherKit.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/match/legacy/ElementMatcher.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/match/legacy/LegacyTacletMatcher.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/TacletMatchProgram.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/TermNavigator.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/VMTacletMatcher.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/BindVariablesInstruction.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchElementaryUpdateInstruction.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramInstruction.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchProgramSVInstruction.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchSchemaVariableInstruction.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchSortDependingFunctionInstruction.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/match/vm/instructions/MatchTermLabelInstruction.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/merge/CloseAfterMerge.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeProcedure.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRule.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/merge/MergeRuleBuiltInRuleApp.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeIfThenElseAntecedent.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeTotalWeakening.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/merge/procedures/MergeWithLatticeAbstraction.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ArrayBaseInstanceOf.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ArrayLength.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ArrayPostDecl.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ConstructorCall.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateFrameCond.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateObject.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/CreateWellformedCond.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/DoBreak.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnhancedForElimination.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EnumConstantValue.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/EvaluateArgs.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ExpandMethodBody.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ForToWhile.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ForToWhileTransformation.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/InitArrayCreation.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/IntroAtPreDefsOp.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MethodCall.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/MultipleVarDecl.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ObserverEqualityMetaConstruct.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/PostWork.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ProgramTransformer.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/ReattachLoopInvariant.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SpecialConstructorCall.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/StaticInitialisation.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/SwitchToIf.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/Unpack.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/UnwindLoop.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformation.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileInvariantTransformer.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/WhileLoopTransformation.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/metaconstruct/arith/Polynomial.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/RewriteTacletBuilderSchemaVarCollector.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletGenerator.java
    #	key.core/src/main/java/de/uka/ilkd/key/rule/tacletbuilder/TacletPrefixBuilder.java
    #	key.core/src/main/java/de/uka/ilkd/key/settings/AbstractPropertiesSettings.java
    #	key.core/src/main/java/de/uka/ilkd/key/settings/PathConfig.java
    #	key.core/src/main/java/de/uka/ilkd/key/settings/ProofIndependentSMTSettings.java
    #	key.core/src/main/java/de/uka/ilkd/key/settings/ProofSettings.java
    #	key.core/src/main/java/de/uka/ilkd/key/settings/StrategySettings.java
    #	key.core/src/main/java/de/uka/ilkd/key/settings/TermLabelSettings.java
    #	key.core/src/main/java/de/uka/ilkd/key/settings/ViewSettings.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/ModelExtractor.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/SMTObjTranslator.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/SMTSolverImplementation.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/SmtLib2Translator.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/communication/LegacyPipe.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/communication/SimplePipe.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/model/Model.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/DefinedSymbolsHandler.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/FieldConstantHandler.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/FloatHandler.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/HandlerUtil.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/IntegerOpHandler.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/ModularSMTLib2Translator.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/QuantifierHandler.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SExpr.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SExprs.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTHandlerServices.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SMTTacletTranslator.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SeqDefHandler.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/SumProdHandler.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/newsmt2/TypeManager.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverPropertiesLoader.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypeImplementation.java
    #	key.core/src/main/java/de/uka/ilkd/key/smt/solvertypes/SolverTypes.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/AbstractAuxiliaryContractImpl.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/AuxiliaryContract.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/BlockContractImpl.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/BlockWellDefinedness.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/ClassAxiomImpl.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/ClassInvariantImpl.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/ClassWellDefinedness.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/ContractAxiom.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/ContractFactory.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/DependencyContractImpl.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalAuxiliaryContract.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/FunctionalOperationContractImpl.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/InitiallyClauseImpl.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/LoopContractImpl.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/LoopSpecImpl.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/LoopWellDefinedness.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/MethodWellDefinedness.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/PartialInvAxiom.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/PositionedString.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/PredicateAbstractionMergeContract.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/QueryAxiom.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/RepresentsAxiom.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/SLEnvInput.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/StatementWellDefinedness.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/WellDefinednessCheck.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLSpecExtractor.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/JMLUtils.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLClassAxiom.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLClassInv.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLConstruct.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLDepends.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLFieldDecl.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLLoopSpec.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMergePointDecl.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLMethodDecl.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLRepresents.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSetStatement.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLSpecCase.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/JMLSpecFactory.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/jml/translation/ProgramVariableCollection.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/ContractClauses.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/DebugJmlLexer.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlChecks.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlIO.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlMarkerDecision.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/JmlTermFactory.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/LDTHandler.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/OverloadedOperatorHandler.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/TextualTranslator.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/njml/Translator.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLExceptionFactory.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLExpression.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLResolverManager.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLTranslationException.java
    #	key.core/src/main/java/de/uka/ilkd/key/speclang/translation/SLTypeResolver.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/ArithTermFeatures.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/FindTacletAppContainer.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/FocussedBreakpointRuleApplicationManager.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/FocussedRuleApplicationManager.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/FormulaTermFeatures.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiationCachePool.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/IfInstantiator.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/IsInRangeProvable.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/NumberRuleAppCost.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/QueueRuleApplicationManager.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/StaticFeatureCollection.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/StrategyProperties.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/AtomsSmallerThanFeature.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DependencyContractFeature.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/DiffFindAndIfFeature.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/FocusIsSubFormulaOfInfFlowContractAppFeature.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/IfThenElseMalusFeature.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ImplicitCastNecessary.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/InfFlowContractAppFeature.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/MergeRuleFeature.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/NoSelfApplicationFeature.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/QueryExpandCost.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/SetsSmallerThanFeature.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/ThrownExceptionFeature.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/feature/TriggerVarInstantiatedFeature.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ClausesGraph.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ConstraintAwareSyntacticalReplaceVisitor.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/ExistentiallyConnectedFormulasFeature.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HandleArith.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/HeuristicInstantiation.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/MultiTrigger.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/PredictCostProver.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TriggersSet.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/TwoSidedMatching.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/quantifierHeuristics/UniTrigger.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/MonomialColumnOp.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/termProjection/TriggerVariableInstantiationProjection.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/termfeature/ConstantTermFeature.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/termfeature/ContainsExecutableCodeTermFeature.java
    #	key.core/src/main/java/de/uka/ilkd/key/strategy/termgenerator/TriggeredInstantiations.java
    #	key.core/src/main/java/de/uka/ilkd/key/taclettranslation/assumptions/AssumptionGenerator.java
    #	key.core/src/main/java/de/uka/ilkd/key/taclettranslation/assumptions/GenericTranslator.java
    #	key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletLoader.java
    #	key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletProofObligationInput.java
    #	key.core/src/main/java/de/uka/ilkd/key/taclettranslation/lemma/TacletSoundnessPOLoader.java
    #	key.core/src/main/java/de/uka/ilkd/key/util/Assert.java
    #	key.core/src/main/java/de/uka/ilkd/key/util/ExceptionTools.java
    #	key.core/src/main/java/de/uka/ilkd/key/util/InfFlowProgVarRenamer.java
    #	key.core/src/main/java/de/uka/ilkd/key/util/InfFlowSpec.java
    #	key.core/src/main/java/de/uka/ilkd/key/util/KeYResourceManager.java
    #	key.core/src/main/java/de/uka/ilkd/key/util/MiscTools.java
    #	key.core/src/main/java/de/uka/ilkd/key/util/Pair.java
    #	key.core/src/main/java/de/uka/ilkd/key/util/Position.java
    #	key.core/src/main/java/de/uka/ilkd/key/util/ProofStarter.java
    #	key.core/src/main/java/de/uka/ilkd/key/util/mergerule/MergeRuleUtils.java
    #	key.core/src/main/java/de/uka/ilkd/key/util/mergerule/SymbolicExecutionState.java
    #	key.core/src/main/java/de/uka/ilkd/key/util/mergerule/SymbolicExecutionStateWithProgCnt.java
    #	key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingException.java
    #	key.core/src/main/java/de/uka/ilkd/key/util/parsing/BuildingIssue.java
    #	key.core/src/main/java/de/uka/ilkd/key/util/parsing/SyntaxErrorReporter.java
    #	key.core/src/main/java/recoder/service/KeYCrossReferenceSourceInfo.java
    #	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatRules.key
    #	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/floatRulesVerifyNormal.key
    #	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heap.key
    #	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/heapRules.key
    #	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSets.key
    #	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/locSetsRules.key
    #	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/mapSize.key
    #	key.core/src/main/resources/de/uka/ilkd/key/proof/rules/seq.key
    #	key.core/src/test/java/de/uka/ilkd/key/java/ProofJavaProgramFactoryTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/java/TestJavaCardDLJavaExtensions.java
    #	key.core/src/test/java/de/uka/ilkd/key/java/TestJavaInfo.java
    #	key.core/src/test/java/de/uka/ilkd/key/java/TestKeYRecoderMapping.java
    #	key.core/src/test/java/de/uka/ilkd/key/java/recoderext/TestEnumClassDeclaration.java
    #	key.core/src/test/java/de/uka/ilkd/key/java/visitor/TestDeclarationProgramVariableCollector.java
    #	key.core/src/test/java/de/uka/ilkd/key/logic/LabeledTermImplTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/logic/TestLocalSymbols.java
    #	key.core/src/test/java/de/uka/ilkd/key/logic/TestPosInTerm.java
    #	key.core/src/test/java/de/uka/ilkd/key/logic/TestTerm.java
    #	key.core/src/test/java/de/uka/ilkd/key/logic/TestTermBuilder.java
    #	key.core/src/test/java/de/uka/ilkd/key/macros/scripts/ScriptLineParserTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/macros/scripts/TestProofScriptCommand.java
    #	key.core/src/test/java/de/uka/ilkd/key/macros/scripts/meta/RewriteTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/macros/scripts/meta/ValueInjectorTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/nparser/TestTacletEquality.java
    #	key.core/src/test/java/de/uka/ilkd/key/parser/AbstractTestTermParser.java
    #	key.core/src/test/java/de/uka/ilkd/key/parser/TestDeclParser.java
    #	key.core/src/test/java/de/uka/ilkd/key/parser/TestJMLParserAssociativity.java
    #	key.core/src/test/java/de/uka/ilkd/key/parser/TestParser.java
    #	key.core/src/test/java/de/uka/ilkd/key/parser/TestTacletParser.java
    #	key.core/src/test/java/de/uka/ilkd/key/parser/TestTermParser.java
    #	key.core/src/test/java/de/uka/ilkd/key/parser/TestTermParserHeap.java
    #	key.core/src/test/java/de/uka/ilkd/key/parser/TestTermParserSorts.java
    #	key.core/src/test/java/de/uka/ilkd/key/parser/messages/ParserMessageTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/TestGoal.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/io/TestZipProofSaving.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/io/consistency/TestProofBundleIO.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/proverules/ProveRulesTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/GenerateUnitTests.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/ProveTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/RunAllProofsFunctional.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingStrategy.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTable.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/DataRecordingTestFile.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/FunctionPerformanceData.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/RuleIndependentData.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/performance/RunAllProofsTestWithComputeCostProfiling.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/ForkedTestFileRunner.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/StatisticsFile.java
    #	key.core/src/test/java/de/uka/ilkd/key/proof/runallproofs/proofcollection/TestFile.java
    #	key.core/src/test/java/de/uka/ilkd/key/rule/TacletForTests.java
    #	key.core/src/test/java/de/uka/ilkd/key/rule/TestApplyTaclet.java
    #	key.core/src/test/java/de/uka/ilkd/key/rule/conditions/TestDropEffectlessElementary.java
    #	key.core/src/test/java/de/uka/ilkd/key/rule/loop/LoopScopeInvRuleTests.java
    #	key.core/src/test/java/de/uka/ilkd/key/rule/merge/MergeRuleTests.java
    #	key.core/src/test/java/de/uka/ilkd/key/rule/merge/PredicateAbstractionLatticeTests.java
    #	key.core/src/test/java/de/uka/ilkd/key/rule/metaconstruct/TestProgramMetaConstructs.java
    #	key.core/src/test/java/de/uka/ilkd/key/rule/tacletbuilder/TestTacletBuild.java
    #	key.core/src/test/java/de/uka/ilkd/key/smt/communication/BufferedMessageReaderTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/MasterHandlerTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/smt/newsmt2/ProveSMTLemmasTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/smt/test/TestCommons.java
    #	key.core/src/test/java/de/uka/ilkd/key/smt/test/TestCvc4.java
    #	key.core/src/test/java/de/uka/ilkd/key/smt/test/TestZ3.java
    #	key.core/src/test/java/de/uka/ilkd/key/speclang/ContractFactoryTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLPreTranslator.java
    #	key.core/src/test/java/de/uka/ilkd/key/speclang/jml/TestJMLTranslator.java
    #	key.core/src/test/java/de/uka/ilkd/key/speclang/jml/pretranslation/TextualJMLAssertStatementTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ClasslevelTranslatorTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/speclang/njml/ContractLoadingTests.java
    #	key.core/src/test/java/de/uka/ilkd/key/speclang/njml/MethodlevelTranslatorTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/speclang/njml/TextualTranslatorTest.java
    #	key.core/src/test/java/de/uka/ilkd/key/util/DesignTests.java
    #	key.core/src/test/java/de/uka/ilkd/key/util/TestMiscTools.java
    #	key.core/src/test/java/de/uka/ilkd/key/util/TestProofStarter.java
    #	key.removegenerics/src/main/java/de/uka/ilkd/key/util/removegenerics/GenericResolutionTransformation.java
    #	key.removegenerics/src/main/java/de/uka/ilkd/key/util/removegenerics/Main.java
    #	key.removegenerics/src/main/java/de/uka/ilkd/key/util/removegenerics/ResolveGenerics.java
    #	key.removegenerics/src/main/java/de/uka/ilkd/key/util/removegenerics/ResolveMemberReference.java
    #	key.removegenerics/src/main/java/de/uka/ilkd/key/util/removegenerics/ResolveTypeDeclaration.java
    #	key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/ResolveGenericClass.java
    #	key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/TestComment.java
    #	key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/TestMemberReference.java
    #	key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/TestMethodDeclaration.java
    #	key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/TestMultipleBounds.java
    #	key.removegenerics/src/test/java/de/uka/ilkd/key/util/removegenerics/TestTypeReference.java
    #	key.ui/src/main/java/de/uka/ilkd/key/core/KeYMediator.java
    #	key.ui/src/main/java/de/uka/ilkd/key/core/KeYSelectionModel.java
    #	key.ui/src/main/java/de/uka/ilkd/key/core/Main.java
    #	key.ui/src/main/java/de/uka/ilkd/key/core/WebstartMain.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/ApplyTacletDialog.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/AutoDismissDialog.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/AuxiliaryContractConfigurator.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/AuxiliaryContractSelectionPanel.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/BlockContractExternalCompletion.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/BlockContractInternalCompletion.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/DependencyContractCompletion.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/ExampleChooser.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/ExceptionDialog.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/GoalList.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/HeatmapOptionsDialog.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeModel.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/InfoTreeNode.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/InfoView.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/InspectorForDecisionPredicates.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/InvariantConfigurator.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/IssueDialog.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooser.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/KeYFileChooserBookmarkPanel.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/KeyboardTacletExtension.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/LogView.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/LoopContractExternalCompletion.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/LoopContractInternalCompletion.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/LoopInvariantRuleCompletion.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/MainStatusLine.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindow.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/MainWindowTabbedPane.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/MaxRuleAppSlider.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/NodeInfoVisualizer.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroMenu.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/ProofMacroWorker.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/ProofManagementDialog.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/ProofScriptWorker.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/ProofSelectionDialog.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/RecentFileMenu.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/SearchBar.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/StrategySelectionView.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/TacletIfSelectionDialog.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/WindowUserInterfaceControl.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/AutoSave.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditMostRecentFileAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EditSourceFileAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/EnsureSourceConsistencyToggleAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalSelectAboveAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/GoalSelectBelowAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HeatmapToggleAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/HidePackagePrefixToggleAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/LicenseAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/MacroKeyBinding.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenFileAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenMostRecentFileAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/OpenSingleJavaFileAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ProofScriptInputAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/RightMouseClickToggleAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/RunAllProofsAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SMTInvokeAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SaveBundleAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SendFeedbackAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SettingsTreeModel.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowActiveSettingsAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowKnownTypesAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/ShowProofStatistics.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SyntaxHighlightingToggleAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/SystemInfoAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TacletOptionsAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/actions/TermLabelMenu.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettings.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/colors/ColorSettingsProvider.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingHelper.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/docking/DockingLayout.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/extension/ExtensionManager.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/extension/api/DefaultContextMenuKind.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/ExtensionSettings.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/HeatmapExt.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/extension/impl/TestExtension.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFactory.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/IconFontSwing.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/fonticons/MaterialDesignRegular.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/KeyStrokeSettings.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/keyshortcuts/ShortcutSettings.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LemmataAutoModeOptions.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/lemmatagenerator/LoadUserTacletsDialog.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/mergerule/MergePartnerSelectionDialog.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/mergerule/MergeRuleCompletion.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/mergerule/MergeRuleMenuItem.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/mergerule/predicateabstraction/AbstractionPredicatesChoiceDialog.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalView.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewListener.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/CurrentGoalViewMenu.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DefaultTacletMenuItem.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/DragNDropInstantiator.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/HTMLSyntaxHighlighter.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InnerNodeView.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/InsertionTacletBrowserMenuItem.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/MainFrame.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/MenuItemForTwoModeRules.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/PosInSequentTransferable.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentHideWarningBorder.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentView.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewInputListener.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewMenu.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/SequentViewSearchBar.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/nodeviews/TacletDescriber.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/notification/ProofClosedNotification.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/notification/actions/ExceptionFailureNotificationDialog.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/notification/actions/GeneralFailureJTextPaneDisplay.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/notification/actions/GeneralInformationJTextPaneDisplay.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/notification/actions/ProofClosedJTextPaneDisplay.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelVisualizer.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/OriginTermLabelsExt.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/ShowOriginAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/ToggleOriginHighlightAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/originlabels/ToggleTermOriginTrackingAction.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDiffFrame.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifference.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/proofdiff/ProofDifferenceView.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/DisableGoal.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIOneStepChildTreeNode.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/GUIProofTreeNode.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreePopupFactory.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/prooftree/ProofTreeView.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsDialog.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SettingsUi.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/settings/SimpleSettingsPanel.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/settings/StandardUISettings.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/settings/TacletOptionsSettings.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/smt/DropdownSelectionButton.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/smt/InformationWindow.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/NewTranslationOptions.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SMTSettingsProvider.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/SolverOptions.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TacletTranslationOptions.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/smt/settings/TranslationOptions.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/JavaDocument.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceView.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/SourceViewFrame.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/sourceview/TextLineNumber.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/BracketMatchingTextArea.java
    #	key.ui/src/main/java/de/uka/ilkd/key/gui/utilities/GuiUtilities.java
    #	key.ui/src/main/java/de/uka/ilkd/key/proof/io/ProblemLoader.java
    #	key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleProofObligationSelector.java
    #	key.ui/src/main/java/de/uka/ilkd/key/ui/ConsoleUserInterfaceControl.java
    #	key.ui/src/main/java/de/uka/ilkd/key/ui/MediatorProofControl.java
    #	key.ui/src/main/java/de/uka/ilkd/key/util/CommandLine.java
    #	key.ui/src/main/java/de/uka/ilkd/key/util/PreferenceSaver.java
    #	key.ui/src/main/java/de/uka/ilkd/key/util/XMLResources.java
    #	key.ui/src/test/java/de/uka/ilkd/key/gui/KeyboardTacletTest.java
    #	key.ui/src/test/java/de/uka/ilkd/key/gui/proofdiff/ProofDifferenceTest.java
    #	key.util/src/main/java/org/key_proje…
    wadoon committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    470be0a View commit details
    Browse the repository at this point in the history
  2. spotless

    wadoon committed Feb 8, 2023
    Configuration menu
    Copy the full SHA
    20b3020 View commit details
    Browse the repository at this point in the history

Commits on Jul 23, 2023

  1. Configuration menu
    Copy the full SHA
    29fda88 View commit details
    Browse the repository at this point in the history

Commits on Jul 24, 2023

  1. wip

    wadoon committed Jul 24, 2023
    Configuration menu
    Copy the full SHA
    8f5e534 View commit details
    Browse the repository at this point in the history

Commits on Jul 30, 2023

  1. fix last problems

    wadoon committed Jul 30, 2023
    Configuration menu
    Copy the full SHA
    953a33f View commit details
    Browse the repository at this point in the history
  2. Configuration menu
    Copy the full SHA
    dc11e4c View commit details
    Browse the repository at this point in the history

Commits on Aug 2, 2023

  1. fix parser

    wadoon committed Aug 2, 2023
    Configuration menu
    Copy the full SHA
    06f7acb View commit details
    Browse the repository at this point in the history

Commits on Aug 27, 2023

  1. Merge branch 'main' into weigl/overop

    * main: (109 commits)
      increase spotless version (and thus also eclipse formatter) to fix missing space in instanceof formatting
      Spotless and fix rebase
      Some additional minor fixes and spotlessApply
      Update `collect(Collectors.toList())` to `toList()`
      Introduction of record classes where it seems useful.
      Refactor: Introduce a pattern variable were possible.
      Translate large string concatenations into raw string literal (text blocks)
      update beanshell version in recoder's dependencies
      Switch to Java 17 for KeY-2.14.0
      repair POM generation using afterEvaluate
      Adding license to KeY files
      Adding license to Java files
      add metadata for POM generation and update templates for license headers
      Bump ch.qos.logback:logback-classic from 1.4.8 to 1.4.11
      Fix bug in icon selection
      update samplesIndex.txt
      Repair example index
      better default keyboard shortcuts, corrected docs URL, cleanup
      removing the SmansEtAl example from first touch
      change docking frames dependencies to maven central versions
      ...
    wadoon committed Aug 27, 2023
    Configuration menu
    Copy the full SHA
    ccbe4c1 View commit details
    Browse the repository at this point in the history

Commits on Oct 12, 2023

  1. Configuration menu
    Copy the full SHA
    1247f70 View commit details
    Browse the repository at this point in the history

Commits on Nov 19, 2023

  1. Merge remote-tracking branch 'origin/main' into weigl/overop

    * origin/main: (181 commits)
      Use Amazon's Corretto
      add caching for gradle dependencies
      Update to Java 21 Runtime for testing
      Use pattern matching to avoid cast
      Change default notification setting to unfocused
      Renaming from reviewer suggestion (got lost when splitting the PR)
      Minor cleanup
      Prevent possible NullPointerException.
      Cleanup. Remove last usage of the legacy matcher.
      Check only new terms for well-typedness
      Move static metavariable cache to service caches
      Minor cleanup incl. spotless changes
      Use array of assumes instantiations
      Preparation for parallel prover engine - make Strategies stateless by introducing a specific explicit state object for TermBuffers and the Backtracking Manager   This will allow strategies to execute in parallel
      Update keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/CounterExampleAction.java
      Update keyext.ui.testgen/src/main/java/de/uka/ilkd/key/gui/testgen/TGInfoDialog.java
      Some cleanup and proper switching to automode
      Avoid access of non-private field in synchronized context
      Pruning a closed proof (and reopening it) did not update the proof status in the task tree and also did not select any node/goal.
      Minor clean up
      ...
    
    # Conflicts:
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/ExpressionBuilder.java
    wadoon committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    2b5d499 View commit details
    Browse the repository at this point in the history
  2. fix compile errors & spotless

    wadoon committed Nov 19, 2023
    Configuration menu
    Copy the full SHA
    ea65e16 View commit details
    Browse the repository at this point in the history

Commits on Nov 27, 2023

  1. Configuration menu
    Copy the full SHA
    f9975f2 View commit details
    Browse the repository at this point in the history

Commits on Dec 16, 2023

  1. Configuration menu
    Copy the full SHA
    48ca4e7 View commit details
    Browse the repository at this point in the history

Commits on Dec 29, 2023

  1. Configuration menu
    Copy the full SHA
    a723d29 View commit details
    Browse the repository at this point in the history
  2. fix merge error

    wadoon committed Dec 29, 2023
    Configuration menu
    Copy the full SHA
    77eab70 View commit details
    Browse the repository at this point in the history
  3. Merge remote-tracking branch 'origin/main' into weigl/overop

    * origin/main:
      spotless
      after discussion: all datatypes are free
      ignore files in */antlr4/gen/*
      adding example file for natural numbers as ADTs
      spotless
      fix merge errors
      no spaces in displaynames of taclets
      fix spaces in origin label manually + spotless
      add an example for case distinction
      add list example with two proofs
      solve double declaration of sorts, functions and taclets
      solve that taclets are unknown
      better printing
      revival of ADTs
      grammar and taclet generation
    
    # Conflicts:
    #	key.core/src/main/antlr4/KeYLexer.g4
    #	key.core/src/main/antlr4/KeYParser.g4
    #	key.core/src/main/antlr4/gen/KeYLexer.java
    wadoon committed Dec 29, 2023
    Configuration menu
    Copy the full SHA
    4c44e9a View commit details
    Browse the repository at this point in the history
  4. fix merge error

    wadoon committed Dec 29, 2023
    Configuration menu
    Copy the full SHA
    9c1dd90 View commit details
    Browse the repository at this point in the history
  5. wip

    wadoon committed Dec 29, 2023
    Configuration menu
    Copy the full SHA
    bbe9db4 View commit details
    Browse the repository at this point in the history

Commits on Feb 3, 2024

  1. Merge branch 'main' into weigl/overop

    # By Alexander Weigl (4) and others
    # Via GitHub
    * main:
      Bump com.diffplug.spotless from 6.24.0 to 6.25.0
      Bump com.diffplug.spotless from 6.23.3 to 6.24.0
      Bump org.slf4j:slf4j-api from 2.0.10 to 2.0.11
      Bump org.slf4j:slf4j-api from 2.0.9 to 2.0.10
      spotless reformat
      automatical translate package.html to package-info.java
      Treat duplicate predicate declarations as error.
      Fix TestTermParser to avoid multiple parsing of declarations
      implement the discussion of KaKeY
      fix passing of warnings
    
    # Conflicts:
    #	key.core/src/main/java/de/uka/ilkd/key/nparser/builder/FunctionPredicateBuilder.java
    wadoon committed Feb 3, 2024
    Configuration menu
    Copy the full SHA
    8157393 View commit details
    Browse the repository at this point in the history

Commits on Feb 11, 2024

  1. Configuration menu
    Copy the full SHA
    71354b6 View commit details
    Browse the repository at this point in the history

Commits on Feb 18, 2024

  1. Merge remote-tracking branch 'origin/main' into weigl/overop

    * origin/main:
      Bump org.slf4j:slf4j-api from 2.0.11 to 2.0.12
    wadoon committed Feb 18, 2024
    Configuration menu
    Copy the full SHA
    3053fc1 View commit details
    Browse the repository at this point in the history