RODIN / Theories Bug Tracker / #4 XD reasoner: Reasoner fails unexpectedly

#4 XD reasoner: Reasoner fails unexpectedly

Milestone: Theory 4.0

Status: closed

Owner: Son Hoang

Labels: None

Updated: 2020-12-22

Created: 2016-02-23

Creator: Son Hoang

Private: No

In the attached development, the interactive proof for thm1/S-THM will cause the following exception when trying XD
java.lang.IllegalArgumentException: Trying to add an invalid self-referring type: S
This bug is reported by J-R. Abrial via email.

1 Attachments

XD-Bug1.zip

Discussion

Son Hoang - 2016-04-24

The matching facilities are now reimplemented using ISpecialization which is the proper way for instantiate types. This fix will be available in the next release of the Theory plug-in.

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Guillaume Verdier - 2020-11-30

Milestone: Rodin 3.1 --> Theory 4.0
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Guillaume Verdier - 2020-12-22

status: open --> closed
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

Guillaume Verdier - 2020-12-22

This bug has been fixed and can't be reproduced with the latest release.

If you would like to refer to this comment somewhere else in this project, copy and paste the following link:

XD reasoner: Reasoner fails unexpectedly

Milestone

Searches

Help

#4 XD reasoner: Reasoner fails unexpectedly

Discussion