Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

IProver tests failing #740

Open
jvierling opened this issue Oct 14, 2019 · 4 comments
Open

IProver tests failing #740

jvierling opened this issue Oct 14, 2019 · 4 comments
Assignees
@jvierling
Labels
Bug 🪲

Comments

@jvierling
Copy link
Contributor

jvierling commented Oct 14, 2019 •
edited

(Commit 479983c) The test case counting 3 fails with the following error:

gapt.formats.tptp.MalformedInputFileException: unknown step c_1212
gapt.formats.tptp.MalformedInputFileException: unknown step c_1212
	at gapt.formats.tptp.TptpProofParser$.$anonfun$parseSteps$6(TptpProofParser.scala:157)
...

It seems that this is due to a bug in iProver. iProver returns a proof that refers to clause c_1212 but this clause is never derived.
@jvierling jvierling self-assigned this Oct 14, 2019
@jvierling
Copy link
Contributor Author

(Commit 1173fbd) For now the test is skipped.

@jvierling jvierling changed the title IProver test "counting 3" failing IProver tests failing Oct 16, 2019
@jvierling
Copy link
Contributor Author

Tests counting 1 and counting 2 also fail with iprover-2018_Jul_24_11h.

jvierling added a commit that referenced this issue Oct 16, 2019
@jvierling
skip some iProver tests
f855068 
Issue #740
@jvierling
Copy link
Contributor Author

Since e88e8a5, tests counting 1 and counting 2 pass with iProver 3.1. Test counting 3 still fails with iProver 3.1.

@quicquid
Copy link
Contributor

quicquid commented Apr 1, 2020

iProver proofs are certainly sometimes incomplete (there are outputs from the CASC competition 2018 that have an incomplete DAG as well). Konstantin is aware of the problem but I don't know how much time he has to work on it.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@jvierling jvierling

Labels
Bug 🪲
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
2 participants
@quicquid @jvierling