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

PVS Bug 872


Synopsis:        show-proofs-theory broken
Severity:        serious
Priority:        medium
Responsible:     owre (Sam Owre)
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Nov 24 15:40:00 2004
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 3.2
Environment: 
 System:          
 Architecture: 

Description: 
  
  --fC8awkkfQC
  Content-Type: text/plain; charset=us-ascii
  Content-Description: message body text
  Content-Transfer-Encoding: 7bit
  
  Hi,
  
  M-x show-proofs-theory on More_List_Props in the appended archive
  reports No proofs found in this theory. PVS 3.1 shows all the
  proofs as expected.
  
  Bye,
  
  Hendrik
  
  
  --fC8awkkfQC
  Content-Type: application/octet-stream
  Content-Disposition: attachment;
  	filename="bug-2.tar.gz"
  Content-Transfer-Encoding: base64
  
  H4sIAMmIpEEAA+19+XPbRpawf7X+ig6nUgXG5CwBXqLWHpcnsXf9fU6scjwbeVwqFiWBMickyOER
  S6n947dv9Al0N0hZsoGqxCLQd7/7vX79a7r4j0cHfjrwGfb7+N9ef4D/7QwS8i95HsWduB/HnV7S
  GT7qxPFg2H8E+oceGHp2m+1kDcCjbfp5U1QOFptOC76zibB/H8jzK9z/3XY2n21v/7paF00w/MHb
  3euZ97/b78TDhO1/dziE3+Ne3O0+AneyiN/4/kc/L9fp+M1ssx2frperzTg5AtE8za63n8aLyQp0
  joD4ux2DbDYH3W7nuD8YJMcx/DPuJMejbjyAJUHUaIBoll3tLrftSXbV3swWq/lsegsa80YTV4X/
  NcFqvfwjvcIVojnsG2xvV2n7Kr3E3wF6NZ5cbXFhVApEF8vlPJ1kIFtm6WK1vW3LNejnjVDj72C6
  XC8mc6WkNl+hSrZbXKRrWx/kq9jFM3C5zDZbUqTx8X0LvAftv7HBnDdA+u/dBKLWLN1ovYyns3R+
  NV6t0yu5FToIqR2xyga3YmlPGft0vVyoE6CtCA2s08ncOhDarjQcVEFtoLBnrcJkO1tmxl5xW3Jv
  tLCpgeJeDRVn2Ta9hrMydMyalDqn5ZUmlG7Tf+edGiqg1gpqGGD3bzJkoRL6qmeTonHAr7v1ZK4D
  LUFmcJVOaeuwZIOg3AphhFAUEQCIhu28LCr28X183uA4iqlEXuWFP9bhlgjNgBuA6+/mEws1wHXi
  YRdAZgG2YPNpCQnz7+h1lBESNX7/448xoVviG5FyxZC99DDl6gz6g17MKdfm9yWiWD+AEwQfm+dg
  24QUCn1Zp5/Xs20KV4DTQoGgNfl0CGVrXy4h3Uu3KSFxAaRIIMHaghTV86eT/tD5y9v3MurgJija
  QNAwVPGlrDWNjJ46kIBvi44ekioG0q1ywcWD3F6k8+Vn4DJmXAGSsJ6FBkrkT6Z8vcHALrNhMY0M
  JmrEZoJIUIsVSG9WUM5jZLHRZO8nm0263qoUMqeTqNukrINE7wC0Y1ZAK4JoMhA+awUy1IBUgBfZ
  LCabT032i1H7dmKegdiE/Fv8Jc61a+cu3XL2cqQ2LrMbKkgHsgyEU88xn1+nl8vrbPZnumbIjGFc
  QmQDiKMGcH2MnWsIR0veABKKUZVz1ArpqmluBcK3iTxLmGAhzm2NKOMiLcDbhJ2zv1VWUZWxzeeV
  Fg81YFk80njTWM1LaAomcZlEud57060xelldYwqRn5yIs69Y4i9d1YLMNyak3C9lz0WIPIiEEqBA
  4jq9bh8kx5JY0zzSjFRdKOrAb6mg6/GfXNxBMk7neNRj4k6nf1yk6DGxxyLU5DKCTaQReXGthn0t
  1MsJO78tEudNi3C9/gh0EV7TFxxhExl/k/3jL9IZahSuUbhG4aoo3CUWB4bCVONEqCs5itALCY2P
  O0PuKYq7utUhk60O12v4IcfSavaCrmYvIETAbiZAw2+AxGgnUJtPim0GUhOqrcD0ptiaYFf+AyhJ
  db3/ao2rTy4v080m1/mpmo/qY9XfrPdOCvVXq0iJgU2VJ2EXmohYWev0kIufulCY1z+fvnn98ld9
  m1qgfLPc9Nn3boqyuDaY6mgUAE56lqVXmv4eqIY4UWB/9ulN9vZAaoPJfHUG4614V+W0lXn9voWP
  UPuLi7hEOFwn7o1APBiYDOuKxim9UthdMvSXWlUbMGZDTHAts6cbDMGYUpZagrvVyMehojdqWbqW
  pb9qWRoK0okoS4vUJNEJTFJEYCh12V3g3reXl7LsXGu1NSbWmGjXahOEiYLKxhFPRkMJA0fxIGF/
  JqPRnWq0vYNotBlRZxWNtdg93i13j/uquGxpShzmZnmIVe7ZK/fskpaqtRdr3MFS1sNT1b+8Zz7U
  WnBPHNh+SvbBxPDa3V27u79qd3clE9uLX34Kq1jsZHe0DnpYG/1MoLhS3B12hwMw6nRUw8Z2MpuP
  L9JPkLoyRxx/Iescx13BFddVJB7ltEdmO+1Rk6CaBH3VJOiesPpKlPBv+6VXYTITokO+jp4vFY0Z
  Kp5WEssrKAWEJ3SSYQJ0Uzc2OeHVzwMz0E+JGyTHndhk4n64Hl00RbsCzEpNVqs0uzKUAwY/sFaE
  F4LNzG/b6c02zTaYLM62t+Dk0+wqxXqqolRr7ZjeVlW87ZpuiML6hQA7J5Fj1MpYWWGXMOn9RLNf
  TkoX4P2+HeP+9DLEmU4wwFRrj8S/9r3Xvvfa9/5t+d6T4RAkiSqNYEyTybjgg7d9lWSVYdw3yipG
  h5nsLfOMd/cgWwcjKockE98W0judwK0Jg69JJ0Cc9GdPPtQKV+kdo/B0LnibKY+V6Kj0pp/TG903
  OI/3pxwhsiKpQ6bDt7kOYG2VKyYFfjXSQLfkUC5gLjpNKeNfirUfXQGL8eIhwT8BjU7DqHqhMqgF
  7JQ0L6w6F3lR1DnF9jUx6HV2PU19SdpE03kuqbLCXPSN1T7bAcNYnKxeFzRm38XgSWxYQmkhjRBp
  KG1ZOFv5YiCzVbN/89+MfSvNDFe7DPoS7qE2Ap9dya6ssybjPyZruLsQMubpoi1SWCe9DlWI7W28
  L7O8BfuIn+zJRzwzDxzLcFQyExeq2WyQ3StclC9qx9jXwfowm2ZVW2oAnw841R4iIe87KCDYc/j6
  1atDmiTuItivkmXFV3SsE66Fah3flEfwnqRPc9EfPXP+9I8T0MuP0RqOxveg5jK5uhoTckBstVhr
  UV5KGks36fBoxm7SVzQWNZNjXC2V4+m7lz+5Wz3TP9L1rZJEgEKLkesE0+Iw2sJWVaqMQULbGLGW
  nw39HghXtfG5Nj5/pcbnYNETTmt3mSq0icvG60l2nYp5Tmjx3OLU7YPuULV3czKdB6BLryS6HR8P
  hya6XXzQjJhJuJqOXuYWpN0mBQ2FVzTAyWZ3sdnKynOEOAHxrUfz72JIUqBSBV/MkwbxpgtvBRVa
  OezGwwskmwQrtJpPLtFYwQ9gvnY5C2dX1e2qdx7w4BXHfWcOV4Wblw6yVwlx7uV5Hz+ZwU0OuTPJ
  otY/Hrb+cRjX2EPL6IUrJJ0uiHsl6bmOmIA7pgMhXEx8xbhYMholcb/bzblYN8/GfBDt4/CSRG2k
  +BaJxAMPW/YgGQ9PeXWzEYcqA4QwDmKQGFPSU7onJI1gb2QiGOfHK7rdRCGCWkAtlfAFGV7MxozO
  ckoSt/iRyfSqz9aQzpllToutqdOEJorFb/Ln/kJ+y2ZjDAvWahceei2K5FWKNCTuZnSv+tdQ5lGw
  9OYtKHqrv/PbTrs2FaANyNJCmX4jVHyYKazuyaFUTzq+Z8N3uM/svoTyChXqQN7allrbUrlhE4W/
  acltKJFPlAxa0msniajYuEmNg4JtU8/3QGWGEnuiE7eTWrQIiocM/a20r/fS1FcrwnVqn32l9omH
  Cb4ojGO2Qot0MlRAgdQj7546GddlBG1CUq3s2hijV6omY2o+V9gQ2ZncFKsNd6DDGRS0glObIVMS
  Z2RS7yxX/tjVO8s4Ehrd6TYSfTRsJQqifg2K76GikI1x3L2SBEv7ViMZRFmyPeUQ1XVRnUvKuU7N
  nfsHK64P7kjtA9d1D5GVwVuiq3Of1E6Er9qJ8GXSL+3ZMHV37o1KyfEYt+IMatA9hpq3qHVP55Pt
  Ns0EhVt8I14L2enHfaOku03Xi1mGwbfgmKzTDjShJH4MRkQYF50kixRPS4xVlV4JEU+dQe/4uG8X
  yb+4rzggfj70CABZIyDHruzHZff2XdiQ7sDPFvcScKy62Si4ZCzUIP+dA/noeNDt9/K7T7s9TZ2b
  7z9nDRmJSfmx30la6LziRyFj00nI0vOfQJiE6ZYz99N5ervCwUbDuISWbcqP25lG8UQjXIQMHWgE
  thONZt+lsehejoGylTF/81fbXFa9WHcSVsJyKFf4WnyuVyls3GmpBFsxqYIKV3talSpaqF3B21v+
  2i8fBJF5H49UCbeqHdyT843eB1eVugEHZ6tp8g/ozmBvjn5P9P0DJm5x0SHqHCx708Zrf62v2chH
  MQjWPvwVHX9lqkxJw8X6I6gP9i0aAdV3Ja2AvpO0yv4AtsA1A/X8I+QDB1AN6DhMugE3YEt6sHpA
  xiJt29UH1VFVKGgrukaRmG1eFLoeBWkwxMeupuARdAvzvnj0rPfhJj5zmfZygg5IoeV4BkxD0rxH
  meDHMSlntqw0NjXNJnAXKVhSIXlg+QWWqnhuaaVIwbnfyVrsYr5sgvLw49wDud5FhKVybKEg+63q
  Bw4yfpgMui/dsdYwvHxtB9BBam2i1ia+VW2CidDlh5a/LhUEV8EXwXZHWk5aEvQpaRfyO/mUfu+Y
  55/tjob3RrtQomF17YJ7MSYrLa2fGuVFD6mbXBJiOZIEQTSru4SpHVL2C4ngDc/8cH/4JMXUyUqZ
  BkHvWBw/KpRXCUt5E+ze9z2m75cqIIi8efD3+qxHze2/ILevchb9MIFquEovHvV6YKiZ7bKcgyrH
  RKTIlURgroNh/5gx12MheYDfXeuMXQrcVM2Jg9Fbzs1amBcHEk1KKJrRfM5T4yh8jcao4sQwkVal
  hbPntPAmomWwlADwH5xwx/L5CWS3TTUJT1HgOckQlGiRyvizyuCJRYxxBX0MTfAM8K/7mG7BbNFc
  UQk8XbPxU00qZDMq0ixJ9nt8YinUWMmYZDXTxS5Ck6U8F55M1w/ZRoawBwlw9hqg2DT55Q2BZsNw
  WTyGWWQ80trBGw0FdLMZ3SWwInFbbxP24PeT3XbZNl5KrArphWZgdjQB0tMVpMSuic8N5SuYY+X1
  7Za2L9cpH1GxYL/LoJg323xShHskwJamzUrCJLwDCeb1ab6vJSK9Ps23p9N8vQ4U8ZA9hp8tNkqH
  oukF1uhxQTEpPENskQwxKTdQ0prS1JSmpjRfKaXpDkCs5i+QrL2ZxdTbGR0f54EkA05vCq9FzXXO
  2GDBdVbaJAmU5ZgyHxouSohgVAT2bI0lf9qEvRK5UafAuEAP2QGGamrCf2QzKLFHrya/w21c/bEZ
  Tye/C6YF8Y1wIKYz7CfxiJnv+6NRwYVxaCjSnXE1Oa3JaU1OJXIas7vVRGOfgHuJho1JETZyslp2
  PA3/7gOlb0gPflwuIHmZoYryrxebzfISBRDejifoTxo6SH8xy2PSj4fJoDNMyPG5wQD+cLQ8Ot19
  RooyTvAXnqnG4iszEsfLT+nl74wo/WYWHdWJCzv9T+8aZ941/vcv/ysD7hmC2H9CWBUqCeU/ePRA
  7czSpX5wq39L5/PpcpddpVdQWkZMGW72Z/hyTN+O5+kN2XT1LU8N0k+Sfr/b6Zk2n+2ZWPl5QwSA
  QhduSQt5KXKhWww5+GRxcTWJbk7Omicvb6B0v4luTz40T1bfxdFN67ZpSKuuXy3nHBcqXcbXBY03
  pHfe4+13idqnVLHgVjvXwFR1GHANSLff9UwdSxW4TbcL2v1SE2oeeXnjYj11HbzjkmhFS8oAfqlg
  r6w51wZBvsQQWf41TqIbnMzfpaJkbG+n2wlowMoNl/jS/HErl0uUBeNpaK4XQ6GCI21SOafWgOJr
  WJePkrV9hwtXVqq8TFmJ4u9FX+3fbFvuHMlsfm/TdeRX8gFUjBmI8mEPH8WTWxOeeJyv9VOnClm/
  hWnqjFBgtH7pUiyMv7CHe3cJMLPG3UjDQsEkHz9+PGuBD+ctQP5FYdSFcwtzukv83qB4LNdXcm6z
  QRdokWmqzDL+1+7qOjXLM+SbJNUMup0uPxLTy82l83SxmMgiyRhzxUK5NNeM25dQRJun25SApCZv
  aRZTy/o2QRcK89jfLkrzb9KbXyZbHJh3M0YBvMIF8cIbaarDDlUplKliX//nKaokiW3FYplcZp1u
  tuvZ5TZAbi9drxLQYKouGYBU9h1SXul7AezwVJ0yOjGRWrv/4cdPE0gN4fr/uVxn48tPy+UmHWdQ
  xxE2wviJ78gw6XRH8B+TklesT7E1X06naYaWoaFcbVQsmImN/AAajFI8h6Sc/0GTOOiC9OVydavF
  B+TyuSkNgvthowaX54ySqinbqamEvj4FMjLvM3HLjao+xQy7Oh/eH5MULXZkow14tUm3hqjm0nIc
  iMqL3pjPpER8t6Ls85QctiFIJnaDvui1yZQb0ZsXP//9pxcgeto8AYjbSkTk41tEMs7hR1PLK/Oo
  MDMkFQ2V8AeLgq6WvQsbqZ8M401i/cJMA8QdDgK6QGLYA1zpeAi0kDpKd2FBnRizlyIZ7nUGnUEo
  GS6hoMXcs5xMm/RbNyon0zYjWS5ITuOTm4Z3Y0ydUtCcxDhKlb2a0gI/SuuHTndHpmpXTu3KeRiu
  HH82f09YMC4+SkC3mDcmJt6YuPFGk2O49grXpKQmJV8hKemOkAkkU9zZMt3omohJ14mYODm1cYCS
  aQh5v4K5q3+MXJW5v9L1mIzom3Lwcil+M5sH0+R+Yg5NWRRl/sUbcAIwtDThH9TLmcE/4SqhN1AP
  jjJ0zET107Exr+azrSGZoX86HDY1CCIQjzez7Jrs7vOigHwytR7OGlN8MIT7VfGM6MmdMqdmWbZP
  XtycN9M3veWXPvbBJoCWqNNsWNPX7E21YT/k7nPMjubpZrOSHT7KqedicHE8aqK0mQ8AHQgywbah
  NDe/ml30Rq9mhMgfpr8N0gA3Ld0yrDyxwUpux2KLFN02wYtffrICFy0X3baAYYkjcrir8PiLYms3
  9aQc2THaphtlTVgSR5XU6pncAfdIXVfj2r1ZqQbrhkoae99bktPwfEwB0nPg6do6ncu+hOT6gLev
  AucnR9+Fy91HCwhOIkGIu1Q3WjWr2BPhT30dlTKV7sMw+1IFS4N5idRq8pwlv5LR95MzXeFMkkO9
  EPuql9aVdPog7quuZ3T4CbeP3M/rdDpPb2Z/0IAH/jO/1K03TOIkHgiaEFGDDCl3VEZoiXLJByDR
  GdqzCZDW6RzTMlGjTECiJRnaXYx32ezfOzqb/HeuRQ76MZxU4q/Y8dDG3YXqhqHnTiRZVlRNbhUl
  Rvzcp7Fqqtxqda/Io1lN1tsZpNBYpjCpVJYR2tqbZNvZ5naxSFHQg1lF420u158n66s2gXyUFbNY
  kUDPfRHR0CYa4MwImT5QLC9fKSRTBiPtoUMcE8q8q8L+9VyG/fy3DPu9Xi8c9mGjtgAeKyBaAVDE
  gp6OJHKBgQlNihElALRtgO0b2HFfwBztlyuYB4GuD274g7kaN0XBHCJvDuPwhwTgI3LupbrVzkjv
  JZVZM8/llXarFZQ/L5AOqEKa78EBI+5ppYoJPDOUPS9JqVyUatoNcsUXQTaagpXjZS0x56UZnZWu
  yIqyt25J9WyrsT/sZj9MYxWhMCmHwvnyc76WhmyEQXCo4INSyhUObXJFXLiBhuFI8OKQ5MfvyEnh
  gpoupbVO2PWcsPqUlykrUfy96Kv926FQozL5MEInLWOFzSISZE9mlUh7W3BM4d6IAz7c2kd0EBfM
  tY6PBC6iXXkdXCnuDMHApB/CeeXKIfwhCw/94wDhgRvFqTxikZB1QUJ0HdCccOJSYhN++m9sxD/9
  Lm4BdJQMoOS/tlLcyzCOT8BZ8wSIK2csSIoV9nrbhP+NUao47SibwSlJphG9evvuxZs3rh0AZvbh
  n1CYL/pC5ps3xyb2hVYA/d862HGsuVmk/BOSrUQok6dUaxvS1DFXl/UWOneudgcc+DD81+GQocJe
  I2Ne6K+P2eqvAy+GzLmY+fqZA7B2DPL6UZCyq3gc4c4Obx7AYZ+0+tJDi8lnaR6baRPut5EBq+TG
  HF6VrGl3EQHodyghSNLxkl5IneAM/5X8J24yGS6cdHsg1m4Vhg1utoKIxX7m3oRuD2UBObg3Affs
  vNrT3XyOnFNicfhbc2CF7KSbHE3sXSaXBl5CbvHiP5UVjZOQFfVbJYxTLst0OHWAiPYxyTQmmQXX
  6WSbiislvlEXSwC/5CDgxzrfOwQeeGl7JscCW0iO1uIbdWlHIUvrvVzOoHhgjDWCImKHk+12dil4
  YugLUdnsjEYoyRNfLUdlk0kY7Lgza9rLJ5nkYaInZygc1KYlIfXnxpQQx8EsY9KMwcnVbI3Sergd
  3Tqs4KIt4SE8gvdPhgnECScZj1ARg99GXeucmpi+8KRho+5w1OklI388KfDoGFCn2C3C4EuJgRQQ
  2xD5KF8Pb0dXPDzh6ncZ1Vyu2sTFVF3JhOgnRVaOG2P2Fc+rPvMsmcS6liO8Wfu033F/DxSbYPrg
  h493ETHmafnlDMxNpwuUSjANcKIo/S6RS/ALnH0w277aZfgqKExcsu14scyWjKLQn+0uIyO9IZRO
  kHQTzm5pm7b4B1Rglu2Wu40e/FCMQIVW4ryAKelZpNw9Ykhj5musU8rPFpPrtPgEhrtFL1KuE0ks
  14ko5Uutf05WS+P00I5ul5k91EmrqQSHdN2v/kBPWYni70Vf7d/2ZdsiUGbweToexpAKF9ugS0rw
  MoK11/k8S/H0i77cH77EaJHpnIBAGiuSaD82Zs1lahzPPU1mltODQ/gxBR7hsnO41qhL/Jj0RQSl
  qzVUloXMJOIbSR2Ph8O4TshdH72uj17vISF3f2hKyC3gXqJhY6JiY1IhIbfh7DLpCtYbI1UOgs+N
  OATxvTCQ4fFxT8zDnAvClgsXCpMvS6IimbkeK5knBUbm5lzZNrNrjRmSPz0v82WDMVzma9SzpYuA
  ZzerJQQcFPwz0ETxRJRgByA2KLeCOILj/6+Wu4t5yvXtBj6J2yARzXRZjMecfQMaS6XZPUQt3R8x
  KISBTArvELYeJKTQJBzvObNKWhx6nCUILy+Mv4TiJ8YFnxer5HmE2OwSFh4iafod36svH67Ppn7B
  s6n+gre7TIwrxHECjkV9ItdJxoxy5VY05YN8KHDUSfztaTTMzWxDm09XuvGsJMY9Z9Yap5Zt/ibz
  nFTUfqqg2LjkFh8vlCyIkVeGgw9Gmc49WUoPSY6P0isHmGhHkryUXH4gFx462clKygCPA4xh7Qs9
  OB1pDOsDGOyBbtXCDgOQx7WkWzmTwU8brtNVEPn1zwhuC45i8Bqul0J4hpr69wBUzQGdc3PqwacP
  4H/jSVg3gMVho5RFz0DHcSa0G0fQp+VdrO7VutA2Jy0/e1O9T6Arrr71A/oEgnLZLXGP7LdfkHtv
  iy76sT+QkITVciR7VWv51/Gt4UJK88cLn0MRzasLQOQIv3Vt9/3KMxyOpujQBDV+tACiVG3Hm5KE
  8XrPELhdH2Xo6GHhstVbd7g+OcUMqpsT97DqDvKG6QmfbMXpAi/vs3UIFYYvUvwgQCFPGN3ndQOo
  f9W6oTXDeZVvpQCyBuREle0ipdH2hGzl/WXF7uV9Sn9JPa2sVDmoyYcN0aWOg3LK6cZlQ7U0by3Q
  U0ML0QELop7Cm79L9c85xqpaP9VEnAD5lIe6+et//oKivzAMxeGeb40Cgbgwl7HtCZlqoFRcQT7V
  NXrL7S+H6R/whC+hEsSdSx7+1YIAQZYjnoSIEbUt4FsWQIrLlJUo/l701f7tUJEM4os7z1ZjjY8t
  jRrhRQgzHdju3dKG657pwT0e2NKVs4wX1BmvWC6ccvFm6CjeOIuz/KyMHq/lRHPdaGyN22VvDxul
  5Bnzi9vaW273g6cjJTVCgssDA22+rYgYt+jdOmzGNzDcP4iuwi0J7T0hs1+coE/IYtilDD4nH/xi
  EHPmr2dGPzvfX+SlIYBaiwm19IVClVy7uaenKQ4ZRukYz4lLJ/0+iEemMy54V5RTLuSdFInW6feP
  LZFo83QBUD4UVEsIvGYh16AxblD+HQkx8G0ograRODmfTW9xQHweoWNl9KGxxffgHhcfWuFHhbzi
  eg8d2uwH8F8sELqOVn4Qslktdh0+WjnpHBuyjImsQGcOMmvoiAldu56sQWEPVOejoXUsJWnWAosW
  uCI3K8L/g6fPwALd1wauAPqrnUmXt+VELiI9N5HdH1/wRmz/+Xs6lCbIVVEx9eh3cWTxHDRbwPxl
  ISQodTi9L8UWd8lljKCxYP8HbaBez2iJawWFJ40kzZr9MKeI5LYvclTtytS5gw0OFSO7uMABkqZb
  JtVkBbHF/kPL5Tf+UYCymObEUHGn2Ge1DuOoZXdclkSZaw3nF/C4hI57HbX/0pkLysKs92zdlS4v
  pZhiha+Cu0vQ592GGwiZ7NsAJ5vdBewigpJp3nwBvJWYgp3BVyjvHb7vDcZCpVJQNnSwXUPOA1XW
  MngWuwm40Ch/Hobxc58Isi8T6T1RP/xE7/ulrOzLxlRBiQwzIj11UUW+jCpWK1e1cvWVKlfBNsNQ
  I5fH7Y6SSYqZAF3NsgLXd7tGMhkNQdJVr8j88fQt1DOvZuv0cgtpM083i5VN7bWgcfaOh8NBX9A4
  nXPgOqe0Zd0b3Ymnb/OpjfTctJer5Xi2GVOhjZ7zld5Jc+mjy0MNKUscU+atljTZR0mSCVT3AWQf
  snFkuuYhTB4tUdk2DoDpGps8/RP7JeZ4GQ36SVx153I7gT2dsFBjrAWziCl+VT3JqpW4ZEzUR/AD
  VLbYRcRQJ+J/LFJEiQruerw3yUdFBGCrWQAaZNdcb14my1BezuMy5xpJpSadqfJwoKdY51n9RbSW
  3slkeTTqOiJ3IfWVYE5ndjrPlWZcA4C4rX2d2ZZf3QD3ctDvHFsM1C53UcsHk8tpJykhGHt2F5GS
  narJRZGPZ+d66neZkGeTRdpmJlLUGrGhe7WqTcoSFFkSE1kSElluBrMFOhaGR3qGHsrdsCUps4E1
  fG4nJc9d2ZPu1lLkZ/1BqCcWxREr0dOnz5rRabMZQsEFrusiqqMyGpVRb6jwiKIJibMLM8vUxF3i
  2UN05bqJuqv8WhfEB0nPj1fnKfQZwzCGn4i8O+c0Nc/22NZjYND7hbTyXCQS4tFkC0D+Ib+xAqXG
  gnzdxNQnu+2yzfeXGaeR9s3tIw3BEZfn4SzLfCnwFE7GKmWhF8LvtfxQBSW1vCG+2lyeteYp8som
  di+qmYtr7jLFWUY9cvivxOwz4+4gp0swuXv4GPxguebCXH5UUp7XYIexbgvTgAkVXA7yeSbp8jpx
  a/EQl9bjyFvUtnwDi4Aqzh2VlykrcSjJy/TBepjEAdQTDuoW9zBwOSvEC0knYUpAPfFBDV4Dg3pS
  lvFOqFCDemk39xPU77OS4eSS5NvheEWOkdmDf+2urtNFmm1R5m9cuaJX2svhHRKUT6PuXP0xdsnO
  UPieSqf1rQP1rQNf4NYBEeu8j8I4m6Pj4x6IE0tCYOSHYIdqBFW3qIQYfdsdCP7DQadTpPwKmg5n
  eQY1SzF15roU8WFS6qcpzDLBN5q9hYU2KdGVQ5FwacUcRcJ9kUFKs0bJEzoAo/A+5HlPqbMXhzmA
  3b9juuvSiB+FyCPjTaeb+DsFsEJgyNqtRXwvJptPzVwhpSgkxwEYbU64EVksLcJRQRPwQVO/U9X5
  8jof3fMyC/vYZw8YbuhunQ7kGAelZkrciU7NFOLnTZz8yWUFwl9TQqORPCEXlYn21DfkGtEjTHTm
  81SymEuvhJuxB91OMuyZ5AaPWA8/o2nJ7bxmz2NJeIvdwu8Qc1JFn5UiSe7mClsL6NHtrwbW/rjj
  j58ujjpnr59HEI1rXE55e7hgrw8kUf4a6lFbGemkVwrSjYxI5xKJ4Bh+9Y0g3ReMyioGZLiiu/nc
  BYYfFovT6Ywne/OnkgTfugK+QXb3/zMoAqXr95P15vfZEU5IgeOXJXmG4KHxk4CP/bg36gzDI4Ps
  yFUYz0nTa+oY53TeSylqPeKVh7To9l6/U4n2I59etnnbF1HxETqVMpWVHTTzTFDGsr/JZ9GGLpE/
  ttF2hdE6XIYTkRoeA+5WGLD+3vR2v8Ra1Sa99LagnFo+5xJIDe8TE97Zb752E5BEje+SN1Du7nFA
  EFc57ulRRmxTaeecd4gvJa7R74hco1+ZawDlqjZuyjEysKCYE2q3knseX88vkLnCxGCKDg4URoia
  iB05rJ2YSFvjzWRxcTWJbk7OmidADL6LhLjW0+/i1g3L30DfRvgWtmYL3JjTN/sFjpYEt9IijnfQ
  CaXLvOdKo45BsVLdoLScPu56CCZ7vTTO6ai5X5sUyJ47X6vk3jBg1lzX0l7Zsok06JGW2695YRfn
  y8/uoFWtT1AlCX9ol3yqnrUUpPOt7X+PV8jUhH1MbyDuXJkCAQ/VNafgfZcIuf32DELu5Mqf7Avk
  kPevF1LLv45vDb/yPqXdy7qWdCvnUqq8jFkFzJ+wZNmRrPE68Vy3NNju/NatPca03AiQa5s2TuXM
  zt0viCmU8qq07CsqVODmtiuZ99sdcDRK7b9f4GLjOkS3fvLpPvoDzpa4Q/XvixP76rUicw9n7+EM
  vhYNWHn34r63XfmqRL5EGtcIvu66Sq97UIzCutX1hyDqFnbVkSdPrN5jZXoW2GtNzw5Sq1Z1/Mvt
  T9UpKlH8vYhLyNpOLs0W0X2qIpHzi4od+LsYWYK/K7nKT7G2Ot8NbE5eWar/fJV2VrM9UT3AWr2j
  AEXNx+56V4paBb0pQFsLUl0qaWcOzu599w00THQEPvEJYbX3l3kdThg3e6a8LoKvIJ0zY7fnxfMP
  SzIPlI+D5XFizB9UMuaHyuXBukBFO0OejmkaOOmqQwj2T+WPu8BSOIxKkwBhVzaLTzuuUhtDbaUG
  yo++Fz9VF7CymrivYewBJMkTaI42jmgPs9rTAqMnXCOX2gjUzffZRtUWqtWvUttPwBGfKpYcZIVs
  T+bz9sUumNpF7R7ymneDp17FFrUPhhPgijMOpNI0BNmsCgZQsa5KE5UIStVF2BO1rmLx1gZUeUr7
  Y0HBdm1lOHuY0h5kJPK0u9XbCJby5Wc/67JHzrwf3rwf7lzz+Kq1a/9FlRq1/8JeoqiA+QI8Y8mH
  FJ5FQ6G7e47P8rDdeMVj+fn7PQOyKgSV+fdW2YoYYCoN8HQHmUfD+HbFYIVKBq9gA6niXRjcsY20
  ikBcLU6PD6GK4lxNnq8Q7sdHUE1pDg7/20//e9GIvK5mLBxLdaVVwqZqIrIbS7M/VTWGWr4+dL1a
  vq5a8mHFB9m+huUR0N/f/UH34Is0Q26e8D6Q/urFm19fGgobxkMMalLZdw1A3+bFRMHadRRIfTpI
  wjfvE/3+B/R9ktXdUR4D08Fux5zJ5vQpWl3bOf86W8EhsxXE/VEHJAM1YcH1dCVmm6K/xCtRjkej
  Xt8x0ZSYIUDJelB6KYqaOqGGm3sBN92h4aY0CWjmFqAZ1UDzzQINTbQl5pY8fbXL8vySM2OWLfWt
  nPDuuG9MlVIYHVuW4sqU2qogpRX7plwQLKfcZbZgwy3C7LNjiifH1E602GS1mt+2sVC1wVnRZ9tb
  cIIsogbLYSQPgi0evphEF31p6aIL+wq/51MpsvvSMiQo/waH4idN8Awiyna7XJQnSCEVbz0q8qrq
  jZtFqop0B0sOAyW6i/2zb3tfp65z+KReH8zEVSBMomg+m9LUjLwgejWeXG1FpoAgTiPA5hb9WU7o
  XYAI6J8DONL2Or1cXmezPyEppY3geUmNmKaFm8At4BGsd5fbJWuCddA0VvXXOCw8z7yIwUoZvgZF
  r2LuxUeTI9I1FpMUlnf0qH7uwfNruviPdy9f/PTzy8P10YHPoNfD//b6A/xvZ5CQf+ETd3qP4k7c
  j+EfUAl71ImTfm/4CHQON6T82UGAXAPwaJt+3hSVg8Wm04LvdC783wfy/Ny+QVj5uQ2lvOV0095+
  gozmFr+CGLwE+DWYZViSHb+ZbbbjUygPbo6y9DN63f1rUmPyA34Q/u+2MyQN/3X1RyEGBD/F+J8M
  O0mf4X93OITf417cT2r8v4tHQetx8vFFC/wdnID3UN44R/9ignD09/R6lh1Bbj5Ps+vtp/FisoIf
  36SLxQRgseDVcj2Zz6M5fDuHzX18cd4CU/jj4wskUP39vAn/puIuaSKCTUTTZoQUxGfsHZQxYKEs
  pIMWmMFfF+l8+TnirTWFbjOxT1gadTuN0Ns5+tU8egl1PW09jo7UV92P723rA8DrxWoJxaPs2tQS
  AFD4SfMpvIeDzuCPbLJF43yXXu7WG3SVHv0KnuGhv34FSz0DHdQXlJB3c+JbfTmH4vWPUMbegDl4
  ++roMfqCWoP/tI4eI7ksmrTQZZXwJfuFB7CGE87aMdc/4MRxO0f0x2wK//o5nWx2ayj4kXHP5j7j
  BoaBB4wad8tGaxnsa22wFETRVDkIqdCjTIEoX+ieXg46aCvnM9oPB1qygbAuhtqMQWt5Xy2wKO7u
  BQ1EWICn8JPceSb1DJvCnRPIXTTZBo0v0k8zCMNuc6Zj+Jt1xmTPUYeoMwR1FIDH6ItLLyDvpmBl
  J6tVml2x+aHp0Z7JGuNuUctj1XijDCBugXmSj4L1DeYxaiWB0PiKvODkIRYpT4LT3tIx0TZ1ihIT
  koLXPm7N+D4kLURBjCSkq5OQng/h6KIFmFxdjdHE8nWG64uJKlpniG+P1+nV7jKNOi1AM/3CIbfA
  5PJyl8MdfAWe4HdNSmpZu2OyC8WLSrvEa8QHRLePlMQ7lo8VLvAT4Wcid1mINKgvAkgGki6PgEOO
  3HkTtMUyDKTMm9TTNimMyvfwDPGSjMmQ1RkCFVA5ljymcwT5ktIVFQD2iQCwjPrQ/uIylJAR8zHE
  SrFl5E8XXimDeP3z6ZvXL3+FgPY4U7+2Mo4HMfobHCkjS8JHpgwD2WMh0ZKWhA6tZGQJ6qMt4DEa
  Iw1Bi+Yc7uiAzosYMmVfmH9RAg3JI+Nh5A1mZHPEyDAnY6Nq8S7RhyZjYoyjMT7GhkmQlNyt4oSi
  aCm3CGAZUJG60bYFVETl9JBd3oIKofV8+06ohYoKY8h0gJ6X9z3HvTFB7OUNLL2JLLjN+Breua3Q
  NV04rXtt62yjyDe76TYeOqB8MfDQCPcXBA1lYJK0aoIrWaKQRiXQLySqkiJN/I2hlLoMxd0pkgcD
  VwHzBdGDCB/0gzBXzrAxggkDbilEWBkzJslPiLRCsTNvlUguBloMicc/shnawp8m2wmye3K6uyPv
  0T/PcVVUEJZ/Nfk9J9LfEx/fLIV4BD/s5ttJut1Md9nvyPzJ24La7ng6+T0yCrKYqRpk2DiXYTPw
  Q94GE0914RmNEo7iCD0/LiHfQPbfZfbxrPWh9U+dw1wwPQupNv8DNdOPZ0i9+XAOX12zVx/Qq3+e
  o2J/iaatazR2Uu6fWPZ+PKe5/uH7M/TxOppGNxCEEPkQBiEP6cVms7z8+FvLMjLO+34+ffvu/etf
  /ktuSRjxb2gkZ9KI80l8MkxicTueoM45TEdT8BdY+S/gEwId/CsiPynIqMPGi3909Fs6n09RgFR6
  BUEJykNbuM7gg30yOCaHjij6DGuPafXnH8/O0Zbe2gt8OKdE4CbCzbRIYbTe+H7Kj2iPz1v4/+dc
  J6LC2QRvGfoOLtifgq6KG4zgHP41jqMJxBX650UTkWdGtvl32DgvgPn4bV4/yesnqD4etDgTKKfc
  8JWXphjlcyNTM9Yd4wsqYQv/j11USWahVgb/Pdlgt7u6kGSF6M7qWwih9E1688tkWwSLpmrfw0F8
  no4hLmMBRBje93j91ukGeci2H/EV3S18pzfcDyR6tgCRP5kjKHraRLUeA/DfL34dv/9w+lKdBJaN
  KTygLmGH6jRRu6jYORHpbviL6GnrKayLsJPMFCEmCuLefMTBA3b4fUpBkwAcLtzC/z8/FzESjQdi
  G/mCBnmVXsLZbqAEO8bR4s/hBKMpAkAchvFM4ioChZxG2RMoITxFfxCO9Jl1EhHIBmipYPnlVoGl
  pwR6ltMpnGe6hvz285TjChkZ7PdNTrnwO44TlEmv5Bro8yqiN5bIuhtSEKMVZuC07p/5G9h39Gfr
  tomB5M/lOoPLsFxu0nEGlUw8MjyESB4trkp25BkFIlKNzh33yYeN+rht3ZBp+/WhvqP7UdCZXCG6
  peK8YQhwt0kZI+NTe6ZccDalXBD/2iJWSAejlMffU8QfzTPWB8HtUCnjnS9f/PqPdy+JcQWVl0Ud
  FapySQ6FFNGtxoZBCerRNC1QT1kKRjjEpvOgHci37Kj3TMK9s9YZxrlT8S1mgjf0zRmaD3fRypPK
  PbfR02dc3oJVYS83qJ50YQ++3Rnd08PRVYB5zPBPEQSwVm55K2IIsW8reCy3uBV8xTS+YToSq5vH
  yIRLtXFDaVtvYyjw/Xun2QpuIMdlreEuZM80Xkl8k5E8XvXVrajc3gDaLYqcNk3SvIS2SRpKGzcG
  9lZxksp41VfiJKmIIcx0jK4RlwBSaY7jGF84RoRO7PNENdkOokBpUT9S9oTporxbuXkjrPDm6V3d
  z+SNUrcihyh2bWx5HQFzUCfiLJRu0QLxwdOLSZEIKY5RWmW9Ol8SdjmvUJ/fdCs2oc1DakUfBG9E
  nIaxET4Tw1C0QEkMgmwJDSAK6zIoFXHklHHys3OBR3OVRQYQDqc0GoWN3jwY0b7s1psM7qZpahBs
  6To3qhSvQuDQ8Ni+BzzoFLDr0De60nhGlCsen0rAQgf3m5aCJJxAIa0RvYFSBDGXsVMwyIkmIg4u
  yGjZdEW7kpgLnrXagAITfBxSOTMrO2AvjFQw4wQRBrC2nG3Zgptkg++R2W87y3bL3UbYGbPZmIkY
  eJcs0sRT/j4PAaSaaZGgYYAEgC2s6FU22RIAZyO1AoYAmS3AANJIvunC8dezxeQ6hVtzCqn0lIEt
  6nGMwFHr0IKpsFMOmgxpNFbAugKnUM29lRAsMvANoO2zYN4CHOJvpQFLiK8jFD2JpkxO9nLpy416
  mG3TNSS/RF6lW9UivAHNW3azvvzxH+9+ff0/L8GZKpVjgRzXyuXvacQbb+FPos83NTl5SXkEsbbx
  NPO9kXU1vkOCLZUOG8kZ+UgAG0pT6hFHII4hPqrij9i1tvps+SGaMnaKXuG/ya6olEDeE9OwMMrd
  yAgyZs2Ujk4VzjDFZ45d48iPNOAQgIraUfSpwRkLeIjRQNg8Op2mYcqEbBK6CW5EGCRboPuQTLDo
  uROOq2748CTWhlg0wNYidIjU+fUMLMJHu+DGyZxLIKZx+rZIj/RnCpjyv3jHKT+y58zW6eU2ZVTO
  YsgRGP0pUxJEHY9OWTCX0LJ/krKYXv5JDIz4T7HrMZMVZUVCHpkoT6LKL/7x/u343cvf3r1+//KJ
  3hRGw9VyzPhKEYfCCtJjbSEYrS+XL2FHSicmVQsd1BVG9J9siPnpHCCaGiPUahP8urtAls/xcmqQ
  C3HvAqfHVajiRIAUTTMSpgbfETtRjv+n2HtkMBMpM5YlSV0vOXosYQcbgbhxeU1C4NA48jrYuGmq
  hm1tk80l4j3MAkNYIWI2cDVm2WROWE4TUEw6fUsQqEjo0hFJFtMgA8Mo6ChnkdU3y9IcQHNqW84S
  mNzG4ccgQAhESSCb1K9NsFKG7HwASLHIKb7CuBBkaswrhBsVcBG+2QYWREG1ybdToIvfg812N50S
  nyuYbcBukxIC346Ojui5g6qUUz/XxxBus4DblaIhYhCGMpWKOCcyoVB0YUmldm5E1srpurCTf0dH
  0llGt7nzY4Muk/6eg7VwbhFiwdNn50zBw54j3JS5GRJ1KVXHmi2czGP4UCaTJ0zA8EnI1c+Ty/VS
  Yky5UcZ8Pl5BLlvPFttYPhs46KakwaqGBMcODFq/oROoAYetIGZh+NHWj60YhzihX9rt/IDdcmzR
  posAWAJbZEIXTg4h754djvEZMfIVdkVoLTo49fED9WC1uBMZFUXTFA8tMe+3YtCQdcYdJFZYCZXt
  Gs/ANfrnyEZJUH+YmGjHcRnQKOAmDgxviKSi0+a+x4YsKqKhyet61PdUt6MiC0InuiSokgipp03i
  lMOzucWNw8GWG8mUkaItFE8gf+mg9Pqpn/qpn/qpn/qpn/qpn/qpn/qpn/qpn/qpn/qpn/qpn/qp
  n/qpn/qpn/qpn/qpn/qpn/qpn/opff4Pov/ttAAwAgA=
  --fC8awkkfQC--

How-To-Repeat: 

Fix: 
Fixed theory-formula-alist to use *pvs-files* instead of *pvs-modules*

(defun theory-formula-alist (file)
  (let* ((theories (cdr (gethash file *pvs-files*)))
	 (ce (unless theories (context-entry-of file))))
    (cond (theories
	   (mapcar #'(lambda (th)
		       (cons (id th)
			     (mapcar #'id
			       (remove-if-not #'(lambda (d)
						  (provable-formula? d))
				 (all-decls th)))))
	     theories))
	  (ce
	   (mapcar #'(lambda (te)
		       (cons (te-id te)
			     (mapcar #'fe-id (te-formula-info te))))
	     (ce-theories ce))))))
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools