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

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

To: "pvs-help@xxxxxxxxxxx" <pvs-help@xxxxxxxxxxx>
Subject: [PVS-Help] An error when pvs generates tcc's
From: Thiago Mendonça Ferreira Ramos<thiagomendoncaferreiraramos@xxxxxxxxxxxx>
Date: Tue, 25 Oct 2011 10:20:49 -0700 (PDT)
Cc: "ayala@xxxxxx" <ayala@xxxxxx>
DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=yahoo.com.br; s=s1024;t=1319563249; bh=hbzrMujt+rrb9VJtk4wWn0nUyf0c+9hRd2P3SxAl5es=;h=X-YMail-OSG:Received:X-Mailer:Message-ID:Date:From:Reply-To:Subject:To:Cc:MIME-Version:Content-Type;b=N5/ij44kyZa7oZWr/APGv1yYGzGeJUFsX+tmzy7+gI7ndtNEnsmKjRk0r5W9x5hnlJmNH+M4tHWtsk8I0CExY4vPF353akUM2DdQvY/NwAiNanRDElGyKfVs0uvtxI87pK3/lg4wx1wec6CTHqWxPH+JJB57qD4I5yvp7mpb+So=
DomainKey-Signature: a=rsa-sha1; q=dns; c=nofws; s=s1024; d=yahoo.com.br;h=X-YMail-OSG:Received:X-Mailer:Message-ID:Date:From:Reply-To:Subject:To:Cc:MIME-Version:Content-Type;b=aS1HTOSaGyQUfE2wPA6eRr5gDS3+ksbwQvPEabygNxelpK7o7jmRP1DFpnMQozY/ZB5WwwilyuYcTv5Dd0jDB7fjKm3fKbiKA5oq4gratsk0vFIr2oJZForevwZDORrXvRFbAlN+H3abxfBL5jRstEtkbEMZwQYBtwh3kM7S0ps=;
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>
Reply-To: Thiago Mendonça Ferreira Ramos<thiagomendoncaferreiraramos@xxxxxxxxxxxx>
Sender: pvs-help-bounces+archive=csl.sri.com@xxxxxxxxxxx

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?

Follow-Ups:
- [PVS-Help] Re: An error when pvs generates tcc's
  - From: Thiago Mendonça Ferreira Ramos
- Re: [PVS-Help] An error when pvs generates tcc's
  - From: Sam Owre

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