PVS‎ > ‎


I locally document PVS bugs here, before reporting them on PVS Bugs and Suggestions.

Assertion failed with PVS 6.0 while proving wf library

I installed PVS 6.0 Allegro version on top of iMac OS X version 10.9.5. My wf library, that used to prove completely under PVS 5.0, crashes PVS in the course of the proof of tc_math_well_founded theorem in well_founded_tc theory with the Error: the assertion *use-rationals* failed. message.

In order to reproduce the problem, you can run Meta-x pri from the wf_properties root theory, after undumping, or at least do Meta-x tc on well_founded_tc theory and  Meta-x pr on tc_math_well_founded theorem.

Details of the crash upon invoking Meta-x pr on tc_math_well_founded theorem:
tc_math_well_founded.1.1.1 :  

{-1}  co?(sum(l, n), sum(l, 1 + n))(k)
[-2]  (LAMBDA (n: nat): lv(n)`2) = v
[-3]  (LAMBDA (n: nat): lv(n)`1) = l
[-4]  (LAMBDA (n: nat):
         choose({l: posnat, v: [cc(0, l) -> T] |
                   v(0) = u(1 + n) AND v(l) = u(n) AND (FORALL (k: co(0, l)): R(v(k), v(k + 1)))}))
       = lv
{1}   R(v(n)(l(n) + sum(l, n) - 1 - k), v(n)(l(n) + sum(l, n) - k))

Rerunning step: (expand "sum" :if-simplifies t)
Error: the assertion *use-rationals* failed.
  [condition type: simple-error]

Restart actions (select using :continue):
 0: retry assertion.
 1: Return to Top Level (an "abort" restart).
 2: Abort entirely from this (lisp) process.