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

PVS Bug 1066


Synopsis:        Soundness bug in PVS
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Fri Sep 10 10:30:08 -0700 2010
Originator:      "Munoz, Cesar Augusto (LARC-D320)"
Release:         PVS 4.2
Organization:    nasa.gov
Environment: 
 System:          
 Architecture: 

Description: 
  --_003_C8AFCF004AD1cesaramunoznasagov_
  Content-Type: text/plain; charset="us-ascii"
  Content-Transfer-Encoding: quoted-printable
  
  Hi Sam,
  
  By running our examples, Mauricio and I discovered a soundness bug in PVS.
  See attached dump file.
  
  My version of PVS is: PVS Version 4.2 - Allegro CL Enterprise Edition 8.1
  [Mac OS X (Intel)] (Jul   22, 2008 4:19). The bug occurs with and without
  the latest patch (which I include for completeness).
  
  The error seems to be in GRIND, which manages to prove the first lemma whic=
  h
  is false. Surprisingly, the second lemma cannot be proved with GRIND.
  
  bug : THEORY
  BEGIN
  
    bug : LEMMA
      FORALL (m: int, (n: int | m /=3D 0 OR n /=3D 0)):
         abs(m) > abs(n) AND NOT (m =3D 0 OR n =3D 0) AND NOT abs(m) =3D abs(=
  n)
         IMPLIES
          abs(rem(abs(n))(abs(m))) > abs(n)
  
    rem : LEMMA
      FORALL (m: nat, (n: nat | m /=3D 0 OR n /=3D 0)):
         m > n AND NOT (m =3D 0 OR n =3D 0) AND NOT m =3D n
         IMPLIES
           rem(n)(m) > n
  
    miracle : LEMMA
      FALSE
  
  END bug
  
  Unrelated to the soundness bug, we have also discovered a bug in the comman=
  d
  show-declaration-tccs. To recreate this bug, just issue the comment M-x
  show-declaration-tccs on the definition Fibonacci in the following
  
  theory.test : THEORY
  BEGIN
  
    factorial(n:posint) : RECURSIVE nat =3D
      IF n <=3D 1 THEN 1
      ELSE n*factorial(n-1)
      ENDIF
    MEASURE n
  
    fibonacci(n:int) : RECURSIVE nat =3D
      COND n >=3D 2 -> fibonacci(n-1) + fibonacci(n-2),
           n =3D 1  -> fibonacci(0),
           n =3D 0  -> 1,
           ELSE   -> fibonacci(0)
      ENDCOND
    MEASURE n=20
  END test
  
  You will get the message:
  
  There is garbage at the end of your file or string:
  Line 34:    (disjointness
              ^
  
  Curiously, in both cases, we spent a few hours blaming our code for these
  behaviors until we discovered that they were actually PVS errors.
  
  
  Cesar
  --=20
  Cesar A. Munoz                             NASA Langley Research Center
  Cesar.A.Munoz@nasa.gov                     Bldg. 1220  Room 115 MS. 130
  http://shemesh.larc.nasa.gov/people/cam    Hampton, VA 23681-2199, USA
  Office: +1 (757) 864 1446                  Fax: +1 (757) 864 4234
  
  
  --_003_C8AFCF004AD1cesaramunoznasagov_
  Content-Type: text/plain; name="bug.dmp"
  Content-Description: bug.dmp
  Content-Disposition: attachment; filename="bug.dmp"; size=6503;
  	creation-date="Fri, 10 Sep 2010 10:57:46 GMT";
  	modification-date="Fri, 10 Sep 2010 10:57:46 GMT"
  Content-Transfer-Encoding: base64
  
  CiUlIFBWUyBWZXJzaW9uIDQuMiAtIEFsbGVncm8gQ0wgRW50ZXJwcmlzZSBFZGl0aW9uIDguMSBb
  TWFjIE9TIFggKEludGVsKV0gKEp1bCAyMiwgMjAwOCA0OjE5KQolJSA4LjEgW01hYyBPUyBYIChJ
  bnRlbCldIChKdWwgMjIsIDIwMDggNDoxOSkKJCQkYnVnLnB2cwpidWcgOiBUSEVPUlkKQkVHSU4K
  CiAgYnVnIDogTEVNTUEKICAgIEZPUkFMTCAobTogaW50LCAobjogaW50IHwgbSAvPSAwIE9SIG4g
  Lz0gMCkpOgogICAgICAgYWJzKG0pID4gYWJzKG4pIEFORCBOT1QgKG0gPSAwIE9SIG4gPSAwKSBB
  TkQgTk9UIGFicyhtKSA9IGFicyhuKQogICAgICAgSU1QTElFUwogICAgICAgIGFicyhyZW0oYWJz
  KG4pKShhYnMobSkpKSA+IGFicyhuKQoKICByZW0gOiBMRU1NQQogICAgRk9SQUxMIChtOiBuYXQs
  IChuOiBuYXQgfCBtIC89IDAgT1IgbiAvPSAwKSk6CiAgICAgICBtID4gbiBBTkQgTk9UIChtID0g
  MCBPUiBuID0gMCkgQU5EIE5PVCBtID0gbgogICAgICAgSU1QTElFUwogICAgICAgICByZW0obiko
  bSkgPiBuCgogIG1pcmFjbGUgOiBMRU1NQQogICAgRkFMU0UKCkVORCBidWcKCiQkJGJ1Zy5wcmYK
  KGJ1ZwogKGJ1Z19UQ0MxIDAKICAoYnVnX1RDQzEtMSBuaWwgMzQ5MzExNjAzNSAzNDkzMTE2NjYw
  ICgiIiAoc3VidHlwZS10Y2MpIG5pbCBuaWwpCiAgIHVuY2hlY2tlZAogICAoKGJvb2xlYW4gbm9u
  ZW1wdHktdHlwZS1kZWNsIG5pbCBib29sZWFucyBuaWwpCiAgICAoYm9vbCBub25lbXB0eS10eXBl
  LWVxLWRlY2wgbmlsIGJvb2xlYW5zIG5pbCkKICAgIChOT1QgY29uc3QtZGVjbCAiW2Jvb2wgLT4g
  Ym9vbF0iIGJvb2xlYW5zIG5pbCkKICAgIChudW1iZXIgbm9uZW1wdHktdHlwZS1kZWNsIG5pbCBu
  dW1iZXJzIG5pbCkKICAgIChudW1iZXJfZmllbGRfcHJlZCBjb25zdC1kZWNsICJbbnVtYmVyIC0+
  IGJvb2xlYW5dIiBudW1iZXJfZmllbGRzCiAgICAgbmlsKQogICAgKG51bWJlcl9maWVsZCBub25l
  bXB0eS10eXBlLWZyb20tZGVjbCBuaWwgbnVtYmVyX2ZpZWxkcyBuaWwpCiAgICAocmVhbF9wcmVk
  IGNvbnN0LWRlY2wgIltudW1iZXJfZmllbGQgLT4gYm9vbGVhbl0iIHJlYWxzIG5pbCkKICAgIChy
  ZWFsIG5vbmVtcHR5LXR5cGUtZnJvbS1kZWNsIG5pbCByZWFscyBuaWwpCiAgICAocmF0aW9uYWxf
  cHJlZCBjb25zdC1kZWNsICJbcmVhbCAtPiBib29sZWFuXSIgcmF0aW9uYWxzIG5pbCkKICAgIChy
  YXRpb25hbCBub25lbXB0eS10eXBlLWZyb20tZGVjbCBuaWwgcmF0aW9uYWxzIG5pbCkKICAgIChp
  bnRlZ2VyX3ByZWQgY29uc3QtZGVjbCAiW3JhdGlvbmFsIC0+IGJvb2xlYW5dIiBpbnRlZ2VycyBu
  aWwpCiAgICAoaW50IG5vbmVtcHR5LXR5cGUtZXEtZGVjbCBuaWwgaW50ZWdlcnMgbmlsKQogICAg
  KE9SIGNvbnN0LWRlY2wgIltib29sLCBib29sIC0+IGJvb2xdIiBib29sZWFucyBuaWwpCiAgICAo
  Lz0gY29uc3QtZGVjbCAiYm9vbGVhbiIgbm90ZXF1YWwgbmlsKQogICAgKHJlYWxfbHRfaXNfc3Ry
  aWN0X3RvdGFsX29yZGVyIG5hbWUtanVkZ2VtZW50CiAgICAgIihzdHJpY3RfdG90YWxfb3JkZXI/
  W3JlYWxdKSIgcmVhbF9wcm9wcyBuaWwpCiAgICAoaW50X2Fic19pc19ub25uZWcgYXBwbGljYXRp
  b24tanVkZ2VtZW50ICJ7ajogbm9ubmVnX2ludCB8IGogPj0gaX0iCiAgICAgcmVhbF9kZWZzIG5p
  bCkKICAgIChyZWFsX2d0X2lzX3N0cmljdF90b3RhbF9vcmRlciBuYW1lLWp1ZGdlbWVudAogICAg
  ICIoc3RyaWN0X3RvdGFsX29yZGVyP1tyZWFsXSkiIHJlYWxfcHJvcHMgbmlsKSkKICAgNDcgNDAg
  bmlsIG5pbCkpCiAoYnVnIDAKICAoYnVnLTEgbmlsIDM0OTMxMTYwNDMgMzQ5MzExNjE0OQogICAo
  IiIgKHNrb3NpbXApICgoIiIgKGdyaW5kKSBuaWwgbmlsKSkgbmlsKSB1bmNoZWNrZWQKICAgKChh
  YnMgY29uc3QtZGVjbCAie246IG5vbm5lZ19yZWFsIHwgbiA+PSBtIEFORCBuID49IC1tfSIgcmVh
  bF9kZWZzCiAgICAgICAgIG5pbCkKICAgIChyZWFsX2x0X2lzX3N0cmljdF90b3RhbF9vcmRlciBu
  YW1lLWp1ZGdlbWVudAogICAgICIoc3RyaWN0X3RvdGFsX29yZGVyP1tyZWFsXSkiIHJlYWxfcHJv
  cHMgbmlsKQogICAgKG1pbnVzX2ludF9pc19pbnQgYXBwbGljYXRpb24tanVkZ2VtZW50ICJpbnQi
  IGludGVnZXJzIG5pbCkKICAgIChyZWFsX2d0X2lzX3N0cmljdF90b3RhbF9vcmRlciBuYW1lLWp1
  ZGdlbWVudAogICAgICIoc3RyaWN0X3RvdGFsX29yZGVyP1tyZWFsXSkiIHJlYWxfcHJvcHMgbmls
  KQogICAgKG11bHRfZGl2aWRlczIgYXBwbGljYXRpb24tanVkZ2VtZW50ICIoZGl2aWRlcyhtKSki
  IGRpdmlkZXMgbmlsKQogICAgKG11bHRfZGl2aWRlczEgYXBwbGljYXRpb24tanVkZ2VtZW50ICIo
  ZGl2aWRlcyhuKSkiIGRpdmlkZXMgbmlsKQogICAgKGludF9hYnNfaXNfbm9ubmVnIGFwcGxpY2F0
  aW9uLWp1ZGdlbWVudCAie2o6IG5vbm5lZ19pbnQgfCBqID49IGl9IgogICAgIHJlYWxfZGVmcyBu
  aWwpKQogICA0NzI1IDEzMCB0IHNob3N0YWspKQogKHJlbV9UQ0MxIDAKICAocmVtX1RDQzEtMSBu
  aWwgMzQ5MzExNjgwMyBuaWwgKCIiIChzdWJ0eXBlLXRjYykgbmlsIG5pbCkgbmlsIG5pbCBuaWwK
  ICAgbmlsIG5pbCBuaWwpKQogKHJlbSAwCiAgICAgIChyZW0tMSBuaWwgMzQ5MzExNjgwMyAzNDkz
  MTE2ODA4CiAgICAgICAoIiIgKGxlbW1hICJidWciKQogICAgICAgICgoIiIgKHNrb3NpbXApCiAg
  ICAgICAgICAoKCIiIChpbnN0IC0xICJtITEiICJuITEiKSAoKCIiIChncmluZCkgbmlsIG5pbCkp
  IG5pbCkpIG5pbCkpCiAgICAgICAgbmlsKQogICAgICAgcHJvdmVkCiAgICAgICAoKGJ1ZyBmb3Jt
  dWxhLWRlY2wgbmlsIGJ1ZyBuaWwpCiAgICAgICAgKGludF9hYnNfaXNfbm9ubmVnIGFwcGxpY2F0
  aW9uLWp1ZGdlbWVudAogICAgICAgICAie2o6IG5vbm5lZ19pbnQgfCBqID49IGl9IiByZWFsX2Rl
  ZnMgbmlsKQogICAgICAgIChudW1iZXIgbm9uZW1wdHktdHlwZS1kZWNsIG5pbCBudW1iZXJzIG5p
  bCkKICAgICAgICAoYm9vbGVhbiBub25lbXB0eS10eXBlLWRlY2wgbmlsIGJvb2xlYW5zIG5pbCkK
  ICAgICAgICAobnVtYmVyX2ZpZWxkX3ByZWQgY29uc3QtZGVjbCAiW251bWJlciAtPiBib29sZWFu
  XSIKICAgICAgICAgbnVtYmVyX2ZpZWxkcyBuaWwpCiAgICAgICAgKG51bWJlcl9maWVsZCBub25l
  bXB0eS10eXBlLWZyb20tZGVjbCBuaWwgbnVtYmVyX2ZpZWxkcyBuaWwpCiAgICAgICAgKHJlYWxf
  cHJlZCBjb25zdC1kZWNsICJbbnVtYmVyX2ZpZWxkIC0+IGJvb2xlYW5dIiByZWFscyBuaWwpCiAg
  ICAgICAgKHJlYWwgbm9uZW1wdHktdHlwZS1mcm9tLWRlY2wgbmlsIHJlYWxzIG5pbCkKICAgICAg
  ICAocmF0aW9uYWxfcHJlZCBjb25zdC1kZWNsICJbcmVhbCAtPiBib29sZWFuXSIgcmF0aW9uYWxz
  IG5pbCkKICAgICAgICAocmF0aW9uYWwgbm9uZW1wdHktdHlwZS1mcm9tLWRlY2wgbmlsIHJhdGlv
  bmFscyBuaWwpCiAgICAgICAgKGludGVnZXJfcHJlZCBjb25zdC1kZWNsICJbcmF0aW9uYWwgLT4g
  Ym9vbGVhbl0iIGludGVnZXJzIG5pbCkKICAgICAgICAoaW50IG5vbmVtcHR5LXR5cGUtZXEtZGVj
  bCBuaWwgaW50ZWdlcnMgbmlsKQogICAgICAgIChib29sIG5vbmVtcHR5LXR5cGUtZXEtZGVjbCBu
  aWwgYm9vbGVhbnMgbmlsKQogICAgICAgICg+PSBjb25zdC1kZWNsICJib29sIiByZWFscyBuaWwp
  CiAgICAgICAgKG5hdCBub25lbXB0eS10eXBlLWVxLWRlY2wgbmlsIG5hdHVyYWxudW1iZXJzIG5p
  bCkKICAgICAgICAoT1IgY29uc3QtZGVjbCAiW2Jvb2wsIGJvb2wgLT4gYm9vbF0iIGJvb2xlYW5z
  IG5pbCkKICAgICAgICAoLz0gY29uc3QtZGVjbCAiYm9vbGVhbiIgbm90ZXF1YWwgbmlsKQogICAg
  ICAgIChhYnMgY29uc3QtZGVjbCAie246IG5vbm5lZ19yZWFsIHwgbiA+PSBtIEFORCBuID49IC1t
  fSIKICAgICAgICAgICAgIHJlYWxfZGVmcyBuaWwpCiAgICAgICAgKHJlYWxfZ3RfaXNfc3RyaWN0
  X3RvdGFsX29yZGVyIG5hbWUtanVkZ2VtZW50CiAgICAgICAgICIoc3RyaWN0X3RvdGFsX29yZGVy
  P1tyZWFsXSkiIHJlYWxfcHJvcHMgbmlsKQogICAgICAgIChyZWFsX2x0X2lzX3N0cmljdF90b3Rh
  bF9vcmRlciBuYW1lLWp1ZGdlbWVudAogICAgICAgICAiKHN0cmljdF90b3RhbF9vcmRlcj9bcmVh
  bF0pIiByZWFsX3Byb3BzIG5pbCkKICAgICAgICAobWludXNfaW50X2lzX2ludCBhcHBsaWNhdGlv
  bi1qdWRnZW1lbnQgImludCIgaW50ZWdlcnMgbmlsKQogICAgICAgIChtdWx0X2RpdmlkZXMyIGFw
  cGxpY2F0aW9uLWp1ZGdlbWVudCAiKGRpdmlkZXMobSkpIiBkaXZpZGVzCiAgICAgICAgIG5pbCkK
  ICAgICAgICAobXVsdF9kaXZpZGVzMSBhcHBsaWNhdGlvbi1qdWRnZW1lbnQgIihkaXZpZGVzKG4p
  KSIgZGl2aWRlcwogICAgICAgICBuaWwpKQogICAgICAgMjEzMyAxMDAgdCBuaWwpKQogKG1pcmFj
  bGUgMAogIChtaXJhY2xlLTEgbmlsIDM0OTMxMTY2NjkgMzQ5MzExNzA4OAogICAoIiIgKGNhc2Ug
  InJlbSgxKSgyKSA+IDEiKQogICAgKCgiMSIgKHR5cGVwcmVkICJyZW0oMSkoMikiKSAoKCIxIiAo
  YXNzZXJ0KSBuaWwgbmlsKSkgbmlsKQogICAgICgiMiIgKGxlbW1hICJyZW0iKSAoKCIyIiAoaW5z
  dD8pICgoIjIiIChhc3NlcnQpIG5pbCBuaWwpKSBuaWwpKQogICAgICBuaWwpKQogICAgbmlsKQog
  ICBwcm92ZWQKICAgKChyZW0gZm9ybXVsYS1kZWNsIG5pbCBidWcgbmlsKQogICAgKE9SIGNvbnN0
  LWRlY2wgIltib29sLCBib29sIC0+IGJvb2xdIiBib29sZWFucyBuaWwpCiAgICAoLz0gY29uc3Qt
  ZGVjbCAiYm9vbGVhbiIgbm90ZXF1YWwgbmlsKQogICAgKE5PVCBjb25zdC1kZWNsICJbYm9vbCAt
  PiBib29sXSIgYm9vbGVhbnMgbmlsKQogICAgKHJlYWxfbHRfaXNfc3RyaWN0X3RvdGFsX29yZGVy
  IG5hbWUtanVkZ2VtZW50CiAgICAgIihzdHJpY3RfdG90YWxfb3JkZXI/W3JlYWxdKSIgcmVhbF9w
  cm9wcyBuaWwpCiAgICAocmVhbF9ndF9pc19zdHJpY3RfdG90YWxfb3JkZXIgbmFtZS1qdWRnZW1l
  bnQKICAgICAiKHN0cmljdF90b3RhbF9vcmRlcj9bcmVhbF0pIiByZWFsX3Byb3BzIG5pbCkKICAg
  IChtdWx0X2RpdmlkZXMxIGFwcGxpY2F0aW9uLWp1ZGdlbWVudCAiKGRpdmlkZXMobikpIiBkaXZp
  ZGVzIG5pbCkKICAgIChtdWx0X2RpdmlkZXMyIGFwcGxpY2F0aW9uLWp1ZGdlbWVudCAiKGRpdmlk
  ZXMobSkpIiBkaXZpZGVzIG5pbCkKICAgIChudW1iZXIgbm9uZW1wdHktdHlwZS1kZWNsIG5pbCBu
  dW1iZXJzIG5pbCkKICAgIChib29sZWFuIG5vbmVtcHR5LXR5cGUtZGVjbCBuaWwgYm9vbGVhbnMg
  bmlsKQogICAgKG51bWJlcl9maWVsZF9wcmVkIGNvbnN0LWRlY2wgIltudW1iZXIgLT4gYm9vbGVh
  bl0iIG51bWJlcl9maWVsZHMKICAgICBuaWwpCiAgICAobnVtYmVyX2ZpZWxkIG5vbmVtcHR5LXR5
  cGUtZnJvbS1kZWNsIG5pbCBudW1iZXJfZmllbGRzIG5pbCkKICAgIChyZWFsX3ByZWQgY29uc3Qt
  ZGVjbCAiW251bWJlcl9maWVsZCAtPiBib29sZWFuXSIgcmVhbHMgbmlsKQogICAgKHJlYWwgbm9u
  ZW1wdHktdHlwZS1mcm9tLWRlY2wgbmlsIHJlYWxzIG5pbCkKICAgIChib29sIG5vbmVtcHR5LXR5
  cGUtZXEtZGVjbCBuaWwgYm9vbGVhbnMgbmlsKQogICAgKD4gY29uc3QtZGVjbCAiYm9vbCIgcmVh
  bHMgbmlsKQogICAgKHJhdGlvbmFsX3ByZWQgY29uc3QtZGVjbCAiW3JlYWwgLT4gYm9vbGVhbl0i
  IHJhdGlvbmFscyBuaWwpCiAgICAocmF0aW9uYWwgbm9uZW1wdHktdHlwZS1mcm9tLWRlY2wgbmls
  IHJhdGlvbmFscyBuaWwpCiAgICAoaW50ZWdlcl9wcmVkIGNvbnN0LWRlY2wgIltyYXRpb25hbCAt
  PiBib29sZWFuXSIgaW50ZWdlcnMgbmlsKQogICAgKGludCBub25lbXB0eS10eXBlLWVxLWRlY2wg
  bmlsIGludGVnZXJzIG5pbCkKICAgICg+PSBjb25zdC1kZWNsICJib29sIiByZWFscyBuaWwpCiAg
  ICAobm9ubmVnX2ludCBub25lbXB0eS10eXBlLWVxLWRlY2wgbmlsIGludGVnZXJzIG5pbCkKICAg
  IChwb3NuYXQgbm9uZW1wdHktdHlwZS1lcS1kZWNsIG5pbCBpbnRlZ2VycyBuaWwpCiAgICAobmF0
  IG5vbmVtcHR5LXR5cGUtZXEtZGVjbCBuaWwgbmF0dXJhbG51bWJlcnMgbmlsKQogICAgKDwgY29u
  c3QtZGVjbCAiYm9vbCIgcmVhbHMgbmlsKQogICAgKG1vZCBub25lbXB0eS10eXBlLWVxLWRlY2wg
  bmlsIGV1Y2xpZGVhbl9kaXZpc2lvbiBuaWwpCiAgICAoPSBjb25zdC1kZWNsICJbVCwgVCAtPiBi
  b29sZWFuXSIgZXF1YWxpdGllcyBuaWwpCiAgICAobnVtZmllbGQgbm9uZW1wdHktdHlwZS1lcS1k
  ZWNsIG5pbCBudW1iZXJfZmllbGRzIG5pbCkKICAgICgrIGNvbnN0LWRlY2wgIltudW1maWVsZCwg
  bnVtZmllbGQgLT4gbnVtZmllbGRdIiBudW1iZXJfZmllbGRzIG5pbCkKICAgICgqIGNvbnN0LWRl
  Y2wgIltudW1maWVsZCwgbnVtZmllbGQgLT4gbnVtZmllbGRdIiBudW1iZXJfZmllbGRzIG5pbCkK
  ICAgIChyZW0gY29uc3QtZGVjbCAie3I6IG1vZChiKSB8IEVYSVNUUyBxOiB4ID0gYiAqIHEgKyBy
  fSIKICAgICAgICAgbW9kdWxvX2FyaXRobWV0aWMgbmlsKSkKICAgNjg5NjcgNDAgdCBzaG9zdGFr
  KSkpCgo=
  
  --_003_C8AFCF004AD1cesaramunoznasagov_
  Content-Type: application/octet-stream; name="patch.lisp"
  Content-Description: patch.lisp
  Content-Disposition: attachment; filename="patch.lisp"; size=6049;
  	creation-date="Fri, 10 Sep 2010 10:57:46 GMT";
  	modification-date="Fri, 10 Sep 2010 10:57:46 GMT"
  Content-Transfer-Encoding: base64
  
  KGRlZnVuIHBhcnNlLXJld3JpdGUtbmFtZSAoZm9ybSBiYW5ncy1hbGxvd2VkPyAmb3B0aW9uYWwg
  YmFuZ3MpCiAgKHVubGVzcyAob3IgKHN0cmluZ3AgZm9ybSkKICAgICAgICAgICAgICAoc3ltYm9s
  cCBmb3JtKQogICAgICAgICAgICAgIChpbnRlZ2VycCBmb3JtKQogICAgICAgICAgICAgIChyZXdy
  aXRlLW5hbWU/IGZvcm0pKQogICAgKGVycm9yLWZvcm1hdC1pZiAifiVJbGxlZ2FsIHJld3JpdGUg
  bmFtZTogfmEiIGZvcm0pKQogIChsZXQqICgocmV3cml0ZSAocGMtcGFyc2UgZm9ybSAncmV3cml0
  ZS1uYW1lLW9yLWZudW0pKQogICAgICAgICAocmV3cml0ZS1uYW1lCiAgICAgICAgICAodHlwZWNh
  c2UgcmV3cml0ZQogICAgICAgICAgICAobGF6eS1yZXdyaXRlLW5hbWUKICAgICAgICAgICAgIChj
  YXNlIGJhbmdzCiAgICAgICAgICAgICAgICghIChjaGFuZ2UtY2xhc3MgcmV3cml0ZSAnZWFnZXIt
  cmV3cml0ZS1uYW1lKSkKICAgICAgICAgICAgICAgKCEhIChjaGFuZ2UtY2xhc3MgcmV3cml0ZSAn
  bWFjcm8tcmV3cml0ZS1uYW1lKSkKICAgICAgICAgICAgICAgKHQgcmV3cml0ZSkpKQogICAgICAg
  ICAgICAobGF6eS1mbnVtLXJld3JpdGUKICAgICAgICAgICAgIChjYXNlIGJhbmdzCiAgICAgICAg
  ICAgICAgICghIChjaGFuZ2UtY2xhc3MgcmV3cml0ZSAnZWFnZXItZm51bS1yZXdyaXRlKSkKICAg
  ICAgICAgICAgICAgKCEhIChjaGFuZ2UtY2xhc3MgcmV3cml0ZSAnbWFjcm8tZm51bS1yZXdyaXRl
  KSkKICAgICAgICAgICAgICAgKHQgcmV3cml0ZSkpKQogICAgICAgICAgICAodAogICAgICAgICAg
  ICAgKHVubGVzcyBiYW5ncy1hbGxvd2VkPwogICAgICAgICAgICAgICAoZXJyb3ItZm9ybWF0LWlm
  CiAgICAgICAgICAgICAgICAifiVEbyBub3QgbWl4IHBhcmVucyBhbmQgISdzIGluIHJld3JpdGUg
  bmFtZXMiKSkKICAgICAgICAgICAgIHJld3JpdGUpKSkpCiAgICAodW5sZXNzIChvciAoZm51bS1y
  ZXdyaXRlPyByZXdyaXRlLW5hbWUpCiAgICAgICAgICAgICAgICAocmVzb2x1dGlvbnMgcmV3cml0
  ZS1uYW1lKSkKICAgICAgKHR5cGVjaGVjayByZXdyaXRlLW5hbWUpKQogICAgcmV3cml0ZS1uYW1l
  KSkKCihkZWZ1biBpbnN0YWxsLXJld3JpdGUtcmVzIChyZXMgbmFtZSBmbWxhIGFsd2F5cz8pICAg
  ICAgICAgICAgCiAgKG11bHRpcGxlLXZhbHVlLWJpbmQgKGxocyByaHMgaHlwKQogICAgICAoc3Bs
  aXQtcmV3cml0ZSBmbWxhKQogICAgKGxldCogKChyZXMgKG9yIChpcy1yZXMtcmV3cml0ZSByZXMp
  IHJlcykpCiAgICAgICAgICAgKGxocy1mcmVldmFycyAoZnJlZXZhcnMgbGhzKSkKICAgICAgICAg
  ICAocmhzLWZyZWV2YXJzIChmcmVldmFycyByaHMpKQogICAgICAgICAgIChoeXAtZnJlZXZhcnMg
  KGZyZWV2YXJzIGh5cCkpCiAgICAgICAgICAgKG9wKiAob3BlcmF0b3IqIGxocykpCiAgICAgICAg
  ICAgKGhhc2huYW1lIChhdXRvLXJld3JpdGUtaGFzaG5hbWUgb3AqKSkKICAgICAgICAgICAoZGVj
  bCAoaWYgKHR5cGVwIGhhc2huYW1lICduYW1lLWV4cHIpCiAgICAgICAgICAgICAgICAgICAgIChk
  ZWNsYXJhdGlvbiBoYXNobmFtZSkKICAgICAgICAgICAgICAgICAgICAgaGFzaG5hbWUpKSkgOzso
  YnJlYWsgImluc3RhbGwtcmV3cml0ZS1yZXMiKQogICAgICAoY29uZAogICAgICAgKChudWxsIGhh
  c2huYW1lKQogICAgICAgIChlcnJvci1mb3JtYXQtaWYgIn4lQ2FuJ3QgcmV3cml0ZSB1c2luZyB+
  YTogIExIUyBrZXkgfmEgaXMgYmFkIiBuYW1lIG9wKikpCiAgICAgICAoKG5vdCAoc3Vic2V0cCBy
  aHMtZnJlZXZhcnMgbGhzLWZyZWV2YXJzCiAgICAgICAgICAgICAgICAgICAgICA6dGVzdCAjJ3Rj
  LWVxKSkKICAgICAgICAoZXJyb3ItZm9ybWF0LWlmICJ+JUNhbid0IHJld3JpdGUgdXNpbmcgfmE6
  IG5vbi1MSFMgZnJlZXZhcnMgaW4gUkhTLiIgbmFtZSApKQogICAgICAgKChub3QgKHN1YnNldHAg
  aHlwLWZyZWV2YXJzIGxocy1mcmVldmFycwogICAgICAgICAgICAgICAgICAgICAgOnRlc3QgIyd0
  Yy1lcSkpCiAgICAgICAgKGVycm9yLWZvcm1hdC1pZiAifiVDYW4ndCByZXdyaXRlIHVzaW5nIH5h
  OiBub24tTEhTIGZyZWV2YXJzIGluIGh5cG90aGVzZXMuIiBuYW1lKSkKICAgICAgICgoYW5kIChy
  ZXNvbHV0aW9uPyByZXMpCiAgICAgICAgICAgICAoZml4cG9pbnQtZGVjbD8gKGRlY2xhcmF0aW9u
  IHJlcykpKQogICAgICAgIChlcnJvci1mb3JtYXQtaWYgIn4lQ2FuJ3QgcmV3cml0ZSB1c2luZyB+
  YTogKGNvKWluZHVjdGl2ZSBkZWZpbml0aW9uIGNhbm5vdCBiZSB1c2VkLiIgbmFtZSkpCiAgICAg
  ICAodAogICAgICAgICh1bmxlc3MgKGNvbnNwIHJlcykgOzsoNi4xNi45NSlhdm9pZHMgYW50ZWNl
  ZGVudCByZXdyaXRlcwogICAgICAgICAgKHR5cGVjaGVjayAobW9kdWxlLWluc3RhbmNlIHJlcykg
  OnRjY3MgJ2FsbCkpCiAgICAgICAgOztOU0goNi4xNC45NSk6IGFib3ZlIHR5cGVjaGVjayBuZWVk
  ZWQgdG8gZ2VuZXJhdGUKICAgICAgICA7O2Fzc3VtaW5nIFRDQ1MuIAogICAgICAgIChwdXNobmV3
  CiAgICAgICAgIChtYWtlLWluc3RhbmNlICdyZXdyaXRlCiAgICAgICAgICAgOmxocyBsaHMKICAg
  ICAgICAgICA6cmhzIHJocwogICAgICAgICAgIDpoeXAgaHlwCiAgICAgICAgICAgOnJlcyByZXMp
  CiAgICAgICAgIChnZXRoYXNoIGRlY2wKICAgICAgICAgICAgICAgICAgKmF1dG8tcmV3cml0ZXMq
  KQogICAgICAgICA6dGVzdCAjJyhsYW1iZGEgKHggeSkodGMtZXEgKHJlcyB4KShyZXMgeSkpKSkK
  ICAgICAgICAocHVzaG5ldyByZXMgKmFsbC1yZXdyaXRlcy1uYW1lcyopIDs7ZG9uJ3QgbmVlZCB0
  Yy1lcQogICAgICAgIDs7ICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgKCphdXRvLXJld3Jp
  dGVzKikKICAgICAgICAoY29uZCAoKGFuZCAoZXEgYWx3YXlzPyAnISEpIDs7TlNIKDUuOC45OCkg
  aW5zZXJ0ZWQgbWFjcm8gY2FzZQogICAgICAgICAgICAgICAgICAgIChub3QgKGFuZCAocmVzb2x1
  dGlvbj8gcmVzKSA7O05TSCgxMi4xLjk1KQogICAgICAgICAgICAgICAgICAgICAgICAgICAgICAo
  ZGVmLWRlY2w/IChkZWNsYXJhdGlvbiByZXMpKSkpKQogICAgICAgICAgICAgICAocHVzaG5ldyBy
  ZXMgKm1hY3JvLW5hbWVzKikKICAgICAgICAgICAgICAgOzs6dGVzdCAjJ3RjLWVxCiAgICAgICAg
  ICAgICAgIChzZXRxICphdXRvLXJld3JpdGVzLW5hbWVzKgogICAgICAgICAgICAgICAgICAgICAo
  cmVtb3ZlIHJlcyAqYXV0by1yZXdyaXRlcy1uYW1lcyopKQogICAgICAgICAgICAgICAoc2V0cSAq
  YXV0by1yZXdyaXRlcyEtbmFtZXMqCiAgICAgICAgICAgICAgICAgICAgIChyZW1vdmUgcmVzICph
  dXRvLXJld3JpdGVzIS1uYW1lcyopKQogICAgICAgICAgICAgICA7Ozp0ZXN0ICMndGMtZXEKICAg
  ICAgICAgICAgICAgKGZvcm1hdC1pZiAifiVJbnN0YWxsaW5nIG1hY3JvKCEhKSB+YX5AWyB+YX5d
  IgogICAgICAgICAgICAgICAgICAgICAgICAgIChpZiAocmVzb2x1dGlvbj8gcmVzKQogICAgICAg
  ICAgICAgICAgICAgICAgICAgICAgICAocmVzb2x1dGlvbi1zdHJpbmcgcmVzKQogICAgICAgICAg
  ICAgICAgICAgICAgICAgICAgICBuYW1lKQogICAgICAgICAgICAgICAgICAgICAgICAgIChhbmQg
  KHJlc29sdXRpb24/IHJlcykKICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChub3QgKGZ1
  bGx5LWluc3RhbnRpYXRlZD8gcmVzKSkKICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICIo
  YWxsIGluc3RhbmNlcykiKSkpCiAgICAgICAgICAgICAgKChhbmQgYWx3YXlzPyA7O05TSCgxMC43
  Ljk1KSBkZWNsIC0+IChkZWNsYXJhdGlvbiByZXMpCiAgICAgICAgICAgICAgICAgICAgKG5vdCAo
  YW5kIChyZXNvbHV0aW9uPyByZXMpIDs7TlNIKDEyLjEuOTUpCiAgICAgICAgICAgICAgICAgICAg
  ICAgICAgICAgIChkZWYtZGVjbD8gKGRlY2xhcmF0aW9uIHJlcykpKSkpCiAgICAgICAgICAgICAg
  IChwdXNobmV3IHJlcyAqYXV0by1yZXdyaXRlcyEtbmFtZXMqKQogICAgICAgICAgICAgICA7Ozp0
  ZXN0ICMndGMtZXEKICAgICAgICAgICAgICAgKHNldHEgKmF1dG8tcmV3cml0ZXMtbmFtZXMqCiAg
  ICAgICAgICAgICAgICAgICAgIChyZW1vdmUgcmVzICphdXRvLXJld3JpdGVzLW5hbWVzKikpCiAg
  ICAgICAgICAgICAgIChzZXRxICptYWNyby1uYW1lcyoKICAgICAgICAgICAgICAgICAgICAgKHJl
  bW92ZSByZXMgKm1hY3JvLW5hbWVzKikpCiAgICAgICAgICAgICAgIDs7OnRlc3QgIyd0Yy1lcQog
  ICAgICAgICAgICAgICAoZm9ybWF0LWlmICJ+JUluc3RhbGxpbmcgcmV3cml0ZSBydWxlKCEpIH5h
  fkBbIH5hfl0iCiAgICAgICAgICAgICAgICAgICAgICAgICAgKGlmIChyZXNvbHV0aW9uPyByZXMp
  CiAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChyZXNvbHV0aW9uLXN0cmluZyByZXMpCiAg
  ICAgICAgICAgICAgICAgICAgICAgICAgICAgIG5hbWUpCiAgICAgICAgICAgICAgICAgICAgICAg
  ICAgKGFuZCAocmVzb2x1dGlvbj8gcmVzKQogICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg
  KG5vdCAoZnVsbHktaW5zdGFudGlhdGVkPyByZXMpKQogICAgICAgICAgICAgICAgICAgICAgICAg
  ICAgICAgIihhbGwgaW5zdGFuY2VzKSIpKSkKICAgICAgICAgICAgICAodCAocHVzaG5ldyByZXMg
  KmF1dG8tcmV3cml0ZXMtbmFtZXMqKQogICAgICAgICAgICAgICAgIDs7OnRlc3QgIyd0Yy1lcQog
  ICAgICAgICAgICAgICAgIChzZXRxICphdXRvLXJld3JpdGVzIS1uYW1lcyoKICAgICAgICAgICAg
  ICAgICAgICAgICAocmVtb3ZlIHJlcyAqYXV0by1yZXdyaXRlcyEtbmFtZXMqKSkKICAgICAgICAg
  ICAgICAgICAoc2V0cSAqbWFjcm8tbmFtZXMqCiAgICAgICAgICAgICAgICAgICAgICAgKHJlbW92
  ZSByZXMgKm1hY3JvLW5hbWVzKikpCiAgICAgICAgICAgICAgICAgOzs6dGVzdCAjJ3RjLWVxCiAg
  ICAgICAgICAgICAgICAgKGZvcm1hdC1pZiAifiVJbnN0YWxsaW5nIHJld3JpdGUgcnVsZSB+YX5A
  WyB+YX5dIgogICAgICAgICAgICAgICAgICAgICAgICAgICAgKGlmIChyZXNvbHV0aW9uPyByZXMp
  CiAgICAgICAgICAgICAgICAgICAgICAgICAgICAgIChyZXNvbHV0aW9uLXN0cmluZyByZXMpCiAg
  ICAgICAgICAgICAgICAgICAgICAgICAgICAgIG5hbWUpCiAgICAgICAgICAgICAgICAgICAgICAg
  ICAgICAoYW5kIChyZXNvbHV0aW9uPyByZXMpCiAgICAgICAgICAgICAgICAgICAgICAgICAgICAg
  ICAobm90IChmdWxseS1pbnN0YW50aWF0ZWQ/IHJlcykpCiAgICAgICAgICAgICAgICAgICAgICAg
  ICAgICAgICAiKGFsbCBpbnN0YW5jZXMpIikpKSkKICAgICAgICAoc2V0ZiAoZ2V0aGFzaCAocmV3
  cml0ZS1kZWNsYXJhdGlvbiBoYXNobmFtZSkgKmF1dG8tcmV3cml0ZXMtb3BzKikgdCkKICAgICAg
  ICA7Oyhmb3JtYXQtaWYgIn4lSW5zdGFsbGluZyByZXdyaXRlIHJ1bGUgfmEiIG5hbWUpCiAgICAg
  ICAgKSkpKSkKCihkZWZ1biByZXNvbHV0aW9uLXN0cmluZyAocmVzKQogIChmb3JtYXQgbmlsICJ+
  QDx+QFt+YUB+XX5hfkBbfkl+PFt+O35Ae35Xfl4sIH46X359fjtdfjo+fl1+QFt+SX48e3t+O35A
  e35Xfl4sIH46X359fjt9fX46Pn5dfkBbLn5hfl1+Oj4iCiAgICAoYW5kIChtb2R1bGUtaW5zdGFu
  Y2UgcmVzKSAobGlicmFyeSAobW9kdWxlLWluc3RhbmNlIHJlcykpKQogICAgKGFuZCAobW9kdWxl
  LWluc3RhbmNlIHJlcykgKGlkIChtb2R1bGUtaW5zdGFuY2UgcmVzKSkpCiAgICAoYW5kIChtb2R1
  bGUtaW5zdGFuY2UgcmVzKSAoYWN0dWFscyAobW9kdWxlLWluc3RhbmNlIHJlcykpKQogICAgKGFu
  ZCAobW9kdWxlLWluc3RhbmNlIHJlcykgKG1hcHBpbmdzIChtb2R1bGUtaW5zdGFuY2UgcmVzKSkp
  CiAgICAod2hlbiAoZGVjbGFyYXRpb24gcmVzKSAoaWQgKGRlY2xhcmF0aW9uIHJlcykpKQogICAg
  KHdoZW4gKGRlY2xhcmF0aW9uIHJlcykKICAgICAgKGlmIChlcSAoa2luZC1vZiAoZGVjbGFyYXRp
  b24gcmVzKSkgJ2V4cHIpCiAgICAgICAgICAob3IgKHR5cGUgcmVzKSAodHlwZSAoZGVjbGFyYXRp
  b24gcmVzKSkpCiAgICAgICAgICAoa2luZC1vZiAoZGVjbGFyYXRpb24gcmVzKSkpKSkpCgogICAg
  ICAgICAKCg==
  
  --_003_C8AFCF004AD1cesaramunoznasagov_--

How-To-Repeat: 

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