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

PVS Bug 573


Synopsis:        Rewrite rule TCC simplified to wrong value
Severity:        serious
Priority:        medium
Responsible:     shankar
State:           open
Class:           sw-bug
Arrival-Date:    Thu Jun 21 15:35:00 2001
Originator:      "Ben L. Di Vito"
Organization:    larc.nasa.gov
Release:         PVS 2.3
Environment: 
 System:          
 Architecture: 

Description: 
  We sometimes find that prelude rewrite rules don't fire when it looks
  like they should.  I was able to isolate a very simple example that
  shows one instance.  Under the assumption that 0 < a, the prover
  simplified a*a /= 0 to false.  It happened after an (assert) as a
  setup step, but gave correct results when (prop) was used instead.
  
  Ben Di Vito
  
  -----------------------
  
  
  rewrite_bug: THEORY
  BEGIN
  
  a:     VAR real
  
  test1: LEMMA 0 < a IMPLIES a > 1    %% not a theorem
  
  END rewrite_bug
  
  
  --------------------
  
  test1 :  
  
    |-------
  {1}   FORALL (a: real): 0 < a IMPLIES a > 1
  
  Rule? (skosimp*)
  Repeatedly Skolemizing and flattening,
  this simplifies to: 
  test1 :  
  
  {-1}  0 < a!1
    |-------
  {1}   a!1 > 1
  
  Rule? (case "2 * a!1 * a!1 /= 0")
  Case splitting on 
     2 * a!1 * a!1 /= 0, 
  this yields  2 subgoals: 
  test1.1 :  
  
  {-1}  2 * a!1 * a!1 /= 0
  [-2]  0 < a!1
    |-------
  [1]   a!1 > 1
  
  Rule? (postpone)
  Postponing test1.1.
  
  test1.2 :  
  
  [-1]  0 < a!1
    |-------
  {1}   2 * a!1 * a!1 /= 0
  [2]   a!1 > 1
  
  Rule? (assert)
  Simplifying, rewriting, and recording with decision procedures,
  this simplifies to: 
  test1.2 :  
  
  {-1}  2 * (a!1 * a!1) = 0
  [-2]  0 < a!1
    |-------
  [1]   a!1 > 1
  
  Rule? (rewrite "nonzero_times3")
  Found matching substitution:
  n0y: nonzero_real gets a!1 * a!1,
  n0x gets 2,
  *WARNING*: TCC a!1 * a!1 /= 0 
             simplifies to FALSE
  
  No change on: (REWRITE "nonzero_times3")
  test1.2 :  
  
  {-1}  2 * (a!1 * a!1) = 0
  [-2]  0 < a!1
    |-------
  [1]   a!1 > 1
  
  Rule? (rewrite$ "zero_times3")
  Found matching substitution:
  y: real gets a!1 * a!1,
  x gets 2,
  Applying zero_times3 where 
    y gets a!1 * a!1,
    x gets 2,
  this simplifies to: 
  test1.2 :  
  
  {-1}  2 * (a!1 * a!1) = 0 IFF 2 = 0 OR a!1 * a!1 = 0
  [-2]  2 * (a!1 * a!1) = 0
  [-3]  0 < a!1
    |-------
  [1]   a!1 > 1
  
  Rewriting directly with -1,
  this simplifies to: 
  test1.2 :  
  
  [-1]  0 < a!1
    |-------
  [1]   a!1 > 1
  
  Postponing test1.2.
  
  test1.2 :  
  
  [-1]  0 < a!1
    |-------
  [1]   a!1 > 1
  
  Rule? (undo 3)
  This will undo the proof to: 
  test1.2 :  
  
  [-1]  0 < a!1
    |-------
  {1}   2 * a!1 * a!1 /= 0
  [2]   a!1 > 1
  Sure?(Y or N): y
  test1.2 :  
  
  [-1]  0 < a!1
    |-------
  {1}   2 * a!1 * a!1 /= 0
  [2]   a!1 > 1
  
  Rule? (prop)
  Applying propositional simplification,
  this simplifies to: 
  test1.2 :  
  
  {-1}  2 * a!1 * a!1 = 0
  [-2]  0 < a!1
    |-------
  [1]   a!1 > 1
  
  Rule? (rewrite "zero_times3")
  Found matching substitution:
  y: real gets a!1,
  x gets 2 * a!1,
  Rewriting using zero_times3, matching in *,
  this simplifies to: 
  test1.2 :  
  
  {-1}  2 * a!1 = 0 OR a!1 = 0
  [-2]  0 < a!1
    |-------
  [1]   a!1 > 1
  

How-To-Repeat: 

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