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

PVS Bug 1031


Synopsis:        latex-proof: parenthesis missing
Severity:        serious
Priority:        medium
Responsible:     owre
State:           open
Class:           sw-bug
Arrival-Date:    Tue Mar 11 13:05:01 -0700 2008
Originator:      Hendrik Tews
Release:         PVS 4.1
Organization:    cs.ru.nl
Environment: 
 System:          
 Architecture: 

Description: 
  Hi,
  
  [For the tar file see the "prettyprint-expanded dies with..." bug
  report.]
  
  Again in the terse output of dt_lift_art_TCC5. The second sequent
  (after Splitting conjunctions, we get 2 subgoals) in the terse
  output is dt_lift_art_TCC5.1. It contains
  
  {1}   pointer?(typ!1) IMPLIES
         (LAMBDA (t: Semantics_Cpp): IF ... ENDIF) (nr(x1!1))
  
  The parenthesis around LAMBDA, which are absolutely essential,
  are missing in the latex output. 
  
  Incidentally there is a \( \) pair in the output at the right
  place, which of course produces latex errors.
  
  Bye,
  
  Hendrik

How-To-Repeat: 

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