search

KeYProject / key

KeY Theorem Prover for Deductive Java Verification
https://key-project.org
Other
48 stars 25 forks source link

GoalBackAction undoes one rule app too much for goals closed by SMT #3072

Closed roundEaredSengi closed 1 year ago

roundEaredSengi commented 1 year ago

Description

Applying a GoalBackAction (i.e. Ctrl + Z) on a goal closed by an SMT solver undoes the previous rule app as well.

Reproducible

always

Steps to reproduce

Describe the steps needed to reproduce the issue.

Example:

  1. Open contraposition.key.
  2. Apply impRight somewhere.
  3. Close via SMT.
  4. Apply GoalBackAction (Ctrl + Z).

Expected: The goal is reopened. Actual: The proof goes back to its initial state, i.e. impRight is also undone.

Additional information

FliegendeWurst commented 1 year ago

Fixed in #3233