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

Re: [PVS-Help] PVS 5 The assertion lib failed

Hi Jean-Claude,

Could you send me your specs, including your libraries?  I have an idea
what is going on, but I would like to verify it.


Jean-Claude Royer <Jean-Claude.Royer@mines-nantes.fr> wrote:

> 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