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

PVS Bug 786


Synopsis:        rewrite "div_cancel4" kills premise after (ASSERT) only
Severity:        serious
Priority:        medium
Responsible:     shankar
State:           open
Class:           sw-bug
Arrival-Date:    Mon Jun 23 12:30:01 2003
Originator:      Rick Butler
Organization:    larc.nasa.gov
Release:         PVS 3.1
Environment: 
 System:          
 Architecture: 

Description: 
  
  --------------Boundary-00=_AG6YFQFMKHLOH3TTY8CD
  Content-Type: text/plain;
    charset="iso-8859-1"
  Content-Transfer-Encoding: 8bit
  
  Dear PVS
      The following bug is causing havoc with Ben Di Vito's
  (CROSS-MULT) strategy in PVS 3.1.  (CROSSMULT) rewrites with
  "div_cancel4" which has the following result on lemma bug3:
  
  
      {-1}  Pred_T(s!1)
      [-2]  Pred_H(s!1)
      [-3]  vr!1`z = (sign(sr!1`z) * H - sr!1`z) / (te!1 - tr!1)
      [-4]  tr!1 > 0
        |-------
      [1]   Pred_S(s!1)
      
      Rule? (rewrite "div_cancel4")
      Found matching substitution:
      n0z: nonzero_real gets (te!1 - tr!1),
      y: real gets (sign(sr!1`z) * H - sr!1`z),
      x gets vr!1`z,
      Rewriting using div_cancel4, matching in *,
      this yields  2 subgoals: 
      bug3.1 :  
      
      [-1]  Pred_T(s!1)
      [-2]  Pred_H(s!1)
      [-3]  tr!1 > 0
        |-------
      [1]   Pred_S(s!1)
  
  Notice that the [-3] formula disappears.  AGH!
  
  Here is the proof
  
   (skosimp*)
   (assert)
   (rewrite "div_cancel4")
  
  Interestingly if you eliminate the (assert) command:
  
   (skosimp*)
   (rewrite "div_cancel4")
  
  you get
  
  
     {-1}  Pred_H(s!1)
     {-2}  vr!1`z = (sign(sr!1`z) * H - sr!1`z) / (te!1 - tr!1)
     {-3}  tr!1 > 0
       |-------
     {1}   Pred_S(s!1)
     
     Rule? (rewrite "div_cancel4")
     Found matching substitution:
     n0z: nonzero_real gets (te!1 - tr!1),
     y: real gets (sign(sr!1`z) * H - sr!1`z),
     x gets vr!1`z,
     Rewriting using div_cancel4, matching in *,
     this yields  2 subgoals: 
     bug3.1 :  
     
     [-1]  Pred_H(s!1)
     {-2}  vr!1`z * te!1 - vr!1`z * tr!1 = (sign(sr!1`z) * H - sr!1`z)
     [-3]  tr!1 > 0
       |-------
     [1]   Pred_S(s!1)
  
  the desired result.  Under PVS2.4 one does not have this problem.
  
  Rick
  --------------Boundary-00=_AG6YFQFMKHLOH3TTY8CD
  Content-Type: text/x-c;
    charset="iso-8859-1";
    name="bug2.dmp"
  Content-Transfer-Encoding: base64
  Content-Disposition: attachment; filename="bug2.dmp"
  
  CiUlIFBWUyBWZXJzaW9uIDMuMQolJSA2LjIgW0xpbnV4ICh4ODYpXSAoRmViIDE0LCAyMDAzIDE4
  OjQ2KQoKJCQkYnVnMi5wdnMKYnVnMjogVEhFT1JZCkJFR0lOCiAKICB4LHkseix0ZSx0cixzLEgg
  IDogVkFSIHJlYWwgCgogIFByZWRfSChzKTogYm9vbAogIFByZWRfUyhzKTogYm9vbAogIFByZWRf
  VChzKTogYm9vbAoKICBidWc0OiBUSEVPUkVNICBQcmVkX0gocykgQU5ECiAgICAgICAgICAgICAg
  ICAgIHRlIC89IHRyIEFORAoJCSAgeCA9ICh6ICogSCAtIHkpIC8gKHRlIC0gdHIpIEFORAoJCSAg
  dHIgPiAwIAogICAgICAgICAgICAgICBJTVBMSUVTCgkgICAgICAgICAgUHJlZF9TKHMpCgoKRU5E
  IGJ1ZzIKCiQkJGJ1ZzIucHJmCihidWcyCiAoYnVnNF9UQ0MxIDAKICAoYnVnNF9UQ0MxLTEgbmls
  IDMyNjQzNDAzMTkgMzI2NDM0MDMzOAogICAoIiIgKHNrb3NpbXAqKSAoKCIiIChhc3NlcnQpIG5p
  bCBuaWwpKSBuaWwpIHByb3ZlZCBuaWwgMTc4MyA2MDAgdCBzaG9zdGFrKSkKIChidWc0IDAKICAo
  YnVnNC0xIG5pbCAzMjY0MzQwMjk4IDMyNjQzNDAzMTkKICAgKCIiIChza29zaW1wKikKICAgICgo
  IiIgKGFzc2VydCkgKCgiIiAocmV3cml0ZSAiZGl2X2NhbmNlbDQiKSAoKCIiIChwb3N0cG9uZSkg
  bmlsIG5pbCkpIG5pbCkpCiAgICAgIG5pbCkpCiAgICBuaWwpCiAgIHVuZmluaXNoZWQgbmlsIDIx
  MiAxODAgdCBzaG9zdGFrKSkpCgo=
  
  --------------Boundary-00=_AG6YFQFMKHLOH3TTY8CD--

How-To-Repeat: 

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