ESCSimplify does not know how to handle arrays

[wadoon]

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

---

• Mantis: MT-222
• Submitted on: 2003-08-01 by (at)rbubel
• Updated: 2006-07-04

Description

when arrays are involved the translation to simplify prints:

sort=java.lang.String, opName=array, opClass=de.uka.ilkd.key.logic.op.ArrayOp
Warning: unknown operator while translating into simplify syntax.
I will quit here.

Files

Notes

(at)aroth at 2004-08-23

Actually it should be possible to translate arrays to Simplify. At least the page http://research.compaq.com/SRC/esc/simplify/Simplify.1.html claims that there are axioms for arrays built into Simplify. And also ESC/Java certainly relies on such a possibility.

(at)rbubel at 2006-07-04

seems to be fixed

History

• (at)rbubel -- (NEW_BUG) 2003-08-01

• (at)aroth -- (BUGNOTE_ADDED) 2004-08-23

• (at)rbubel -- (NORMAL_TYPE) 2006-07-04

• (at)rbubel -- (BUGNOTE_ADDED) 2006-07-04

Attributes

• Category: Prover Core
• Status: CLOSED
• Severity: MINOR
• OS: 2.4.x
• Target Version:
• Resolution: OPEN
• Priority: NORMAL
• Reproducibility: ALWAYS
• Platform: x86
• Commit: None
• Build:
• Tags []
• Labels: ~Prover Core ~Bug ~NORMAL

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:26:16.196Z
• updated_at: 2017-05-29T02:26:17.250Z
• closed_at: 2017-05-29T02:26:17.058Z (closed_by: )
• milestone:
• user_notes_count: 0