Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools

PVS Bug 944


Synopsis:        PVS Release Candidate
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Tue Jan 24 13:45:00 2006
Originator:      "Thomas Witkowski"
Organization:    inf.tu-dresden.de
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  ------=_20060102112421_16306
  Content-Type: text/plain; charset="iso-8859-1"
  Content-Transfer-Encoding: 8bit
  
  Hi Sam,
  
  thank you for your message! I've tried some things with the RC. As far as
  I know, Hendrik Tews has written you a mail about which bugs are working
  now. But I've found a further problem when trying to make a theory
  refinement. Can you have a look on the file I've attached to this mail?
  The last line produces a typecheck error because "RF2" is not an
  interpretation of "X". But I think that this should work. What is
  interesting that the problem can be solved when renaming "RF2" into "X".
  
  Regards,
  
  Thomas
  
  
  > Hi Thomas,
  >
  > I have a new release candidate for you to try; it's in
  > ftp://ftp.csl.sri.com/pub/users/owre/pvs3.3-release-candidate/
  > and should fix the bugs you reported.
  >
  > Let me know what you think of it.
  >
  > Regards,
  > Sam
  >
  
  ------=_20060102112421_16306
  Content-Type: application/octet-stream; name="exa04.pvs"
  Content-Transfer-Encoding: base64
  Content-Disposition: attachment; filename="exa04.pvs"
  
  WCA6IFRoZW9yeQpCZWdpbgogIGkxIDogaW50CiAgaTIgOiBpbnQKICBpMyA6IGludAogIGk0IDog
  aW50CgogIGF4MDEgOiBBeGlvbQogICAgaTEgPD0gMTI4CiAgYXgwMiA6IEFYSU9NCiAgICBpMiA8
  PSAyNTYKICBheDA0IDogQVhJT00KICAgIGkzIC89IGk0CkVuZCBYCgolIEZpcnN0IHJlZmluZW1l
  bnQKClhEYXRhMSA6IFRoZW9yeQpCZWdpbgogIGkxIDogaW50ID0gNjQKICBpMiA6IGludCA9IDIw
  MApFbmQgWERhdGExCgpYQXhpb20xIDogVGhlb3J5CkJlZ2luCiAgTXlfWCA6IFRoZW9yeSA9IFgK
  ICBheDAzIDogQVhJT00KICAgIGkxIDw9IGkyCkVuZCBYQXhpb20xCgpYUmVmMSA6IFRoZW9yeQpC
  ZWdpbgogIElNUE9SVElORyBYRGF0YTEKICBSRjEgOiBUaGVvcnkgPSBYe3tpMSA9IFhEYXRhMS5p
  MSwgaTIgPSBYRGF0YTEuaTJ9fQogIElNUE9SVElORyBYQXhpb20xe3tNeV9YIDo9IFJGMX19CkVu
  ZCBYUmVmMQoKJSBTZWNvbmQgcmVmaW5lbWVudAoKWERhdGEyIDogVGhlb3J5CkJlZ2luCiAgaTMg
  OiBpbnQgPSAxMDAKICBpNCA6IGludCA9IDEwMDEKRW5kIFhEYXRhMgoKWEF4aW9tMiA6IFRoZW9y
  eQpCZWdpbgogIE15X1ggOiBUaGVvcnkgPSBYCiAgYXgwNCA6IEFYSU9NCiAgICAgaTQgPiAxMDAw
  CkVuZCBYQXhpb20yCgpYUmVmMiA6IFRoZW9yeQpCZWdpbgogIElNUE9SVElORyBYRGF0YTIKICBJ
  TVBPUlRJTkcgWFJlZjEKCiAgUkYyIDogVGhlb3J5ID0gUkYxe3tpMyA9IFhEYXRhMi5pMywgaTQg
  PSBYRGF0YTIuaTR9fQoKJSBUeXBlY2hlY2sgZXJyb3I6IFJGMiBpcyBub3QgYW4gaW5zdGFuY2Ug
  b2YgWAogIElNUE9SVElORyBYQXhpb20ye3tNeV9YIDo9IFJGMn19CkVuZCBYUmVmMgo=
  ------=_20060102112421_16306--
  

How-To-Repeat: 

Fix: 
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools