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

PVS Bug 713


Synopsis:        Resolver bug
Severity:        serious
Priority:        medium
Responsible:     owre
State:           analyzed
Class:           sw-bug
Arrival-Date:    Wed Aug 28 16:05:01 2002
Originator:      Daniel Kroening
Organization:    cs.cmu.edu
Release:         PVS 2.4
Environment: 
 System:          
 Architecture: 

Description: 
  Hello,
  
  the resolver does not complain about ambiguities that arise from theory
  instantiation. It rather picks the theory that has been imported last. Is
  this a bug or desired behavior?
  
  In the attached example, it will complain about the ambiguity in lemma2 but
  not in lemma1. Depending on the importing order, lemma1 is either true or
  false.
  
  Daniel
  
  ---------------
  main: THEORY
  BEGIN
  
    T1, T2: TYPE;
  
  END main
  
  t1[(IMPORTING main) x: T1]: THEORY
  BEGIN
  
    arg: T1;
  
  END t1
  
  t2[(IMPORTING main) x: T2]: THEORY
  BEGIN
  
    arg: T2;
  
  END t2
  
  testx: THEORY
  BEGIN
    IMPORTING t1, t2;
  
    vt: T1;
    vt: T2;
  
    ft(x: T1):bool=FALSE;
    ft(x: T2):bool=TRUE;
  
    lemma1: LEMMA
      ft(arg[vt]);
  
    lemma2: LEMMA
      ft(vt);
  
  END testx
  

How-To-Repeat: 

Fix: 
Fixed get-decl-resolutions to not set the type of the actuals too soon.
Home Intro Announce FAQ Docs Download Mail Status Bugs Users Related FM Tools