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
Sebastian KringsReporter
Michael LeuschelPriority
MajorMore 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.