KeYProject/key

Issues

• TestTacletEquality ignores semantic switches

  #3489 opened 8 months ago by WolframPfeifer
  4

• no_state modifier no longer supported

  #3452 opened a year ago by mattulbrich
  1

• JavacExtension does not work with classpath/bootclasspath

  #3513 opened 6 months ago by WolframPfeifer
  2

• Missing spaces in .key files are ignored

  #3538 opened a month ago by mattulbrich
  3

• Ask before closing a proof whose branches are "used" in other proofs

  #3469 opened 10 months ago by unp1
  2

• Location#compareTo(Location) breaks with undefined Location

  #3518 opened 3 months ago by BookWood7th
  4

• Soundness bug: Assignable treatment is wrong

  #3524 opened 3 months ago by mattulbrich
  0

• KeY GUI slows down already at proofs of size 10000

  #3500 opened 4 months ago by unp1
  1

• SMT Translation naming conflicts

  #3455 opened a year ago by BookWood7th
  2

• EqualsModProofIrrelevancy might not be properly working

  #3515 opened 5 months ago by tobias-rnh
  0

• Decrease Log Level of "Duplicate Sort" Warnings

  #3501 opened 6 months ago by WolframPfeifer
  1

• Drag and drop does no longer indicate target formula

  #3378 opened 6 months ago by mattulbrich
  1

• Improved Taclet Options

  #3414 opened 6 months ago by WolframPfeifer
  1

• KeY proofs cannot be replayed if certain labels are present

  #3483 opened 8 months ago by mattulbrich
  5

• Control-C may leave a defunct process

  #3456 opened 7 months ago by mattulbrich
  3

• Follow-up tasks for overflow checking fix (#3353)

  #3487 opened 8 months ago by WolframPfeifer
  1

• Taclet option for checking overflows (in Java code) does not work

  #3352 opened 8 months ago by WolframPfeifer
  0

• Assignable prevents proving the algorithm

  #3362 opened 9 months ago by fab918
  8

• LemmaGenerator

  #3477 opened 9 months ago by wadoon
  0

• Support for JML `TYPE`

  #3407 opened 10 months ago by flo2702
  4

• JML ghost declarations should behave like set statements

  #3466 opened 10 months ago by wadoon
  0

• Missing rule for type of array

  #3389 opened a year ago by WolframPfeifer
  1

• Inifite NullPointerExceptions when proving accessible clause

  #3411 opened 10 months ago by Drodt
  2

• Simple Java program with array creation cannot be sliced

  #3437 opened 10 months ago by FliegendeWurst
  0

• Metadata in KeY proof files

  #3449 opened a year ago by wadoon
  0

• JML Assert Statement Mutable During Proving

  #3300 opened a year ago by unp1
  1

• Broken link in README.md

  #3442 opened a year ago by Ao-senXiong
  1

• KeY crashes after initial launch terminates unconventionally

  #3416 opened a year ago by BookWood7th
  3

• Poor error message for simple syntax error

  #3441 opened a year ago by FliegendeWurst
  0

• Proof independent settings seem to be no longer saved

  #3366 opened a year ago by unp1
  5

• Make the proof tree (or the KeY GUI in general) responsive during automatic proof search

  #3415 opened a year ago by WolframPfeifer
  0

• Do not update proof tree if not visible

  #3410 opened a year ago by unp1
  0

• User-defined sorts cannot be referenced in quantified expressions

  #3404 opened a year ago by mattulbrich
  1

• SourceView does not highlight symbolically executed statements (sometimes)

  #3342 opened a year ago by unp1
  0

• Allow pausing of cache replay for a specific proof

  #3351 opened a year ago by unp1
  1

• Generic sort in problem definition leads to broken sequent

  #3409 opened a year ago by WolframPfeifer
  0

• Reverse Origin Lookup

  #3354 opened a year ago by unp1
  1

• Userdefined \sorts can't be used in .java files

  #3402 opened a year ago by FabianKof
  0

• Function symbols with clashing names are not detected

  #3403 opened a year ago by mattulbrich
  1

• KeY-BOOK2: Testgen has diverged from book description

  #3401 opened a year ago by wadoon
  0

• Assignable does not work correctly with Boxed types

  #3364 opened a year ago by fab918
  0

• Proof tree filters not applied correctly

  #3367 opened a year ago by WolframPfeifer
  8

• Be able to edit the source file in the main interface

  #3363 opened a year ago by fab918
  1

• [2.12.1] Solver file Z3_QF.props could not be loaded.

  #3323 opened a year ago by FliegendeWurst
  1

• Switching proofs resets selection

  #3347 opened a year ago by FliegendeWurst
  1

• RuleSet names with more structure

  #3350 opened a year ago by unp1
  0

• Cannot slice proofs with filename matching .+slice[^0-9].+

  #3336 opened a year ago by FliegendeWurst
  0

• Proof Slicer always active

  #3301 opened a year ago by unp1
  2

• Disabling OriginLabels causes proof to crash

  #3315 opened a year ago by unp1
  0

• TacletAppIndex or TermTacletAppIndex becomes corrupted

  #3313 opened a year ago by unp1
  1