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

PVS Bug 887


Synopsis:        Error: the assertion (eq (declaration t1) (declaration t2)) failed.
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Thu Jan  6 08:15:00 2005
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  
  --PtCLjYmwOL
  Content-Type: text/plain; charset=us-ascii
  Content-Description: message body text
  Content-Transfer-Encoding: 7bit
  
  Hi,
  
  I get the subject error, when I typecheck the appended file.
  
  Bye,
  
  Hendrik
  
  
  --PtCLjYmwOL
  Content-Type: application/octet-stream
  Content-Disposition: attachment;
  	filename="bug.tar.gz"
  Content-Transfer-Encoding: base64
  
  H4sIAChY3UEAA+1bbW/bRhLOV+tXLFAYoC7MnSU7CZDaDdxGufrOiQ3Hae0aAkHLS5sNRaok1Uj5
  9Tcz+8Ld5VKW3UuLw2k/WNJyd+eZ95mVfD2//ceTrzx2YLx8/pxe956/oNedF0PxKsaTwc7gxcvh
  8z148GRnMHi5t/OEPf/awHDMqzouGXtS88/VqnWwLElWPFeMqNf/kXEN+p/XaZbWy7/Pfl8pgUcP
  UvfeXof+d4c7L3eV/ndf7KL+94aD4RP2pwjx/1z/74qSR8dpVUenZTGrouHVYci+Z6/Y+XLGx/h6
  x4ty2fue36Z5r8dYxvPb+i6axjN4eMyn05jBLGNvizLOsiCD2QyOuzochyyBD1eH7Nl37PtxH97T
  QnVEAEcEST/I+n12oOayPtLIHQL3nR2yFD7lca2JpGy/OZIdTWdZyitJPjdpw1YknwQ4m+Gnfm+U
  37CWXHo9d2r36rxLTgxJFmWd5re+kxir40+84eccOMgbDs74ZF5W6e9cPWUHBP3oLaw6YDtIK2f5
  PMtoepRVnP0QV7xiGTt529vCJ3gavIS9rUmRV0EcsjLDs9UnAlACw/mzAbAsJAOM0zk9+SFN4N07
  HlfzkrNc4E6zh+BmHuCPQE1kFdoOsEctsNJUkdVOU3JYoMNytn/QaT1yXigQ9pL12uTSbE1yD6CG
  YlfUmsXPBOV8LS5DNl3N6GF+Q9NTcJ7c4zQNz3AUsS18ZtpvQNzH+4NAWIx6ASmxOIDYU5hT9hpd
  87sUXPpBOvmuUyUNUSSITij9eW3Ns7VUH89mPL9RQkcWJWVpBGRyGFb4ouZ5lRZ5jFm8BWAQsmzY
  oFC0WTbAU4bgnG/FRKCQDEwjG4JK3r+RmOSZGG2veVZ8Nrb0UaEk/0GYal0MQwyoPcVNJNa7GJkL
  UktoSxJQ0oCFgMjEB2CfGmCVJUp6g/vEYStlKzesbkCcM2PKAXH07vT4aPSB9ba2cvdpmGsZDPA9
  c4ANHw/MQRGDaYO9WhKRyO4BNkQazwwV9nre3Lfbaye/vYekvF2ygBtQP8w1LgHMUVmATEKm2Cr5
  zXzCg52QHcfT65sYrStk8WQyb0IGTIG+ca4viwV1boQpo9P9kFbLzTUkyjZAS9QiREGjtYkIWa5W
  nuTLJtEogUkLbkiQDTcfhzbJlZG94ct2SPJHG4GOJDZxDK7GGhVi/Kaw1zaFx1VBe8hiksU1xK4g
  0+xI4x+vKoNk0UBVg8wFEIVV5SBmSKEZlg9UPyjhh5okPuir0kHVEap6UEIUup/y6TUv19I8um2N
  YlDCF3uDOmSu/nXYZUGzCC3h5MzYhUsNDHk7dmb3086Imqq+RwtYDdbuNxmVQilK1AZpKbgW+Zbq
  ulA0yu6vh0cCaoRB0EQVZNRbDjCrGfHZlV1ZWagMt8AGQSzp0zMVvuX6aFZUaQ051yZ7cnZ4fAyJ
  NGvJBAsfEXsUADPVZCLVGDWPwatTFzgO7QAVO56aR5ksfuvw4e/hPDq1CrcODmTlxu7jg5KSgSq8
  hyXJUZ+SBG1uThXVpydUQaD6mKdoim/iOq4hPumoNBfz+PKatuJCWP82/tSEsG12w5M0TznEA3gw
  z+qY11Uyzz+h2vVZs9+rKIk/Bd42iBKbpwMaNB1Qzv7WnKGam3brhSgBRQ/HD8VUWd/VRXgZ/tKO
  v9eqW8cu+ae4ZFcX2ClfjmHqVk1d4tQvY1z2TZCEt4hdrPuFOretTGThBcxf4MPbIAkW4AoYBg0Q
  NqTDqiomVz+HHch0Znh3enJ2fvT+n/ZJBuKfEcmFhbhh4s7DxHQZxUhc23SQsG9g8zfsDk2HPgXi
  ozQZFzYJv9f7mWdZUszzG34DpgQ1SQ1yZpfdzCwyXlUSUfAZdkdy++urizGqdNm94HIsg9kioGNC
  sRjlfXo2enN1hToeh/R3rDtqWSDFpDJ8zq7VW+OihQ4MgIdfo0EQg6/It9d9TDMq/ejncLheQPFo
  2ewfNvuHuJ9Am5xAab/QkrdYDBreBGvevdGv85tbrHP+ha9TnteCC3cz+zGuInRnV5BCQlKzbRWC
  lR7zxfu4XmWLvm3bAOJzEoEvU9FuwNsm+ZW8qssUbOSq5DGWHPAX9IGVWchEeXZdFBmP83Gw38dd
  W4z9ePghOr88HblMUOko7QFJAkGXTTwXl41FF7TQE8F+uA970TsFp+iYd3GaV1cn5Q0vu+13X5qm
  MDhaHNLf8dj0SMQD3iaeIMgbPgFuK6jvogkSeg0MBgkaIHKsbFVmFSNCJkH+FCqdfXwjMutnRSQQ
  ls1QVLC+qB1b2hfWUyQJ8MlLqBs+J9pXBDKge9xELprTPiGLjZm9Ax/PILSR0dutLvbTwYwKEbn3
  SzMDtIMv4bJPRvKlKHMQQ1FUPMqhJydkBCGw0dJWoZEDaURim+SdaGrYSGMZLgTbD6Phzkl9rCBm
  bwiWsgP2QABtizXexOdSllkwTWQWpE81pkIJxllPzznmRz/HbRD6FpOr3Dk6/PDxbCQuyHC9Xeq4
  VtVUpO9PzpWq6Y7Zsnpks8PqZUohh+vJNok2VZC3ul3vwPK9i/CCfO7UnKUkuJAzF8hPyRPwfJS0
  xZSeBkgHut6CrUBlgfvm0ISU0TWyTUuCU1Br466GzVPCP0ULUKcs9SlQpD/6FMKypFPm13J3PzC3
  +zGq4tI93LO6i1oEBd9v81YrvYCMq04jErMYWtY4iwpUnpAkeoGD151amvdBCybJ3mZ+Jv0i7GLS
  s9qrGKD2B5l08LpTJpOyxDA4jUAetkE6x2kf04JTQehVN5+4U2kQzrMaLkcnqqfWZO3jvbaijweX
  rsX0KmNuLOoWgkDN19ljeA4SMblwyKKANPhknkEErLGENDFaUm5v1yLh01m9tPcryNYRLT6sU9og
  9CEmG95DNCceKBMovTNe8wjbwHQiI5YSocdEYa+yUtNHTlUmvxgbOVq3LLaBaDsVNDV6Pxiz7V6P
  mm3uPjZbFtxBurkcWi2FR0IjbNtsWkCBVeTphL2d5xNsg6p203ghmiu1VJpF29wXoeMkOkBh14gz
  UEUQ4SRdzIo0B2NJbMehhSqWJTNJykouxLV7gGMTGoe1zp/KviIVFSrU5YQoBrAoPz1ZVRLYl6aq
  hCAtrKoWDs90tYCleVrySc1VoOuoyQ2dnap4b6Zr+4ruS7P2i1hLLH4RvSK9NUlHyu3tnGAjM0MD
  bj78eH4SnY1+Pjs6Hz1tH0U+NSsi5dctK3TcoLfVEoRSz/2hAgg5RHxZE7RrIvpWQUyrSC63usYA
  T+2zD/NrbGKjIvG4OFHf18oWW2QODPYJI5b3BmswJ0p+AUOw0Wfeit/h2A4K7RTT21JJBldqBKbi
  mp30jHA0e6hP9W2jtimuJliyq2JaOCPW3SCNNAfhUQiCvlmU16cndN2U1ypidVzNbONXAOBE82Je
  GdGt7WN0on2FYzvXsvXkEi8a7inSPVdv24y+p8G5PBaWrCG+tu44fOHVMOyQKRWSdvMiJ6m+RutG
  c2yZPE66pZL0AunhzRaJIJ3GtxyiIlpRc7FLh7RXyHtBmSYidZhbhNq+SUe204qXATsc2Y9NpBqC
  acBeATb1cDcOk2mHErXGgNRTUjKQbm9Ly3eLidCYyKAyKzl+U1lHSNKOjDreKNrBOtA9BuCVU0uM
  q0VpnENQ3PbHNClHMMgzY66J6aHFITt2G1VLE8pRMKCaMmuJzHInqUV5qP7mwXs6WQxu7jz6HhtZ
  U0+P89TGELsEDvI2zU3XW0uffNtCUnfhTUyVIRamiybMdhUsdjS1IzPWItsdZcv2wwIoPXbiZ1rz
  EtoOkS/kqlAkIpS8/eO00Q8fzz4c/TRiF+5tFF1E0a7m3ikJ9OEhPTJ/Kcd9P40T6zHLdOHpN+Zh
  31FqGzG+C5Wwsb9ukDAFpW9RjDAiR1CHujHPJL0i3hpdJL0VxZ1b/9p25APVlNXQq8sFndjQP2zh
  PAyhik+NUxgKkAc3gdplxg0MTUtg4W7/fshnXA8Cvp4YPfNPB30X3yp0ofN9LSQep2z1IxZC9VoE
  /V5t6spOxfX1WRE/GNTFfaO4e+13XSY8Ypc/ifLmPQ0A++vGeOwaLVI2dD9Kb5twTxLxZK9V6ljT
  /Ft+a3S8bOFyiH1Li0t/NvTA7SZE5b8fY0Cti5GEzKzTw/RR1fMkEb8NYWnF5hUXpv8s6PWOxa3J
  H22ng9Y1jOrCqilomAuYqGIIx0439cruHp27LuvKbO1D7Fs3KRzJK8jk3zkIjpfncVl9StfjXW1e
  i+ltnXuDxl4hbe8fjNUFDn0zTEf5jxE/0Le2j4Wqe1sw5M1DoMMyOZ7oYd/Fk7KwbiuaS1dJObI8
  zPXHLsrMf/fdcAOg+9YNlXtRuCYBz62eh8htMnucBOleg0ZLfkpi2uIMupJs9hXJam9psYsGbJkt
  fkV2Cn6uPThc8QOL67ji8imQEqVVlib11aX8hjrUPxLBpdRnSSUTDPnrFufC0q7O5xCuqCux7y0P
  2C3VC12RBOlRMEm7rNIxNxMYKcSqguVx23RRLe/tkPl2vbgta1hZM6I7SZHgJtNST/viS3fiZkmH
  A9j7L8EdpKhCQ2O9v/pflzbjvzDw///ORodv3o2+Ho3V//+3szPYHTr//zl8Mdjb/P/fnzHwEnpy
  xyefWBKnWcU+p/Ud643KsihfYWPM4qriJf3SNeC/seCGT7JY1HCsHvSdCfxhM57Db/6+CQ+bsRmb
  sRmbsRmbsRmbsRmbsRmbsRmbsRmbsRl/+fgPtRwmLwBQAAA=
  --PtCLjYmwOL--

How-To-Repeat: 

Fix: 
Fixed the cause of the assertion.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools