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

PVS Bug 1003


Synopsis:        Problem with "some"
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           open
Class:           sw-bug
Arrival-Date:    Fri Aug 31 11:30:01 2007
Originator:      "Alejandro Tamalet"
Organization:    gmail.com
Release:         PVS 4.0
Environment: 
 System:          
 Architecture: 

Description: 
  ------=_Part_9699_23440302.1188574323106
  Content-Type: multipart/alternative; 
  	boundary="----=_Part_9700_24785508.1188574323106"
  
  ------=_Part_9700_24785508.1188574323106
  Content-Type: text/plain; charset=ISO-8859-1
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline
  
  Hi Sam,
  
  I'm having a problem with the function some that is generated for datatypes.
  I define a datatype body with subdatatypes. I want to define a function
  var_names that returns the names of the variables used in a body. If I
  define
  
    var_names2(b : Body) : set[Name] =
      {n : Name | some(LAMBDA (m : Name) : m = n)(b)}
  
  everything works fine except for the case CaseJML, which has as parameter a
  list of tuples. I would expect some to recurse over the list and its
  elements but I can prove that it doesn't:
  
    problem_with_var_names : LEMMA
      FORALL(x : list[[BoolExpr, Stmt]]) :
        var_names2(CaseJML(x)) = emptyset
  
  I enclose the files needed to reproduce this. The function is defined in
  Program.pvs in the theory ProgramFunctions.
  
  
  There is another problem I want to report, but unfortunately I don't know
  how to reproduce it. From time to time I get a TCC about the existence of an
  element of a type that is declared as a non-empty type. For instance,
  recently I got
  
  var_names_TCC1: OBLIGATION EXISTS (x: Name): TRUE;
  
  even when Name is a TYPE+. It is solved by typechecking again or restarting
  PVS. Usually it is not a big deal, but in this case var_names has 33 TCCs
  and the sporadic addition of this TCC shifts the proofs of the others.
  
  
  I using PVS 4.0 - Allegro (Nov 28, 2006 16:50), GNU Emacs 21.4.1 and Ubuntu
  7.04 (Feisty Fawn).
  
  Best regards,
  
  Alejandro Tamalet
  
  ------=_Part_9700_24785508.1188574323106
  Content-Type: text/html; charset=ISO-8859-1
  Content-Transfer-Encoding: 7bit
  Content-Disposition: inline
  
  Hi Sam,<br><br>I&#39;m having a problem with the function some that is genera
 ted for datatypes. I define a datatype body with subdatatypes. I want to defin
 e a function var_names that returns the names of the variables used in a body.
  If I define
  <br><br>&nbsp; var_names2(b : Body) : set[Name] =<br>&nbsp;&nbsp;&nbsp; {n : 
 Name | some(LAMBDA (m : Name) : m = n)(b)}<br><br>everything works fine except
  for the case CaseJML, which has as parameter a list of tuples. I would expect
  some to recurse over the list and its elements but I can prove that it doesn&
 #39;t:
  <br><br>&nbsp; problem_with_var_names : LEMMA<br>&nbsp;&nbsp;&nbsp; FORALL(x 
 : list[[BoolExpr, Stmt]]) :<br>&nbsp;&nbsp;&nbsp;&nbsp;&nbsp; var_names2(CaseJ
 ML(x)) = emptyset<br><br>I enclose the files needed to reproduce this. The fun
 ction is defined in Program.pvs in the theory ProgramFunctions.
  <br><br><br>There is another problem I want to report, but unfortunately I do
 n&#39;t know how to reproduce it. From time to time I get a TCC about the exis
 tence of an element of a type that is declared as a non-empty type. For instan
 ce, recently I got
  <br><br>var_names_TCC1: OBLIGATION EXISTS (x: Name): TRUE;<br><br>even when N
 ame is a TYPE+. It is solved by typechecking again or restarting PVS. Usually 
 it is not a big deal, but in this case var_names has 33 TCCs and the sporadic 
 addition of this TCC shifts the proofs of the others.
  <br><br><br>I using PVS 4.0 - Allegro (Nov 28, 2006 16:50), GNU Emacs 
  21.4.1 and Ubuntu 7.04 (Feisty Fawn).<br><br>Best regards,<br><br>Alejandro T
 amalet<br>
  
  ------=_Part_9700_24785508.1188574323106--
  
  ------=_Part_9699_23440302.1188574323106
  Content-Type: application/x-gzip; name="tamalet.tgz"
  Content-Transfer-Encoding: base64
  Content-Disposition: attachment; filename="tamalet.tgz";
   filename="tamalet.tgz"
  X-Attachment-Id: f_f60ufgjn
  
  H4sIADoz2EYAA+09f2/buJL7tz8FkYdgpTs3iJ0f3S12L0hbpy+LNikSt3uLIjBkmbbVypJXkpN4
  3+t3fzNDUiQlynGaeg8HmEAbm+QMh8PhcDgc0qeL+7NFEuZ789v8hw2lfUjHh4f4t/P8aN/8i+nw
  +PDoh87+8fHxfvfo6BDyO51DyGL7myLITIu8CDLGfghivrLeQ+X/T1POi24c5cWnPnvB+n+8793g
  33/2Lq/+aL3svTm/aLUYU5W8HArHURIVfAB5n/o3PmRc9V59uLo+/9hjAtEN+xVgGDs/Y3w2L5Yn
  Xu5TBqC9YMkijulb7+11j73t9dk9+5WF0zTNOVRss/scvmd8lt5y777Ncp8BEUylME1yylYk3ee+
  wN67eH1+Rp/e9U6vP1z1JNCrIBshBfB199Xlxcce0Hp5USJotXaB1HfvL6/65xdv2Bn17poX58lo
  ERZRmkCHTB4M8mDGBzzmM54UyI+3vXfvTtkue/FM0HF2eXX69i2r8wq6hrwFlknKZnw25Jnq5NmZ
  mVFy3BeUs4vLPvtw3XstSBkIUnjxiPZxrBCsC189swHgd95qtYCBBlda+GeMqmGlaAz5OM24F7TZ
  EEvbLJat1IRjmKYxDxIpHK9Or3vXUPnyTDID5QLqn52CWLRb9mDDGEMRyBOKylBxQzcdUBUtJEYi
  mSOkzmIQQok2aAbvX31ohO6ZHGgmQwsnfKK+OyQ15smkmHqxrxk7GAEroyQsVghaE+8lVou+2EdZ
  f3sOvEcWBshPbI3f8mw5iPIB1A1oIJpam0PZPOMjEujKYMsWCZk396EngF8BKuE3pNygZu7dU7fz
  FGYX0MHvAe2q6bUGHYirJKP3v+fX/esmMk5B9hUJNLWABJTIQZoNUApXEHKfu7hOWoxk+vKqbHsp
  hmlpQ4i6JOtLLCQiaDaWU1DMxsEsmA/klOy0Wb+7Yl6W9UU3G+k3ye8oFQXIx/AXctiz/4F2blw6
  CyelGj2ZOwYOthm06o19oZjLbmjapWoZpGPUS4OHVQzVLtLBIgFt7JVDLZRaRcmITL0A4Qic4Iwq
  JzMtSaKaXoYE6jDIoGq70mA4wtzKIiMnrj1lLbhBvhhCM82Mr3ZE8L5U1TV+G5NFoD6hXJs5FstN
  DuMyVy4hYPG9z9K5g9dJAMtDkUXJxEugGL46VvhwGmQmj0F695sWeBJrBPD2gbMW+mes08DVpGXT
  MoiSzxwW41vuYGdZduJpiHI8urAE5vzPNTF80v2DNZgw3XgGGr+JLmIyWgvNikspAZpZgAOnlmwC
  eWx0Y+zL1ViOU2uD9h/gn2TBbG+ejTfWxmr7v3N8fFTa/1CN7P+D/YOt/f93JO+3/nLO/ZbXuw/n
  Bfx9mY6W8EfKRYt5Gc95dstHg7s0G+WD/qtXHZruroJnHZZEMTs4+Pn50fH+cfeAvno7O2COLoYF
  tPSsCEOfcuEfTQz5ufoPNa6i4kxOrhzImWfpEIzvwV1UTAe3QTZIwB7PBUXuMouoTue4oz52D39C
  AgR5X9I8ms3FVPUoi9/Pg2T0X2ynxNTdYTtq/dhRhp6oHMzn8fIZvy94kgOlQRwVS20KmgjZDtol
  O+xZx5f5QPY8uNdc8c3/lXlcflZ8AyhgPnXAU0SRui2ejXgYQzNAJK4neQnCPN2VatVPF5B9s8Oq
  LDeA0YJnSZpQa89oNPmfAgOSLg18E+L9Ve81q1UccdCmIDdYYNZG0RO1y6qYNQhGhVELuccgCyqN
  Jfmy5R1X9V+tjn4C86uPmleCQIf5nwscrcgiBYw2CwyrtwlIAQOko8P9/gnRlvEwnSTRXzxTGKhz
  VsMOYs/OngR+wSdPgn+VJp+fhKD355PAX0LhxyDr3Qbxk/H07udZXfRcnQ5y/tu7t09q8Hzcn/Kk
  F+f8SWiuQRZ5Ej4VSfE0+C/R/GkIilmB3H8Skv40S++ehiFbvgqKcPokJL9Po/hpw3Gawyr5xBEB
  hq4lymipVhQobQScAk8UkZLLFmGRCpLEarMj7OBPah61GZJwc4OUlvPFb1Bhp8rsLwzt7FSWyiNk
  Lymr1hNco9g4zWZB/KwByrl+EfhPz7udI9Y53GcFy6cp2H1fsECviYZtY+fZFsT+8yNt1hQ8m0Vg
  zUNTjzBtqq12Ha12N97qgaPVg423euho9XDjrR45Wj3aeKvHjlaPN97qc0erzzfe6k+OVn/aeKs/
  O1r9eeOtdvZdamJ/8+061dPm9VPHpaA6m9dQHZeK6mxeR3VcSqqzeS3Vcampzub1VMelqDqb11Qd
  l6rqbF5XdVzKqrN5bdVxqavO5vVV16WvupvXV12Xvur+DfaU06DavL7quvRVd/P6quvSV93N66uu
  S191N6+vui591d28vuq69FV38/qq69JX3c3rq65LX3U3r68OXPrqYPP66sClrw42r68OXPrqYJW+
  crrT8b+Gdh1tOrd/q3TVN7U54cVZxOPRa9igmzvsev5jW36Iw9DC2zQMYkfLlfwNtPwGHQyOliv5
  37tldIMEGR8NbAtDNN9Q6KRBH4w0DXojDfy+GKykY0WF700LNJLnNQKqud9b5me8mKajWrO17O89
  +qKBepPf3suGniopHwhOWhJu5H1vvsZp+mUxH8yK6chos5q74Va7zla/r672W97vPI7P0mzGR9Kj
  6bc2EQdQnv9vLvz3gfP/w8PjzvPy/L9z9JzO/w/2t+f/f0faZdfRbB5H4ygMhL88Slgx5WyWjngc
  JROWjsHKgYx8mRTBPXz18egZhSZ/0dplvwEDWU4HV0UUxGUZFP3O2ShNfiwELhZkWbDMGR6BRwnY
  TeMg5FjtndBRbBrccvYZ0aUJZ/MAsHCoBjXOk4hw3wbxgud4AMDGaDsAsoyzj0HcZklaMDyq2GP9
  aQSdyFmRsuA2jUbiuBl7EiQY68vSbMQz7BZHfNRr/AZE5JxxwMFzPMLP96D2ZRIvWXGXMnFWjUD3
  IZ8Tp14wOqQKhjGnTl0s4vh9Sl3bw74HcZ7KruNxC7WtoeErWSHQqSxCHKIzal1kQUHDMOSTKEnk
  OFAGnhh5cfSF40i9D3LA4StmExtEk1Ey5VlUBEkoqAMxL6KQpbc8i9NgJDHK9YFGOMqYiKUIJaOG
  nO3MgmQS89FOm+1Fe5woCFMQBCklUUKnMcRDYPgoyoPZMJoAV6luQmFnqWpcDloC4ydzZPuiVsaL
  RZYATnEkBTj3bOEIoEq+iDHMYTYHIUmQR8CoCKXKGDqi/o7Gk0SGxGGqvgCd0DPRGB8hhZeLjAWj
  USSGFTLkGdcLGMM4vSNZAuYGwBlASSG5oRCbxMAL7AzYBO27ckyr0h1gyCoG5bXZPBUB3DQ4IBb0
  GcZ+kfMW0kRxOcQLHowQN35vA+UhVmGiNBcsoTAc9oUvMRKHxOLjdUsgeMFen/ZPMbRSB/mdJ4Us
  k59OmJFwuhV8wrMcquIJoKyrPp6YVV/KMzqo+hHn2gv6Y+FTVbEAql3xsUQoP1Uah1ye4SG4Ckmn
  fuBnDFBy9kdPQ2NKnkCBMSOhyPiGhTC+gBLyxYcT2Rw102rhySaFxMjA1P++MZuu90+m38/7/2TX
  H15irWsmzk4vFjPxQR+nQif1uaruyC7WhVmLasFURNArviT1UGrF6C8YcYxzAglQ0kbTF2V1CjIF
  wocIxYxFsQURKitqzbcn5MGLKASRoj3hq2MAIb1QXQGY9/Ei94YdEMiuzkdoLDhxwQAt76LEhFIg
  lH3ibAiA+hHopDoQZTcCvY5u6yCQWe2Y2SX4JINPcE+ciLFHEfBFNRWZomHEmMk5YI4Y5fezBUzY
  M1gGOK1PbZzqbVh+aCSr0zZX8xZ6TNHQffcgWMQriQKgszO8PXH2OKALPvGGRhb1FIOIVgFhlJBm
  rgkq4occQDQi+WfXkOSfT5qaAqi3BasDva3LZwWKu6D46m71/nQAYUDTyqYuuAsMck9WQb1xEfhm
  JYEI5WLGm5XMEBq8WaytiCsDTkh2qYsrsn0h7urgn5Xy9kIpOqH3m8nQhScaRtAgNyg/5hUaTuHT
  JPHAeJ9QlD2iarM8XWQhN9gjqp3IHOQH/q0J/UsRsOTqgpb6EYEWPC8M6DbZOQMkTlZuM3N94DD9
  zVI5T0Z2g2Uzwlx4BXaHV0yKEqPBLxs9A2UyMXVpCW/rRjXhqQuJrbIvmjqv4a4ILtMjKq4FPABX
  HUE0+sS9OWSosLG8YQY26pSX11BqUUfEMRWk90IsmbBolSF3DSOSY9SUqF5lGY2JUU6rnhHCV/ZC
  tqXi8rwcZl/eNaB0xF6VASVo8aCMUsSeA/RLhFc0RDzeWkmDyhA8ryJ4OjSvEZQMKGVIrdWuBpUR
  d16RLUvOh5jjHAfYlYGYLg1u6pA9dwMUjVcfbtoSaSwyZs8GFWF4ih/m1FcBeg3dElYhmoNkll+r
  XbDe6Er5rlmL1t0ahl3X10xhz4o3O0TQdduSztLyvLGyaWiiXEqRmFmXIOiZtiSEGTGJbnnCAtSX
  AezsOc6168WcA6Oy/HyM/6Ok41+Udgvhb8FtUMFHW9kUt8EJhzywLnEC4+YHyaG5xlKiA60a1Thh
  UwTsIfH2bQFm3U2l3soLRf9KJEXs33SziDp9eUWfqRvqC3ZGf8Yu6W/Ysa/lvdkezG7aJOLuOEyz
  jIeFMJNvyXuAlpcazXKDVaDJPeRxChtlqAtfCV3OYUeMO9dROoNNcJtN0zu879hmd7QBhy0/1M6F
  T2VJ3BH+B+1mwF0d+TMEQtSJzCMW3kXQMOC5SxfxSJCHO08Kl8cdbum5kAiiv8iG99GILw9TpAgC
  Hz79g30uxF6LNlG2nJnJXF4aK2GjA1iioaInQ/hPfPYPuh1NrgxYwr+VAJsGiVSsZRa6hwkVy6FJ
  T0NFMCYMTeCaibpqammclXVjsG4q4m0S0wRm6LDVpAj/wVpVlYdhjbrKAbFG1YyW6gf5ANUG5tjL
  MX2FhwOPG9IcZ704VSAbYbySvii5XXOoyFUzqA9XOZMa4KQX61Ewys9mAQn5vpGckcuIxRvqNK+A
  EQsFFK1N6qoWLk867JkcY6CrovkiRg1TKjjYf8rP6E0oyvWrBF29kFnLmLn02cvV7i77kMN6MRbN
  3aK/sf/qVU6uuTI5XlsQvWs/WE8yTyh5aspyg9CFV1YeLnoJt21ec9mhpsx1hy6Ovz199/L1KfNm
  xj5lhpe6fUDmf63gH5rK5MkNDOsNZNw2vp+EP6vjNw3SJ+FWqA3cuWGd1XA/Cnnu07IOQ37af8Fe
  p7hakp+9XCzRTQsmxpcgSxd00gAzIcrJBXbyKLLEjepHEmfLrQmsdjBQi14bEI8kRCO6Wnbj2/IO
  6IN52RTeC6/uiuiZAxuGPUggTMTPg4537/tgKn0bdBeh/XLThs+H+F99a+rT6L/88AZMavKQkAEG
  9hlIcM75LJcOePSF03VN4casW0p00U+eM2ifPI3kHmzXyOAiMwTvyuuLjXJvP1pWh/XRk1AIMlmW
  UYGnIvLOJelWbLThLqq8+00NqlcWVu1uJfeMLqi98T09zqJud9q6t/6IgtDCLUstGbzQt/iFhjeu
  HVmPsgzZ5RmNoxxPcg8jgvLpBHtRNVzBWEvMG4OEjt82Ker6fglad7nSoEV45lQILJRZApBrtIEO
  8oA2lJGjE3EbhGishkfzsT3QXsPHQjoccw90XrrdGrpYd7A9gM7yoCm3BMIEo1GZa2hLUW50QHjS
  VnFVe8wMN1lb+8SMx1oYq3EP4fz2qgoKpcVljd0g1varCYdaGzcLev65GpgUFmqsb4yHcKbZDEh0
  uXSa2eWZwaCKB8zmRvl6SVmsy+yXTCrWV8967Mh6IKRimxqrTPMiw1ypyii9spjsMlYM34FH98wo
  pbdAShZVvHyGa6+tvXirh3AtISI0NSGiXGPAK35A14zP7Rmfdy3w4ttnm/QGNkx+y+FnC5yYH6UC
  le69BjymC0/67trKUffAZM2W0PNqLmGwOKKQGV3Tbj3hy3PxVQ6joWiwoqXMlH/P0f2WlCz18pZ6
  aGbIXv7BfvmlZS+aaAsIfeEyIT5IuzC3yv7NEnzFyZR97s3I0KqVwLZTFknqKxWwa02wYvuvSt3w
  auPfgEPu9bH0q2/3HI/DaQNW6Thb2XP1so3FN0ma3Ph6oQ/tkeFboWZWIwLFXMW8PYL/igqzD5II
  uY3Gt8BCJxFhjYhx4wbfX8t3ab72U8ISKOCWNEBF/AzG5le78XiVA+lx7ccVZxg9Aph7sUFCrEkw
  qRArBmt8v2qMSnBMpyFNfKoatp6Y1QqSjNvqRB9XNCjVE7v81yo2qrrTZ8yKJq9KkJM8xTJrgBrE
  yCFAqzyZlST8RTgDxmL3agWgryDWGnZFb3VAXSS3ma3CGol9RL9qE7mxpkcuUKiFkgXqJ8bXFbMJ
  6RvZfR0F/6ixmqwzVo5OaU8fkj9BMgQdg3IcPDV12qxCETkcXUOBb5cmE+ica0wqY+y7Zpx62BQt
  PfmYwYmHb5dhJpl4i7knX0aFbLmK0ZuTaVGkM7WqnZ+p7pTMeaA7NdbqvlTnQ2Vm+S7t9f07UgrI
  t3ekKiwVsUM50B2ZbKIj9TsOK6S9yUuhYasj4ePWo7QhdLIgLCFcC8JiEkLQpHXf2VizP3VX2uN7
  9a19W6uHptP+wQNINBVaUs1887CuucyQcIZ6gTavkJitgq1uInoEAfZKUadgfb1vJ6J8VqV8FavU
  cYikVROmrZkHuGXRqtYacXJktStDaz4GcalI5KFK+ahlGfp0Qk4AQm+NuG/cIqIqTiXxr5JiYPmq
  4a0g+/qQbtll/cvXly+EdOZzHpYR/NWDbnWgfcfJhYlFMtA6SJaSZYRQulrV4RAdIE0DETmdwc43
  QtNL+E0AVz6lQ2qJCuuMoywvJBZCOI14FmThdIneXHWUJY/AR0vAFIUUV095k2KvJaOFhmDbLWX0
  Oz5oNI3EGfwolXH9MUdvf1SAYpEH0Qhr3Mixp0Y52mAXqRlQDrxXCqbvG+O/mJ94hvD4YogNKVNy
  0Aay7hJHXZDBxC0TpmSbQtGEaE2DU3WkmR6XE6aSSqmkqTtL1hbEd8FyyMVZi3oLVckI5Md8bIwW
  eiVDGkBZA49wCJchTmGafFaIyrgJsvyTQmWQvMKSlBSKj0KIzsfSY/9jgRpmhMETGhhFFEQCatBt
  E9Fmrp75lmIE1RukSMVN0gtzDwiMHn/E1zQymsP9vsldNSEw6gUvkXFgjffLL3QBB/LwzUKsI74N
  RI0ZHQiIiwTlCVd1Q2C/xZ6zX35h2rOAi53I0n6EMk87D+qnEfKhYQdBwm3WuJcExQ47wrBbUhse
  6HMLKbOl701U9ZEYqKaeRC4lO+zIEtLYXfFlJZe+gT6Xp6N5FKqkA7xfJ7wZHsGk82RFpS5WcnQ0
  ygdFFiR51PD6sd1FJ+8lT7sWT8seKI47jqf0g+VV13Jb+27EzyuoHtHT1gN5WNH87roZgG6SOiRi
  oKD6VvbKQxkHBekYiVizfcBneqM0OU2tl+NfDv+Q2ArkryC8S6AU6KGW6UGYjrht3JjH2nqi02mv
  sKMaHQXqSLhmqKiCujEoC0g3SL8lkTeK0PhAZtJRjEVU5TlxlIry2F0cQeb4uxASteuUJJjPeTKi
  4wtx8qBPpP127WC7nhCwQiFLmTiuMFBpXMY5RAhLQZuRASEeN28rcqp9pnOHh4nRqYqA+wYJjsOH
  hnbJg1bL7Fq4XCcR1B3xtU1nTwaAOH2gt91VVvXIgcDFAZ8NrM4cMFdnlicNoHLabGzF/2IlK9h3
  RaDvA7PBjGv5u2YDt2aDGaSlX7JGso3IeBFWLM1sCpHfE5c6wVKKFyMZgmuY4uLnZzAmV0ZZSds9
  HROkiLq4JjtLhFbg3l1e8Q0oFAPA5Z5A3JOleIvRYh7jRgKggPOAqnYP/fHhYXZkGan7u/GAWG7v
  6GyzRC1MM1z+ug+cLXSqGtUs7FYLhYXbod0pfazVAAQdNIC7JrX1nb6b4hXbVKXdNQPEqiJaUWJc
  3gnG33/5jHcWB2A6r24cPV9j7I11slFzr2hXR+yqbPtUdOWJq7LtSFHOM0XyiTcWu8VYBCMo34Eu
  j0X5pKl8bJa3mlgEO9pB5S36B5ml23A5tUB92girjcO2GI9HQCEPzLdEHmy2Zk6uOKiqSbRZ6Jbo
  UEt0vQaZcb9Cs5W+BHFsyptkxzr98G6NzbTJPk/bN04nKFYQUr9LFyiDXHkCjPvkWFbu2fIB4Bgg
  EWI1a6Rut2keurW5YlG5SouLYB7u1kJ17iQ2uBm/jfid2OHqQLWWcccgwRviKV55APVp+WTayHAV
  4Cui+y29TuofdGQoN8GGhsfr4RiioO8FyPsAd6CYKcJ6pDDvSX1/J99dEE4YdJXM0NVDDDZxt3EL
  PEp5Tm80BF9wUUhyXl6NwHcPRtGYHGECGUw18TICMzq0WlTW0Gp66j9qfjvBVs1MC6BU6E40TZNC
  xmk2yyWJzOmH/uXgqvf71Xm/98zglLWjF784INbvdEzD+WxMC62+WkTVX2oHnnjaAdfzKQ/meMkn
  YOM4KMAkSjPMzKiauqkjB5tceYRKvzUhnyMQrBIx+BjFaPsA9x5alRzbI6UbbKFQOsiUmpqCevQK
  9thF7HHr2BpL2Rqr2XdZ0Jq3oZW511rB5s0seis8Cvb5RMOSt0oi/i+WQ+wlfNU3L9br3bd3rE6Y
  aRsK4gS/jQEwfdCrfDrG1qbJijZaW2FCb9S+3hXHGLOIWE4HD/TiEC/0lWEG6+OC7oumYbjI8spx
  xTo2DXMEZlujaNoza4wiazJ6yvJG40dsCmt7q03+0pc7fQzijb79hemB3//t7h918P2vg8PuwfFx
  5+iH/c7+Ybe7ff/r70jKeH1JRzt4vrbI5TXf0tbAa2IR/aIVGipkatCt4FmwVMaosD8CvN5FHz07
  PM+X/gL2yTpdx2jpr3gPAaTwps2Gi0KYutioCO3aJdfG3TQKp2isKtOb3r6JYzxZkmoAjVt8JwdU
  x506dAJjOE1ueRKB+kC/E5nkpELG+hIcqEaBXpi804yD4sEu5MyTtrf57pioG98iaQY14TRIJpxe
  12JFBBoEfTCvU3kQm4zRfpMs9gJxiES3XsSJWps2DuUvsajTLTyfZKMANCC+gARAjQ8SMe19QT87
  XftAo1QdVZ1QATWvhpouvO8aZ3LUyZbzNaCW/eQHaexAPao147M0W2IYM77OQfsVbR6oSrXjXrw1
  PsRfPGwxfdYOrKF22yYG65UQeSbfojBQND/xT3l3f5eNFrPZUr7HpV74YkPIQQfX2HC+ofoFjsIn
  8yr+em4tNRIgsvJxKqYE4YT2xPKQsNwI0S9vSraT9qf6wSKm+9QL7mFPxA/xMetytXktp9C/lWw9
  4IU/rCnzK691id/iKUvlA13IMZWlH+O6KH+1U0VJlzyin6D8+1embdqmbdqmbdqmbdqmbdqmbdqm
  bdqmbdqmbdqmbdqmbdqmbdqmbdqmbdqmbdqmbdqmbVon/QcDvFOJAKAAAA==
  ------=_Part_9699_23440302.1188574323106--

How-To-Repeat: 

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