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

PVS Bug 1060


Synopsis:        PVS doesn't recognize trivial truth
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Wed Jul 21 02:20:00 -0700 2010
Originator:      Hendrik Tews
Release:         PVS 4.2
Organization:    os.inf.tu-dresden.de
Environment: 
 System:          
 Architecture: 

Description: 
  
  --UGryaBjJit
  Content-Type: text/plain; charset=us-ascii
  Content-Description: message body text
  Content-Transfer-Encoding: 7bit
  
  Hi,
  
  in the attached file, the prove of the last lemma yields the
  following sequent:
  
  {1}   MESIState_adt[MESIStateModel_2.number_of_cores_def].modified(0) =
         MESIState_adt[MESIStateModel_2.number_of_cores_def].modified(0)
  
  However, assert does not finish this branch. Only
  apply-extensionality is able to solve this.
  
  Bye,
  
  Hendrik
  
  
  --UGryaBjJit
  Content-Type: application/octet-stream; name="simple-mesi-trivial-truth.pvs"
  Content-Disposition: attachment;
  	filename="simple-mesi-trivial-truth.pvs"
  Content-Transfer-Encoding: base64
  
  TW9yZVNldHNbVCA6IFR5cGVdIDogVGhlb3J5CkJlZ2luCiAgdHdpbihhLCBiIDogVCkgOiAobm9u
  ZW1wdHk/W1RdKSA9IHsgeCA6IFQgfCB4ID0gYSBvciB4ID0gYiB9CgpFbmQgTW9yZVNldHMKCgpU
  eXBlc0RlZmluaXRpb25zIDogVEhFT1JZCkJFR0lOCiAgRGVsYXkgOiBUWVBFID0gIG5hdApFTkQg
  VHlwZXNEZWZpbml0aW9ucwoKCkNhY2hlSW50ZXJmYWNlW1NlbGYgOiBUWVBFICwgQ29yZSA6IFRZ
  UEVdIDogVEhFT1JZCkJFR0lOCiAgSU1QT1JUSU5HIFR5cGVzRGVmaW5pdGlvbnMKICAKICBDYWNo
  ZVNpZ25hdHVyZSA6IFRZUEUgPSAKICAgIFsjCiAgICAgIHdyaXRlIDogW1tTZWxmICwgQ29yZV0g
  LT4gW1NlbGYgLCBEZWxheV1dICwgCiAgICAgIGV4Y2hhbmdlIDogW1tTZWxmICwgQ29yZV0gLT4g
  W1NlbGYgLCBEZWxheV1dICwgCiAgICAgIHJlcGxhY2UgOiBbW1NlbGYgLCBDb3JlXSAtPiBbU2Vs
  ZiAsIERlbGF5XV0KICAgICNdCiAgCkVORCBDYWNoZUludGVyZmFjZQoKCk1FU0lTdGF0ZVtjb3Jl
  cyA6IG5hdF0gOiBEYXRhdHlwZQpCZWdpbgogIG1lbW9yeSA6IG1lbW9yeT8gJSA9IGludmFsaWQg
  aW4gYWxsIGNhY2hlcwogIG1vZGlmaWVkKGNvcmUgOiBiZWxvdyhjb3JlcykpIDogbW9kaWZpZWQ/
  CiAgZXhjbHVzaXZlKGNvcmUgOiBiZWxvdyhjb3JlcykpIDogZXhjbHVzaXZlPwogIHNoYXJlZChj
  b3JlX3NldCA6IG5vbmVtcHR5X3NldFtiZWxvdyhjb3JlcyldKSA6IHNoYXJlZD8KRW5kIE1FU0lT
  dGF0ZQoKCgpNRVNJU3RhdGVNb2RlbF8yIDogVGhlb3J5CkJlZ2luCgogIG51bWJlcl9vZl9jb3Jl
  c19kZWYgOiBuYXQgPSAyCgogIENvcmUgOiBUeXBlID0gYmVsb3cobnVtYmVyX29mX2NvcmVzX2Rl
  ZikKCiAgSW1wb3J0aW5nIE1vcmVTZXRzLCBDYWNoZUludGVyZmFjZSwgTUVTSVN0YXRlCgogIFNl
  bGYgOiBUeXBlID0gTUVTSVN0YXRlW251bWJlcl9vZl9jb3Jlc19kZWZdCgogICUgYWJzdHJhY3Qg
  ZGVsYXlzOgogICUgICBkX2MgICBjYWNoZSAgICAgICAgICAgZm9yIGNhY2hlIGhpdHMgKHJlYWQg
  b3Igd3JpdGUpCiAgJSAgIGRfbSAgIG1lbW9yeSAgICAgICAgICBmb3IgY2FjaGUgbWlzc2VzIChy
  ZWFkIGZyb20gbWVtb3J5KQogICUgICBkX2N0ICBjYWNoZSB0cmFuc2ZlciAgZm9yIHRyYW5zZmVy
  aW5nIGEgbW9kaWZpZWQgaXRlbSBmcm9tIGEgCiAgJSAgICAgICAgICAgICAgICAgICAgICAgICBk
  aWZmZXJlbnQgY2FjaGUKICAlICAgZF93YiAgd3JpdGUgYmFjayAgICAgIGZvciB3cml0aW5nIGEg
  bW9kaWZpZWQgaXRlbSB0byBtZW1vcnkKCiAgd3JpdGUoZF9jLCBkX20sIGRfY3QsIGRfd2IgOiBE
  ZWxheSkgOiBbU2VsZiwgQ29yZSAtPiBbU2VsZiwgRGVsYXldXSA9IAogICAgTGFtYmRhKHMgOiBT
  ZWxmLCBjb3JlIDogQ29yZSkgOiAKICAgICAgVGFibGUgcywgICAgICAgICAgICAgICAgICAgICAg
  ICAgICAgICAgIGNvcmUKICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgfFsgICAgICAgICAg
  MCAgICAgICAgICAgfCAgICAgICAgICAxICAgICAgICAgIF18CiUgICAgICAgLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS18
  fAogICAgICAgIHwgbWVtb3J5ICAgICAgICAgICAgICAgfCAobW9kaWZpZWQoMCksIGRfbSkgICB8
  IChtb2RpZmllZCgxKSwgZF9tKSAgfHwKJSAgICAgICAtLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLXx8CiAgICAgICAgfCBt
  b2RpZmllZCgwKSAgICAgICAgICB8IChtb2RpZmllZCgwKSwgZF9jKSAgIHwgKG1vZGlmaWVkKDEp
  LCBkX2N0KSB8fAolICAgICAgIC0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tfHwKICAgICAgICB8IG1vZGlmaWVkKDEpICAg
  ICAgICAgIHwgKG1vZGlmaWVkKDApLCBkX2N0KSAgfCAobW9kaWZpZWQoMSksIGRfYykgIHx8IAol
  ICAgICAgIC0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tfHwKICAgICAgICB8IGV4Y2x1c2l2ZSgwKSAgICAgICAgIHwgKG1v
  ZGlmaWVkKDApLCBkX2MpICAgfCAobW9kaWZpZWQoMSksIGRfbSkgIHx8CiUgICAgICAgLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS18fAogICAgICAgIHwgZXhjbHVzaXZlKDEpICAgICAgICAgfCAobW9kaWZpZWQoMCksIGRf
  bSkgICB8IChtb2RpZmllZCgxKSwgZF9jKSAgfHwKJSAgICAgICAtLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLXx8CiAgICAg
  ICAgfCBzaGFyZWQoc2luZ2xldG9uW0NvcmVdKDApKSAKCSAgICAgICAgICAgICAgICAgICAgICAg
  fCAobW9kaWZpZWQoMCksIGRfYykgICB8IChtb2RpZmllZCgxKSwgZF9tKSAgfHwKJSAgICAgICAt
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLXx8CiAgICAgICAgfCBzaGFyZWQoc2luZ2xldG9uW0NvcmVdKDEpKSAKCSAgICAg
  ICAgICAgICAgICAgICAgICAgfCAobW9kaWZpZWQoMCksIGRfbSkgICB8IChtb2RpZmllZCgxKSwg
  ZF9jKSAgfHwKJSAgICAgICAtLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLXx8CiAgICAgICAgfCBzaGFyZWQodHdpbltDb3Jl
  XSgwLDEpKSAgICAKCSAgICAgICAgICAgICAgICAgICAgICAgfCAobW9kaWZpZWQoMCksIGRfYykg
  ICB8IChtb2RpZmllZCgxKSwgZF9jKSAgfHwKJSAgICAgICAtLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLXx8CiAgICAgIEVu
  ZFRhYmxlCgoKICBleGNoYW5nZShkX2MsIGRfbSwgZF9jdCwgZF93YiA6IERlbGF5KSA6IFtTZWxm
  LCBDb3JlIC0+IFtTZWxmLCBEZWxheV1dID0gCiAgICBMYW1iZGEocyA6IFNlbGYsIGNvcmUgOiBD
  b3JlKSA6IAogICAgICBUYWJsZSBzLCAgICAgICAgICAgICAgICAgICAgICAgIGNvcmUKICAgICAg
  ICAgICAgICAgICAgICB8WyAgICAgICAgICAgIDAgICAgICAgICAgICAgIHwgICAgICAgICAgICAx
  ICAgICAgICAgICAgICBdfAolICAgICAtLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLXx8CiAgICAgIHwgbWVtb3J5ICAg
  ICAgIHwgKG1vZGlmaWVkKDApLCBkX20gKyBkX2MpICB8IChtb2RpZmllZCgxKSwgZF9tICsgZF9j
  KSAgfHwKJSAgICAgLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS18fAogICAgICB8IG1vZGlmaWVkKDApICB8IChtb2Rp
  ZmllZCgwKSwgZF9jICsgZF9jKSAgfCAobW9kaWZpZWQoMSksIGRfY3QgKyBkX2MpIHx8CiUgICAg
  IC0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tfHwKICAgICAgfCBtb2RpZmllZCgxKSAgfCAobW9kaWZpZWQoMCksIGRf
  Y3QgKyBkX2MpIHwgKG1vZGlmaWVkKDEpLCBkX2MgKyBkX2MpICB8fCAKJSAgICAgLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS18fAogICAgICB8IGV4Y2x1c2l2ZSgwKSB8IChtb2RpZmllZCgwKSwgZF9jICsgZF9jKSAg
  fCAobW9kaWZpZWQoMSksIGRfbSArIGRfYykgIHx8CiUgICAgIC0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tfHwKICAg
  ICAgfCBleGNsdXNpdmUoMSkgfCAobW9kaWZpZWQoMCksIGRfbSArIGRfYykgIHwgKG1vZGlmaWVk
  KDEpLCBkX2MgKyBkX2MpICB8fAolICAgICAtLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLXx8CiAgICAgIHwgc2hhcmVk
  KHNpbmdsZXRvbltDb3JlXSgwKSkgfCAKICAgICAgICAgICAgICAgICAgICAgICAobW9kaWZpZWQo
  MCksIGRfYyArIGRfYykgIHwgKG1vZGlmaWVkKDEpLCBkX20gKyBkX2MpICB8fAolICAgICAtLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLXx8CiAgICAgIHwgc2hhcmVkKHNpbmdsZXRvbltDb3JlXSgxKSkgfCAKICAgICAg
  ICAgICAgICAgICAgICAgICAobW9kaWZpZWQoMCksIGRfbSArIGRfYykgIHwgKG1vZGlmaWVkKDEp
  LCBkX2MgKyBkX2MpICB8fAolICAgICAtLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLXx8CiAgICAgIHwgc2hhcmVkKHR3
  aW5bQ29yZV0oMCwxKSkgICAgfCAKICAgICAgICAgICAgICAgICAgICAgICAobW9kaWZpZWQoMCks
  IGRfYyArIGRfYykgIHwgKG1vZGlmaWVkKDEpLCBkX2MgKyBkX2MpICB8fAolICAgICAtLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLXx8CiAgICAgIEVuZFRhYmxlCgoKICByZXBsYWNlKGRfYywgZF9tLCBkX2N0LCBkX3di
  IDogRGVsYXkpIDogW1NlbGYsIENvcmUgLT4gW1NlbGYsIERlbGF5XV0gPSAKICAgIExhbWJkYShz
  IDogU2VsZiwgY29yZSA6IENvcmUpIDogCiAgICAgIFRhYmxlIHMsICAgICAgICAgICBjb3JlCgkJ
  ICAgICAgICAgICAgICAgIHxbICAgICAgIDAgICAgICAgICAgfCAgICAgICAgIDEgICAgICAgICAg
  ICAgXXwKJSAgIC0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLXx8CiAgICB8IG1lbW9yeSAgICAgICAgICAgICAgICAg
  ICAgIHwgKG1lbW9yeSwgMCkgICAgICB8IChtZW1vcnksIDApICAgICAgICAgICB8fAolICAgLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tfHwKICAgIHwgbW9kaWZpZWQoMCkgICAgICAgICAgICAgICAgfCAobWVtb3J5
  LCBkX3diKSAgIHwgKG1vZGlmaWVkKDApLCAwKSAgICAgIHx8CiUgICAtLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS18
  fAogICAgfCBtb2RpZmllZCgxKSAgICAgICAgICAgICAgICB8IChtb2RpZmllZCgxKSwgMCkgfCAo
  bWVtb3J5LCBkX3diKSAgICAgICAgfHwgCiUgICAtLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS18fAogICAgfCBleGNs
  dXNpdmUoMCkgICAgICAgICAgICAgICB8IChtZW1vcnksIDApICAgICAgfCAobWVtb3J5LCAwKSAg
  ICAgICAgICAgfHwKJSAgIC0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLXx8CiAgICB8IGV4Y2x1c2l2ZSgxKSAgICAg
  ICAgICAgICAgIHwgKG1lbW9yeSwgMCkgICAgICB8IChtZW1vcnksIDApICAgICAgICAgICB8fAol
  ICAgLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tfHwKICAgIHwgc2hhcmVkKHNpbmdsZXRvbltDb3JlXSgwKSkgfCAo
  bWVtb3J5LCAwKSAgICAgIHwKICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg
  ICAgICAoc2hhcmVkKHNpbmdsZXRvbltDb3JlXSgwKSksIDApIHx8CiUgICAtLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS18fAogICAgfCBzaGFyZWQoc2luZ2xldG9uW0NvcmVdKDEpKSB8IChzaGFyZWQoc2luZ2xldG9u
  W0NvcmVdKDEpKSwgMCkgCiAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAg
  ICAgICAgICAgICB8IChtZW1vcnksIDApICAgICAgICAgICB8fAolICAgLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  fHwKICAgIHwgc2hhcmVkKHR3aW5bQ29yZV0oMCwxKSkgICAgfCAoc2hhcmVkKHNpbmdsZXRvbltD
  b3JlXSgxKSksIDApIAogICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICAgICB8
  IChzaGFyZWQoc2luZ2xldG9uW0NvcmVdKDApKSwgMCkgfHwKJSAgIC0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLXx8
  CiAgICAgIEVuZFRhYmxlCgoKJSAgcmVhZChkX2MsIGRfbSwgZF9jdCwgZF93YiA6IERlbGF5KSA6
  IFtTZWxmLCBDb3JlIC0+IFtTZWxmLCBEZWxheV1dID0gCiUgICAgTGFtYmRhKHMgOiBTZWxmLCBj
  b3JlIDogQ29yZSkgOiAKJSAgICAgIFRhYmxlIHMsICAgICAgICAgICBjb3JlCiUJCSAgfFsgICAg
  ICAgICAgICAwICAgICAgICAgICAgICAgfCAgICAgICAgICAgICAxICAgICAgICAgICAgICBdfAol
  JSAgIC0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS18fAolICAgIHwgbWVtb3J5ICAgICAgIHwgKGV4Y2x1c2l2ZSgw
  KSwgZF9tKSAgICAgICAgfCAoZXhjbHVzaXZlKDEpLCBkX20pICAgICAgICB8fAolJSAgIC0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS18fAolICAgIHwgbW9kaWZpZWQoMCkgIHwgKG1vZGlmaWVkKDApLCBkX2MpICAg
  ICAgICAgfCAoc2hhcmVkKHR3aW4oMCwxKSksIGRfY3QpICB8fAolJSAgIC0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS18fAolICAgIHwgbW9kaWZpZWQoMSkgIHwgKHNoYXJlZCh0d2luKDAsMSkpLCBkX2N0KSAgfCAo
  bW9kaWZpZWQoMSksIGRfYykgICAgICAgICB8fCAKJSUgICAtLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tfHwKJSAg
  ICB8IGV4Y2x1c2l2ZSgwKSB8IChleGNsdXNpdmUoMCksIGRfYykgICAgICAgIHwgKHNoYXJlZCh0
  d2luKDAsMSkpLCBkX20pICAgfHwKJSUgICAtLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tfHwKJSAgICB8IGV4Y2x1
  c2l2ZSgxKSB8IChzaGFyZWQodHdpbigwLDEpKSwgZF9tKSAgIHwgKGV4Y2x1c2l2ZSgxKSwgZF9j
  KSAgICAgICAgfHwKJSUgICAtLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tfHwKJSAgICB8IHNoYXJlZChzaW5nbGV0
  b24oMCkpIHwKJSAgICAgICAgICAgICAgICAgICAgKHNoYXJlZChzaW5nbGV0b24oMCkpLCBkX2Mp
  IHwgKHNoYXJlZCh0d2luKDAsMSkpLCBkX20pICAgfHwKJSUgICAtLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tfHwK
  JSAgICB8IHNoYXJlZChzaW5nbGV0b24oMSkpIHwKJSAgICAgICAgICAgICAgICAgICAgIChzaGFy
  ZWQodHdpbigwLDEpKSwgZF9tKSAgIHwgKHNoYXJlZChzaW5nbGV0b24oMSkpLGRfYykgfHwKJSUg
  ICAtLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tfHwKJSAgICB8IHNoYXJlZCh0d2luKDAsMSkpICAgIHwKJSAgICAg
  ICAgICAgICAgICAgICAgICAgKHNoYXJlZCh0d2luKDAsMSkpLCBkX2MpIHwgKHNoYXJlZCh0d2lu
  KDAsMSkpLCBkX2MpICAgfHwKJSUgICAtLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0t
  LS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tLS0tfHwKJSAgICAgIEVuZFRhYmxl
  CgoKICBtZXNpXzJfc3RhdGVzKGRfYywgZF9tLCBkX2N0LCBkX3diIDogRGVsYXkpIDogQ2FjaGVT
  aWduYXR1cmVbU2VsZiwgQ29yZV0gPSAoIwogICAgJXJlYWQgOj0gcmVhZChkX2MsIGRfbSwgZF9j
  dCwgZF93YiksCiAgICB3cml0ZSA6PSB3cml0ZShkX2MsIGRfbSwgZF9jdCwgZF93YiksCiAgICBl
  eGNoYW5nZSA6PSBleGNoYW5nZShkX2MsIGRfbSwgZF9jdCwgZF93YiksCiAgICByZXBsYWNlIDo9
  IHJlcGxhY2UoZF9jLCBkX20sIGRfY3QsIGRfd2IpCiAgIykKCgpFbmQgTUVTSVN0YXRlTW9kZWxf
  MgoKCgpNRVNJU3RhdGVNb2RlbF9OIDogVGhlb3J5CkJlZ2luCgogIG51bWJlcl9vZl9jb3Jlc191
  bmRlZiA6IG5hdAoKICBDb3JlIDogVHlwZSA9IGJlbG93KG51bWJlcl9vZl9jb3Jlc191bmRlZikK
  CiAgSW1wb3J0aW5nIENhY2hlSW50ZXJmYWNlLCBNRVNJU3RhdGUKCiAgU2VsZiA6IFR5cGUgPSBN
  RVNJU3RhdGVbbnVtYmVyX29mX2NvcmVzX3VuZGVmXQoKICB3cml0ZShkX2MsIGRfbSwgZF9jdCwg
  ZF93YiA6IERlbGF5KSA6IFtTZWxmLCBDb3JlIC0+IFtTZWxmLCBEZWxheV1dID0gCiAgICBMYW1i
  ZGEocyA6IFNlbGYsIGNvcmUgOiBDb3JlKSA6IAogICAgICBDYXNlcyBzIE9GCiAgICAgICAgbWVt
  b3J5ICAgICAgOiAobW9kaWZpZWQoY29yZSksIGRfbSksCgltb2RpZmllZChpKSA6IAoJICBJRiBp
  ID0gY29yZQoJICBUaGVuIChzLCBkX2MpCgkgIEVsc2UgKG1vZGlmaWVkKGNvcmUpLCBkX2N0KQoJ
  ICBFbmRJRiwKCWV4Y2x1c2l2ZShpKSA6CgkgIElGIGkgPSBjb3JlCgkgIFRoZW4gKG1vZGlmaWVk
  KGNvcmUpLCBkX2MpCgkgIEVsc2UgKG1vZGlmaWVkKGNvcmUpLCBkX20pCgkgIEVuZElGLAoJc2hh
  cmVkKGlzKSA6CgkgIElGIG1lbWJlcihjb3JlLCBpcykKCSAgVGhlbiAobW9kaWZpZWQoY29yZSks
  IGRfYykKCSAgRWxzZSAobW9kaWZpZWQoY29yZSksIGRfbSkKCSAgRW5kSUYKICAgICAgRW5kQ2Fz
  ZXMKCgogIGV4Y2hhbmdlKGRfYywgZF9tLCBkX2N0LCBkX3diIDogRGVsYXkpIDogW1NlbGYsIENv
  cmUgLT4gW1NlbGYsIERlbGF5XV0gPSAKICAgIExhbWJkYShzIDogU2VsZiwgY29yZSA6IENvcmUp
  IDogCiAgICAgIENhc2VzIHMgT0YKICAgICAgICBtZW1vcnkgICAgICA6IChtb2RpZmllZChjb3Jl
  KSwgZF9tICsgZF9jKSwKCW1vZGlmaWVkKGkpIDogCgkgIElGIGkgPSBjb3JlCgkgIFRoZW4gKHMs
  IGRfYyArIGRfYykKCSAgRWxzZSAobW9kaWZpZWQoY29yZSksIGRfY3QgKyBkX2MpCgkgIEVuZElG
  LAoJZXhjbHVzaXZlKGkpIDoKCSAgSUYgaSA9IGNvcmUKCSAgVGhlbiAobW9kaWZpZWQoY29yZSks
  IGRfYyArIGRfYykKCSAgRWxzZSAobW9kaWZpZWQoY29yZSksIGRfbSArIGRfYykKCSAgRW5kSUYs
  CglzaGFyZWQoaXMpIDoKCSAgSUYgbWVtYmVyKGNvcmUsIGlzKQoJICBUaGVuIChtb2RpZmllZChj
  b3JlKSwgZF9jICsgZF9jKQoJICBFbHNlIChtb2RpZmllZChjb3JlKSwgZF9tICsgZF9jKQoJICBF
  bmRJRgogICAgICBFbmRDYXNlcwoKCiAgcmVwbGFjZShkX2MsIGRfbSwgZF9jdCwgZF93YiA6IERl
  bGF5KSA6IFtTZWxmLCBDb3JlIC0+IFtTZWxmLCBEZWxheV1dID0gCiAgICBMYW1iZGEocyA6IFNl
  bGYsIGNvcmUgOiBDb3JlKSA6IAogICAgICBDYXNlcyBzIE9GCiAgICAgICAgbWVtb3J5ICAgICAg
  OiAobWVtb3J5LCAwKSwKCW1vZGlmaWVkKGkpIDogCgkgIElGIGkgPSBjb3JlCgkgIFRoZW4gKG1l
  bW9yeSwgZF93YikKCSAgRWxzZSAocywgMCkKCSAgRW5kSUYsCglleGNsdXNpdmUoaSkgOgoJICBJ
  RiBpID0gY29yZSAgCgkgICUgZGlzdGluZ3Vpc2ggY2FzZXMgaGVyZSBiZWNhdXNlIHRoZSBlbHNl
  IHZhcmlhbnQgaXMgaW1wb3NzaWJsZQoJICBUaGVuIChtZW1vcnksIDApCgkgIEVsc2UgKG1lbW9y
  eSwgMCkgCgkgIEVuZElGLAoJc2hhcmVkKGlzKSA6CgkgIElGIGlzID0gc2luZ2xldG9uKGNvcmUp
  CgkgIFRoZW4gKG1lbW9yeSwgMCkKCSAgRWxzSUYgbWVtYmVyKGNvcmUsIGlzKQoJICBUaGVuIChz
  aGFyZWQocmVtb3ZlKGNvcmUsIGlzKSksIDApCgkgIEVsc2UgKHMsIDApCgkgIEVuZElGCiAgICAg
  IEVuZENhc2VzCgogIG1lc2lfbl9zdGF0ZXMoZF9jLCBkX20sIGRfY3QsIGRfd2IgOiBEZWxheSkg
  OiBDYWNoZVNpZ25hdHVyZVtTZWxmLCBDb3JlXSA9ICgjCiAgICAlcmVhZCA6PSByZWFkKGRfYywg
  ZF9tLCBkX2N0LCBkX3diKSwKICAgIHdyaXRlIDo9IHdyaXRlKGRfYywgZF9tLCBkX2N0LCBkX3di
  KSwKICAgIGV4Y2hhbmdlIDo9IGV4Y2hhbmdlKGRfYywgZF9tLCBkX2N0LCBkX3diKSwKICAgIHJl
  cGxhY2UgOj0gcmVwbGFjZShkX2MsIGRfbSwgZF9jdCwgZF93YikKICAjKQoKCkVuZCBNRVNJU3Rh
  dGVNb2RlbF9OCiAgICAgIAoKTUVTSV9FcXVpdiA6IFRoZW9yeQpCZWdpbgogIEltcG9ydGluZyBN
  RVNJU3RhdGVNb2RlbF8yLCBNRVNJU3RhdGVNb2RlbF9OCgogIGVxdWl2IDogTGVtbWEgCiAgICBu
  dW1iZXJfb2ZfY29yZXNfdW5kZWYgPSBudW1iZXJfb2ZfY29yZXNfZGVmCiAgICAgIEltcGxpZXMK
  CW1lc2lfMl9zdGF0ZXMgPSBtZXNpX25fc3RhdGVzCgpFbmQgTUVTSV9FcXVpdgo=
  --UGryaBjJit
  Content-Type: application/octet-stream; name="simple-mesi-trivial-truth.prf"
  Content-Disposition: attachment;
  	filename="simple-mesi-trivial-truth.prf"
  Content-Transfer-Encoding: base64
  
  KE1vcmVTZXRzCiAodHdpbl9UQ0MxIDAKICAodHdpbl9UQ0MxLTEgbmlsIDM0ODg2ODkzODkgbmls
  ICgiIiAoc3VidHlwZS10Y2MpIG5pbCBuaWwpIG5pbCBuaWwKICAgbmlsIG5pbCBuaWwgbmlsKSkp
  CihUeXBlc0RlZmluaXRpb25zKQooQ2FjaGVJbnRlcmZhY2UpCihNRVNJU3RhdGUpCihNRVNJU3Rh
  dGVNb2RlbF8yCiAod3JpdGVfVENDMSAwCiAgKHdyaXRlX1RDQzEtMSBuaWwgMzQ4ODY4OTM5NSBu
  aWwgKCIiIChzdWJ0eXBlLXRjYykgbmlsIG5pbCkgbmlsIG5pbAogICBuaWwgbmlsIG5pbCBuaWwp
  KQogKHdyaXRlX1RDQzIgMAogICh3cml0ZV9UQ0MyLTEgbmlsIDM0ODg2ODkzOTUgbmlsICgiIiAo
  c3VidHlwZS10Y2MpIG5pbCBuaWwpIG5pbCBuaWwKICAgbmlsIG5pbCBuaWwgbmlsKSkKICh3cml0
  ZV9UQ0MzIDAKICAod3JpdGVfVENDMy0xIG5pbCAzNDg4Njg5Mzk1IG5pbCAoIiIgKGNvbmQtY292
  ZXJhZ2UtdGNjKSBuaWwgbmlsKSBuaWwKICAgbmlsIG5pbCBuaWwgbmlsIG5pbCkpCiAod3JpdGVf
  VENDNCAwCiAgKHdyaXRlX1RDQzQtMSBuaWwgMzQ4ODY4OTM5NSBuaWwgKCIiIChzdWJ0eXBlLXRj
  YykgbmlsIG5pbCkgbmlsIG5pbAogICBuaWwgbmlsIG5pbCBuaWwpKQogKHdyaXRlX1RDQzUgMAog
  ICh3cml0ZV9UQ0M1LTEgbmlsIDM0ODg2ODkzOTUgbmlsICgiIiAoc3VidHlwZS10Y2MpIG5pbCBu
  aWwpIG5pbCBuaWwKICAgbmlsIG5pbCBuaWwgbmlsKSkKICh3cml0ZV9UQ0M2IDAKICAod3JpdGVf
  VENDNi0xIG5pbCAzNDg4Njg5Mzk1IG5pbCAoIiIgKGNvbmQtY292ZXJhZ2UtdGNjKSBuaWwgbmls
  KSBuaWwKICAgbmlsIG5pbCBuaWwgbmlsIG5pbCkpCiAod3JpdGVfVENDNyAwCiAgKHdyaXRlX1RD
  QzctMSBuaWwgMzQ4ODY4OTM5NSBuaWwgKCIiIChzdWJ0eXBlLXRjYykgbmlsIG5pbCkgbmlsIG5p
  bAogICBuaWwgbmlsIG5pbCBuaWwpKQogKHdyaXRlX1RDQzggMAogICh3cml0ZV9UQ0M4LTEgbmls
  IDM0ODg2ODkzOTUgbmlsICgiIiAoY29uZC1jb3ZlcmFnZS10Y2MpIG5pbCBuaWwpIG5pbAogICBu
  aWwgbmlsIG5pbCBuaWwgbmlsKSkKICh3cml0ZV9UQ0M5IDAKICAod3JpdGVfVENDOS0xIG5pbCAz
  NDg4Njg5Mzk1IG5pbCAoIiIgKGNvbmQtY292ZXJhZ2UtdGNjKSBuaWwgbmlsKSBuaWwKICAgbmls
  IG5pbCBuaWwgbmlsIG5pbCkpCiAod3JpdGVfVENDMTAgMAogICh3cml0ZV9UQ0MxMC0xIG5pbCAz
  NDg4Njg5Mzk1IG5pbCAoIiIgKGNvbmQtY292ZXJhZ2UtdGNjKSBuaWwgbmlsKQogICBuaWwgbmls
  IG5pbCBuaWwgbmlsIG5pbCkpCiAod3JpdGVfVENDMTEgMAogICh3cml0ZV9UQ0MxMS0xIG5pbCAz
  NDg4Njg5Mzk1IG5pbCAoIiIgKGNvbmQtY292ZXJhZ2UtdGNjKSBuaWwgbmlsKQogICBuaWwgbmls
  IG5pbCBuaWwgbmlsIG5pbCkpCiAod3JpdGVfVENDMTIgMAogICh3cml0ZV9UQ0MxMi0xIG5pbCAz
  NDg4Njg5Mzk1IG5pbCAoIiIgKGNvbmQtY292ZXJhZ2UtdGNjKSBuaWwgbmlsKQogICBuaWwgbmls
  IG5pbCBuaWwgbmlsIG5pbCkpCiAod3JpdGVfVENDMTMgMAogICh3cml0ZV9UQ0MxMy0xIG5pbCAz
  NDg4Njg5Mzk1IG5pbCAoIiIgKGNvbmQtY292ZXJhZ2UtdGNjKSBuaWwgbmlsKQogICBuaWwgbmls
  IG5pbCBuaWwgbmlsIG5pbCkpCiAod3JpdGVfVENDMTQgMAogICh3cml0ZV9UQ0MxNC0xIG5pbCAz
  NDg4Njg5Mzk1IG5pbCAoIiIgKGNvbmQtZGlzam9pbnQtdGNjKSBuaWwgbmlsKQogICBuaWwgbmls
  IG5pbCBuaWwgbmlsIG5pbCkpCiAod3JpdGVfVENDMTUgMAogICh3cml0ZV9UQ0MxNS0xIG5pbCAz
  NDg4Njg5Mzk1IG5pbCAoIiIgKGNvbmQtY292ZXJhZ2UtdGNjKSBuaWwgbmlsKQogICBuaWwgbmls
  IG5pbCBuaWwgbmlsIG5pbCkpCiAocmVwbGFjZV9UQ0MxIDAKICAocmVwbGFjZV9UQ0MxLTEgbmls
  IDM0ODg2ODkzOTUgbmlsICgiIiAoY29uZC1kaXNqb2ludC10Y2MpIG5pbCBuaWwpCiAgIG5pbCBu
  aWwgbmlsIG5pbCBuaWwgbmlsKSkpCihNRVNJU3RhdGVNb2RlbF9OCiAocmVwbGFjZV9UQ0MxIDAK
  ICAocmVwbGFjZV9UQ0MxLTEgbmlsIDM0ODg2ODk0MDUgbmlsICgiIiAoc3VidHlwZS10Y2MpIG5p
  bCBuaWwpIG5pbCBuaWwKICAgbmlsIG5pbCBuaWwgbmlsKSkpCihNRVNJX0VxdWl2CiAoZXF1aXZf
  VENDMSAwCiAgKGVxdWl2X1RDQzEtMSBuaWwgMzQ4ODY4OTQwNSBuaWwgKCIiIChzdWJ0eXBlLXRj
  YykgbmlsIG5pbCkgbmlsIG5pbAogICBuaWwgbmlsIG5pbCBuaWwpKQogKGVxdWl2IDAKICAoZXF1
  aXYtMSBuaWwgMzQ4ODY4OTQ2MiAzNDg4Njg5NTYxCiAgICgiIiAoc2tvc2ltcCogOnByZWRzPyB0
  KQogICAgKCgiIiAoYXBwbHktZXh0ZW5zaW9uYWxpdHkgOmhpZGU/IHQpCiAgICAgICgoIiIgKGV4
  cGFuZCAibWVzaV8yX3N0YXRlcyIpCiAgICAgICAgKCgiIiAoZXhwYW5kICJtZXNpX25fc3RhdGVz
  IikKICAgICAgICAgICgoIiIgKHByb3ApCiAgICAgICAgICAgICgoIjEiIChhcHBseS1leHRlbnNp
  b25hbGl0eSA6aGlkZT8gdCkKICAgICAgICAgICAgICAoKCIxIiAoZXhwYW5kICJ3cml0ZSIpCiAg
  ICAgICAgICAgICAgICAoKCIxIiAocmVwbGFjZSAtMSA6YWN0dWFscz8gVCkKICAgICAgICAgICAg
  ICAgICAgKCgiMSIgKGNhc2UgIm1lbW9yeT8oeCE1KSBhbmQgeCE2ID0gMCIpCiAgICAgICAgICAg
  ICAgICAgICAgKCgiMSIgKGZsYXR0ZW4pCiAgICAgICAgICAgICAgICAgICAgICAoKCIxIiAoYXNz
  ZXJ0KQogICAgICAgICAgICAgICAgICAgICAgICAoKCIxIiAocmVwbGFjZSAtMiAqIExSKQogICAg
  ICAgICAgICAgICAgICAgICAgICAgICgoIjEiIChhc3NlcnQpICgoIjEiIChwb3N0cG9uZSkgbmls
  IG5pbCkpCiAgICAgICAgICAgICAgICAgICAgICAgICAgICBuaWwpKQogICAgICAgICAgICAgICAg
  ICAgICAgICAgIG5pbCkpCiAgICAgICAgICAgICAgICAgICAgICAgIG5pbCkpCiAgICAgICAgICAg
  ICAgICAgICAgICBuaWwpCiAgICAgICAgICAgICAgICAgICAgICgiMiIgKHBvc3Rwb25lKSBuaWwg
  bmlsKSkKICAgICAgICAgICAgICAgICAgICBuaWwpKQogICAgICAgICAgICAgICAgICBuaWwpKQog
  ICAgICAgICAgICAgICAgbmlsKSkKICAgICAgICAgICAgICBuaWwpCiAgICAgICAgICAgICAoIjIi
  IChwb3N0cG9uZSkgbmlsIG5pbCkgKCIzIiAocG9zdHBvbmUpIG5pbCBuaWwpKQogICAgICAgICAg
  ICBuaWwpKQogICAgICAgICAgbmlsKSkKICAgICAgICBuaWwpKQogICAgICBuaWwpKQogICAgbmls
  KQogICB1bmZpbmlzaGVkIG5pbCA5ODUzNSAyNDAgdCBzaG9zdGFrKSkpCgo=
  --UGryaBjJit--

How-To-Repeat: 

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