WaryClashFreeSubst does not work with Anonymous Updates

[wadoon]

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

---

• Mantis: MT-459

• Submitted on: 2005-03-09 by (at)aroth

• Updated: 2005-03-09

• Assigned to: (at)rbubel

Description

Application of WaryClashFreeSubst (and thus application of the all_left taclet) on a term containing an anonymous update results in a term with an empty update instead of the anonymous update.

Steps to reproduce

Load the attached file and look at the last rule application.

Files

0459-bug2.tgz

Notes

(at)rbubel at 2005-03-09

fixed in 0.1482

(at)aroth at 2005-03-09

Vielen Dank!

History

• (at)aroth -- (NEW_BUG) 2005-03-09

• (at)aroth -- (FILE_ADDED) 2005-03-09

• (at)rbubel -- (NORMAL_TYPE) 2005-03-09

• (at)rbubel -- (NORMAL_TYPE) 2005-03-09

• (at)rbubel -- (NORMAL_TYPE) 2005-03-09

• (at)rbubel -- (BUGNOTE_ADDED) 2005-03-09

• (at)aroth -- (NORMAL_TYPE) 2005-03-09

• (at)aroth -- (BUGNOTE_ADDED) 2005-03-09

Attributes

• Category: Prover Core
• Status: CLOSED
• Severity: MAJOR
• OS:
• Target Version:
• Resolution: FIXED
• Priority: NORMAL
• Reproducibility: ALWAYS
• Platform:
• Commit: None
• Build: 0.1478
• Tags []
• Labels: ~Prover Core ~Bug ~NORMAL

---

View in Mantis

---

Information:

• created_at: 2017-05-29T02:44:31.800Z
• updated_at: 2017-05-29T02:44:32.553Z
• closed_at: 2017-05-29T02:44:32.511Z (closed_by: )
• milestone:
• user_notes_count: 0