This bug is confirmed. I've added two new tests to the regression suite.
Actually, this lemma raises an assertion error when assertions are enabled in the JVM. However, by default, assertions are disabled and the predicate prover succeeds, while ignoring the assertion.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
As a quick fix, Java assertions are now always enforced in critical plug-ins (org.event.core, org.event.core.ast, org.event.core.seqprover, org.event.pp, org.event.pptrans), so that such a problem will not happen again.
There still needs to fix this bug at its root.
If you would like to refer to this comment somewhere else in this project, copy and paste the following link:
Context with a proved false theorem
Logged In: YES
user_id=1041912
Originator: NO
This bug is confirmed. I've added two new tests to the regression suite.
Actually, this lemma raises an assertion error when assertions are enabled in the JVM. However, by default, assertions are disabled and the predicate prover succeeds, while ignoring the assertion.
Logged In: YES
user_id=1041912
Originator: NO
As a quick fix, Java assertions are now always enforced in critical plug-ins (org.event.core, org.event.core.ast, org.event.core.seqprover, org.event.pp, org.event.pptrans), so that such a problem will not happen again.
There still needs to fix this bug at its root.