PROBPLUGIN - Disprover does not work with Theory Plugin

Description

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.

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

Assignee

Reporter

Priority

More fields

Created January 20, 2014 at 9:19 AM
Updated January 27, 2014 at 9:59 AM
Resolved January 27, 2014 at 9:59 AM