PROBPLUGIN - Disprover does not work with Theory Plugin
Description
Environment
None
Attachments
2
Gliffy Diagrams
Activity
Show:

Sebastian Krings January 27, 2014 at 9:59 AM
seems to work now

Daniel Plagge January 27, 2014 at 7:38 AM
The theory's operators are now added in the type checking. The given should work now. I actually tried another example, so please check if it now works.
Fixed
Details
Details
Assignee

Reporter

Priority
More fields
Story Points, Original estimate
More fields
Story Points, Original estimateCreated January 20, 2014 at 9:19 AM
Updated January 27, 2014 at 9:59 AM
Resolved January 27, 2014 at 9:59 AM
I have just tried the Disprover on a proof obligation involving operators from the Theory plugin.
When trying to prove the PO thm6/THM from “BaumTest” in the project (SequenzenTest.zip) below I get an error message involving “Unknown operator identifier …” messages.