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

PVS Bug 707


Synopsis:        Could not determine the full theory instance (sometimes)
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Aug 14 10:40:01 2002
Originator:      Hendrik Tews
Organization:    tcs.inf.tu-dresden.de
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  
  Hi,
  
  in our project it sometimes happens that a smash or a grind fails
  with 
  
     Could not determine the full theory instance for OK?
  
  But often the problem disappears later (and reappears somewhere
  else).
  
  With the appended tar file you can reproduce the problem:
  - untar
  - start pvs in directory hw
  - "yes", create a new context
  - M-x load-file typecheck.el, to type check everything
  - visit file everything.pvs
  - invoke prove-importchain on theory Everything
  - the status report will show 
  
   Proof summary for theory paging
             ....
      GoPaging_TCC2...............................unfinished          [O](0.08 
 s)
      Theory totals: 13 formulas, 13 attempted, 12 succeeded (22.23 s)
  
  and when you run the proof for GoPaging_TCC2 you get:
  
      Rerunning step: (SMASH)
      Could not determine the full theory instance for OK?
        Theory instance: Result_adt[[BasicTypes.address -> BasicTypes.byte],
  				  BasicTypes.word]
  
  - retypecheck now paging.pvs (with C-u M-x tcp)
  - now the proof for GoPaging_TCC2 works
  
  It would be nice to get a patch or a workaround for this bug
  soon, because it is really annoying that the same proof sometimes
  works and sometimes fails.
  
  Bye,
  
  Hendrik
  
---Spec removed----  

How-To-Repeat: 

Fix: 
Seems to have been fixed in the course of fixing another bug
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools