[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]

[PVS-Help] PVS 5 The assertion lib failed



Hi all
I would know what is the problem "ERROR: the assertion lib failed"
It appears sometimes when I type checked my specifications.
Most of the time it disappears after removing .pvscontext
or pvsbin or changing a .pvs file and re-type checking.

I am using some personal libraries and generic datatypes,
but I cannot provided yet a simple example of the problem.
I don't think I am doing something special with "lib".
I did not see neither something related in Help and Bug list, nor
in the documentations.
This is an annoying problem which seems related to the way PVS
save its information.

In one case, all the above solutions where not successful,
until I cleanup my librairies (removing .pvscontext, pvsbin, *_adt.pvs)
and type-checking the global specification.
Now this trick solves the problem.

regards


Jean-Claude.Royer@mines-nantes.fr
ASCOLA, Mines de Nantes - INRIA
+ 33 2 51 85 82 05