PVS‎ > ‎

### bugs

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.