Re: "assertion itheory failed" error

[Sam Owre <owre@csl.sri.com>]

Hi Venkatesh,

Could you send me your files?  I think this is triggering the same
assertion, but for a different reason.

Thanks,
Sam

> I have a bunch of theories that typecheck all by themselves okay. However,
> when I import them in another theory, I get a message "Error: the
> assertion itheory failed." I am not sure whether this is something that I
> could fix on my part, and wanted to confirm this. There wasn't any follow
> up on the list after Sam Owre's reply to Marieke Huisman, dated 12 Feb
> 2002, and my situation seems similar. Additionally, PVS says that one of
> the theories is ambiguous.
> 
> Thanks,
> 
> -V
> 
> PS: pvs-3.1, Redhat Linux 9,
> *pvs*
> :bt gives
> 
> Error: the assertion itheory 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 process.
> [1] pvs(16): ;;;
> ; Fast