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

Re: [PVS-Help] An error when pvs generates tcc's

To: =?iso-8859-1?Q?Thiago_Mendon=E7a_Ferreira_Ramos?= <thiagomendoncaferreiraramos@xxxxxxxxxxxx>
Subject: Re: [PVS-Help] An error when pvs generates tcc's
From: Sam Owre <owre@xxxxxxxxxxx>
Date: Tue, 25 Oct 2011 11:24:56 -0700
Cc: "ayala@xxxxxx" <ayala@xxxxxx>, "pvs-help@xxxxxxxxxxx" <pvs-help@xxxxxxxxxxx>
Comments: In-reply-to =?iso-8859-1?Q?Thiago_Mendon=E7a_Ferreira_Ramos?=<thiagomendoncaferreiraramos@yahoo.com.br>message dated "Tue, 25 Oct 2011 10:20:49 -0700."
In-reply-to: <1319563249.29098.YahooMailNeo@web45906.mail.sp1.yahoo.com>
List-Help: <mailto:pvs-help-request@csl.sri.com?subject=help>
List-Id: PVS-Help <pvs-help.csl.sri.com>
List-Post: <mailto:pvs-help@csl.sri.com>
List-Subscribe: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=subscribe>
List-Unsubscribe: <http://lists.csl.sri.com/mailman/listinfo/pvs-help>,<mailto:pvs-help-request@csl.sri.com?subject=unsubscribe>
References: <1319563249.29098.YahooMailNeo@web45906.mail.sp1.yahoo.com>
Sender: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

Hi Thiago,

It looks like you found a bug - could you send me your specs so I can
analyze it?

Thanks,
Sam Owre

Thiago MendonÃ§a Ferreira Ramos wrote:

> Hi,
> 
> I am trying generate tcc's in pvs. However, it appears an error message:
> 
> "Error: the assertion (and resolutions (null (cdr resolutions))) failed."
> 
> Unfortunatily, I do not know how solve this problem.
> 
> Could you help me, please?

References:
- [PVS-Help] An error when pvs generates tcc's
  - From: Thiago Mendonça Ferreira Ramos

Prev by Date: [PVS-Help] An error when pvs generates tcc's
Next by Date: [PVS-Help] problem encountered when running PVS 5.0 on Mac air
Prev by thread: [PVS-Help] An error when pvs generates tcc's
Next by thread: [PVS-Help] Re: An error when pvs generates tcc's
Index(es):
- Date
- Thread