Menu

#191 False theorem proved by newPP

V0.8.2
closed-fixed
7
2008-03-26
2008-03-20
No

Under the hypotheses

cst3 : cst1
cst1 <: set1
cst2 <: set1

the false theorem

cst3 : cst2

is proved by "restricted nPP" (v0.8.2 and v0.8.1)

Archive attached.

Discussion

  • Louis Mussat

    Louis Mussat - 2008-03-20

    Context with a proved false theorem

     
  • Farhad Mehta

    Farhad Mehta - 2008-03-23
    • priority: 5 --> 7
    • assigned_to: mehta --> lvoisin
     
  • Laurent Voisin

    Laurent Voisin - 2008-03-25

    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.

     
  • Laurent Voisin

    Laurent Voisin - 2008-03-26

    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.

     
  • Laurent Voisin

    Laurent Voisin - 2008-03-26
    • status: open --> closed-fixed
     

Log in to post a comment.