exception during strategy execution

[wadoon]

This issue was created at git.key-project.org where the discussions are preserved.

---

• Mantis: MT-1195
• Submitted on: 2012-07-09 by (at)pschmitt
• Updated: 2012-07-09

Description

During the (automatic) proof of the proof obligation in file "problem1.key"
KeY aborts showing with the error message

An exception occurred during strategy execution.
Exception:java.lang.Array.Index.OutOfBoundsException

Steps to reproduce

Load the attached file "problem1.key".
Push start button.

Files

problem1.key

Notes

(at)mulbrich at 2012-07-09

The problem with using the "Z" function is that within KeY at many places every
occurrence of "Z(t)" is translated to the corresponding integer literal. If "t" is
not a literal term, this transformation fails blatantly.

History

• (at)pschmitt -- (NEW_BUG) 2012-07-09

• (at)pschmitt -- (FILE_ADDED) 2012-07-09

• (at)mulbrich -- (BUGNOTE_ADDED) 2012-07-09

• (at)mulbrich -- (NORMAL_TYPE) 2012-07-09

• (at)mulbrich -- (NORMAL_TYPE) 2012-07-09

• (at)mulbrich -- (NORMAL_TYPE) 2012-07-09

Attributes

• Category: Calculus
• Status: CONFIRMED
• Severity: MAJOR
• OS:
• Target Version:
• Resolution: OPEN
• Priority: NORMAL
• Reproducibility: ALWAYS
• Platform:
• Commit: None
• Build:
• Tags []
• Labels: ~Calculus ~Bug ~NORMAL
• Version: 1.6

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:29:03.362Z
• updated_at: 2017-05-29T02:42:32.404Z
• closed_at: None (closed_by: )
• milestone:
• user_notes_count: 0