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

PVS Bugs List

This list summarizes the bug reports that have been received since PVS version 2.1 was released. Most of these were originally sent to pvs-bugs@csl.sri.com. Click on the bug number to get the full report.

The bugs not marked as open have been fixed at SRI. A release candidate is available that contains all but the most recent fixes. Please let us know at pvs-bugs@csl.sri.com to report a new bug, or to request that a previously reported bug be given priority.

based on the information below:

Search (regexp)    Submitted by (regexp)

 open: The problem has been filed and the responsible person notified
 analyzed: The problem has been resolved internally at SRI
 feedback: The problem has been resolved, and any changes are in the latest release
 closed: The problem has been resolved, and any changes are in an earlier release
 suspended: Work on the problem has been postponed, usually because it can't be recreated

Submitted since in chronological order.

Note: this makes use of the GNATS bug tracking system available at ftp://prep.ai.mit.edu/pub/gnu/. The report numbers have gaps because of tests and the way the GNATs system works.

No. Status Date Submitted by Synopsis
PVS 2.1 Released April 24, 1997
Patches Released September 9, 1997
Patches Released October 17, 1997
Patches Released February 7, 1998
PVS 2.2 Released September 17, 1998
PVS 2.3 Released September 5, 1999
361analyzed1999-09-13Natarajan Shankarmusimp problem
369open1999-10-28mokkedemmodel-check
388analyzed1999-11-24Marcelo Glusmanbug after add-declaration
390analyzed1999-11-24srivasBug in the COMMENT command?
392analyzed1999-11-11Chris GeorgeCoercion changes meaning
394open1999-12-08Oleg Sheynermodel checker error
404analyzed1999-08-03Ralph D. JeffordsBUGS in PVS 2.3 beta
Patches Released December 28, 1999
412analyzed2000-01-04Bruno DutertreSlow proofs and typechecking problem
413analyzed2000-01-05Marcelo GlusmanWhere is tarmail?
414analyzed2000-01-05Marcelo Glusmanadding declarations
423analyzed2000-01-17Tamarah AronsFile no longer typechecking after loading patch
430analyzed2000-02-07Ben L. Di VitoRecognizer "equality?" for strategies has changed
434analyzed2000-02-11Pieter Audenaertbug report
443analyzed2000-02-25Mamoun FILALI-AMINETCC generation
444analyzed2000-02-27Jason WuPVS2.2 vs PVS2.3 (problem report)
446open2000-03-12rusuproblem with the abstract-and-mc command
448analyzed2000-03-12Kellom{ki PerttiTypechecking problem
453analyzed2000-03-21Bruno DutertreNonemptiness TCCs
454open2000-03-24Aaron Ballardproblems with decision proc.
456analyzed2000-04-06Paul Y Gloessloop in type checker (PVS 2.3 with or without patches)
458open2000-04-21Ralph D. JeffordsBug in (ABSTRACT)
459analyzed2000-04-25Steven Shapiro dependent types in datatype declaration
461analyzed2000-05-02Myla ArcherGRIND inconsistency + nontermination
464analyzed2000-06-15Natarajan ShankarProblem with reduce_nat
465analyzed2000-06-20Ralph D. JeffordsBugs in recognizer types vs. ADT's
466analyzed2000-06-27Jonathan FordIncorrect proof-incomplete status
467analyzed2000-06-27Sam OwreParse error while showing TCCs
469analyzed2000-07-07Sylvan S. PinskyData-Subtypes
470analyzed2000-07-10Jean-Christophe Filliatrebug in pvs-lisp-theory
471analyzed2000-07-10Sam OwreBug in prettyprinter
474analyzed2000-07-17Christoph BergITHEORY assertion
478analyzed2000-08-21ian a. masonType checker problem
481open2000-09-06Bruno Dutertre(ASSERT :linear? T)
490analyzed2000-09-28Holger PFEIFERTYPE+ FROM leads to unprovable TCC
491analyzed2000-09-28Holger PFEIFERInvalid type cast breaks
493analyzed2000-11-02Paul Y Gloessrewrite/importing bug (PVS 2.3 with patches)
494analyzed2000-11-02Paul Y GloessPVS 2.3 tc crash upon switching two definitions
495analyzed2000-11-09Paul Y GloessPossible bug with PVS 2.3 patches
500open2000-12-05Martin HofmannCan prove FALSE with abstract-and-mc
501analyzed2000-12-22Joachim van den Bergfailure in resolving constructor names
503open2001-01-02Hendrik Tewscheckpoints confuse proof display
504analyzed2001-01-08Hendrik Tewsnew-decision-procedures as default
506analyzed2001-01-08Hendrik Tewsreset-pvs confuses PVS
507analyzed2001-01-08Joachim van den Bergprover breaks with tuples and (replace)
508analyzed2001-01-08Hendrik Tewspretty printer captures constants
510analyzed2001-01-08Hendrik TewsImporting nonexisting theories
512analyzed2001-01-12Hendrik Tewsshow-expanded-sequent does not show instanciations of inline operators
514analyzed2001-01-15Hendrik Tewserror in process filter: Window height 1 too small (after splitting)
516open2001-01-15Hendrik Tews4 more problems
517analyzed2001-01-15Hendrik TewsParameter instanciation error
519analyzed2001-02-01Eric Marsdenfont-lock in Emacs: pvs-mode should call 'kill-all-local-variables'
528analyzed2001-03-04Andre RenaudBoolean predicate to function
529analyzed2001-03-07Christoph BergPVS wishes
530open2001-03-07Christian JacobiModelchecker
531analyzed2001-03-07Mark A. HillebrandStrange COND-ENDCOND Paarse Errors
539open2001-03-20Hendrik Tewsold/new decision procedures confuse pvs
540analyzed2001-03-20Hendrik Tews(hide -) does not work
541analyzed2001-03-20Steve JohnsonStrange trap to ILISP
551analyzed2001-04-02Christoph BergUnprovable TCC for theory actual
561analyzed2001-05-02Sam Owreprove-untried-pvs-file does not automatically typecheck
562analyzed2001-05-09Hendrik TewsNo methods applicable for generic function
563analyzed2001-05-15Hendrik Tewserror message missing with inst for nested forall
564analyzed2001-05-15Joachim van den Berg(typepred "<") breaks prover
565analyzed2001-05-16Hendrik TewsM-x siblings shifts *pvs* buffer
566analyzed2001-05-16Hendrik Tewsdetuple-boundvars
567analyzed2001-05-16Hendrik Tewsproof does not rerun
569analyzed2001-05-21Paul LoewensteinSyntax incompatibility
572open2001-06-20Tamarah AronsProblem using comments in strategies
573open2001-06-21Ben L. Di VitoRewrite rule TCC simplified to wrong value
583open2001-07-23Oliver Moellerabstract/modelcheck bug
589analyzed2001-07-31Ben L. Di Vitoload-prelude-library theory invisible without importings
597analyzed2001-08-07Jerry James[2.3] Prelude bug fix
617analyzed2001-11-03Ajay Chanderlists and members
PVS 2.4 Released November 25, 2001
618analyzed2001-11-26Bruno DutertrePVS2.4 bugs
619analyzed2001-11-27Jerry JamesImport with name change => no proof file
620analyzed2001-11-27John Rushbydistilled problem
621analyzed2001-11-27Bruno DutertrePVS2.4 typecheck or parse error
622analyzed2001-11-28Jerry JamesC-n error with no region selected
623analyzed2001-11-28John Rushbyground flawed
624analyzed2001-12-03Jerry JamesFalse type predicate
625analyzed2001-12-01Marcelo GlusmanBug resolving use of overloaded function
627analyzed2001-11-27John Rushbyrelease notes
629analyzed2001-12-07Marcelo Glusmanhow to repeat the PROGRAM ERROR
631analyzed2001-12-11Ralph D. JeffordsBUG: (apply-extensionality) on function overrides
632analyzed2001-12-11Jaco van de Polerrors with records
633analyzed2001-11-30John Rushbydump file
634analyzed2001-12-12Hendrik TewsDeclarations in assumptions rejected
636analyzed2001-12-12Hendrik Tewstypecheck problem
PVS 2.4 patchlevel 1 Released December 18, 2001
641analyzed2002-01-02Jerry JamesTAB e failure
643analyzed2002-01-04Jerry JamesTrivial documentation bug
645analyzed2002-01-04Jerry Jamesmouse-show-declaration for XEmacs
652open2002-01-23Mark LawfordMODEL-CHECK soundness bug with multiple subrange( , ) fields
654open2002-01-16Jerry JamesContext corruption?
656open2002-02-04Christian JacobiPVS 2.3/2.4 problems with (assert)
657analyzed2002-02-04Cesar MunozLoop in ASSERT
663analyzed2002-03-29Chris GeorgeTCC generation bugs
670open2002-05-21Ralph D. JeffordsProblem with (ABSTRACT)
675analyzed2002-06-12Hendrik Tewstypo in System Guide
676open2002-06-13Tamarah AronsEnahancement request: Selective unlabeling feature
679open2002-07-09Christoph BergComponents not available in record definitions
PVS 3.0 Beta Released July 20, 2002
683analyzed2002-07-22John Rushbyuse strategy
687analyzed2002-07-22Judy CrowPVS shell script ignores flags in raw mode
693analyzed2002-07-30Bruno DutertreError when saving proofs
695open2002-07-30Sam Owreassert problem with floor
696open2002-07-31Bruno Dutertreprover loops
705open2002-08-09Sanjai Rayadurgamlift[T].down(bottom)
706analyzed2002-08-14Hendrik TewsAttempt to store declaration in illegal theory
707analyzed2002-08-14Hendrik TewsCould not determine the full theory instance (sometimes)
709analyzed2002-08-15Bruno DutertreMinor bugs in PVS3
711analyzed2002-08-22Bruno DutertreMultiple proofs and proof display in PVS3
712analyzed2002-08-26Bruno DutertreType of function updates
713analyzed2002-08-28Daniel KroeningResolver bug
714analyzed2002-09-09Hendrik TewsError: No methods applicable for generic function
715open2002-09-23Judy Crowparse/typecheck errors encountered via show-tccs
717analyzed2002-11-08Jaco van de Polaxiom translation and theory instantiation
718analyzed2002-11-08Jan Schaumanndetecting XEmacs 21
719open2002-12-04Kellomaki PerttiMore ground evaluator problems
PVS 3.0 Released December 19, 2002
723open2002-12-23John Donerinstalling 3.0
728analyzed2003-01-10Hendrik Tewsrewrite fails with "No next method for method"
729open2003-01-15Hendrik Tewsemacs is busy-waiting for allegro lisp
733open2003-01-29Jerry JamesIllegal instruction when dumping
736open2003-02-03Hendrik Tewsstrange error message II
737analyzed2003-02-03Hendrik Tewsshow-expanded-sequent does not show instanciations of all infix operators
738open2003-02-03Hendrik Tewsedit-proof takes much longer when the prover is active
741open2003-02-11Hendrik Tewsexpand does not terminate
PVS 3.1 Released February 14, 2003
744open2003-02-19Rick Butlerrelative addressing not working right in PVS 3 libraries
745open2003-02-21Paul Jacksonmusimp causing segmentation violation
748analyzed2003-03-14Hendrik Tewsauto_rewrite declarations do not work (II)
749analyzed2003-03-14Hendrik Tewscursor does not point to the location the error (V)
751analyzed2003-03-14Hendrik Tewsresult of show-expanded-sequent does not typecheck
752analyzed2003-03-17Hendrik Tewsunstable proofs
754analyzed2003-03-24Hendrik TewsSymbol's function definition is void: set-prelude-files-and-regions
756analyzed2003-03-27Hendrik Tewsinvisible lemma
764open2003-04-12Alfons GeserASSERT scraps a premise
768open2003-05-02Alfons GeserASSERT unable to infer >= from =
769open2003-05-02Alfons GeserUnexpected restrict of numfield type
772open2003-05-23Rick ButlerAUTO_REWRITE+ statements impact TCCS via conversion
774open2003-05-28Rick ButlerAUTO_REWRITE+ causes ASSERT to report "Free variables in type Seq[T](G)"
781analyzed2003-06-18Kai Engelhardtminute highlighting omission: CODATATYPE
784analyzed2003-06-20Hendrik Tewsrule-induct fails on Coinductive definitions
785open2003-06-20Hendrik Tewsdata type updates are not simplified
786open2003-06-23Rick Butlerrewrite "div_cancel4" kills premise after (ASSERT) only
788open2003-07-02Venkatesh Phadnavispvs-prover-guide.pdf
789open2003-07-22Quan TranIllegal instruction signal
792analyzed2003-07-23Hendrik TewsNo methods applicable for generic function with bin files
794open2003-07-29Hendrik Tewsx-theory-hierarchy does include some library theories
798analyzed2003-08-04Hendrik Tewsshow-expanded-form fails
810open2003-09-26David Naumannannoying behavior
813open2003-10-06Paul S. MinerIncorrect PVS proof status information, perhaps related to incremental typechecking
817open2003-12-04David Naumanntypepred bug?
819analyzed2004-01-07Paul S. Minermin and max name overload conflict
820open2004-01-14David Naumanntypecheck-prove used subtype-tcc for termination TCC
825open2004-03-08Tamarah AronsDatatype typecheck error + feature request
826open2004-03-10Ricky W. Butlerexpand sends PVS 3.1 into an infinite loop
827open2004-03-10Ricky W. Butler(assert) crashes PVS with stack overflow
829open2004-03-16Ricky W. Butlerrewriting after (ASSERT) throws away needed formula
830open2004-03-31Jerry JamesCODATATYPE: some is INDUCTIVE
PVS 3.2 Released November 4, 2004
865analyzed2004-11-12Ricky W. ButlerTAB i prompt fails
866analyzed2004-11-16Hendrik TewsNo methods applicable for generic function (introduced in 3.2)
867analyzed2004-11-17Jerry JamesDeclaration generic function
868analyzed2004-11-19Pertti KellomakiTCC generation bug
869analyzed2004-11-19Pertti KellomakiTCC bug probably not a TCC bug
870analyzed2004-11-23Hendrik TewsError: the assertion (new in 3.2)
871open2004-11-24Hendrik TewsPVS not exited
872analyzed2004-11-24Hendrik Tewsshow-proofs-theory broken
873analyzed2004-11-24Hendrik TewsTCC pretty printing problem
874analyzed2004-11-25Hendrik TewsTypeckeck crash: Error: the assertion (singleton? resolutions) failed.
875open2004-11-26Hendrik Tewsinduct problem
876open2004-11-29Cesar A. MunozTheory interpretations in PVS3.2
877open2004-12-01Ricky W. Butlertrivial consequence of trichotomy crashes PVS3.2 with Stack overflow
878analyzed2004-12-02robert[PVS-Help] nonempty type tcc
885open2004-12-18Alfons Gesersome AUTO_REWRITE+ rules are not applied
887analyzed2005-01-06Hendrik TewsError: the assertion (eq (declaration t1) (declaration t2)) failed.
895open2005-01-27Chris Georgesmail-pvs-files requires a command "chunk"
901analyzed2005-04-07Hanne GottliebsenDirectory name with & causes PVS to crash
906open2005-05-17Hendrik Tewsfast user confuses PVS
920analyzed2005-11-03Mooij, A.J.invisible variables in PVS
922open2005-11-15Stan RosenbergTCC bug
924open2005-11-21Hesselink20 <= 14? and 20 <= 17?
928analyzed2005-12-06Thomas WitkowskiPVS Bug, Parser not changed for Bug 780
933open2006-01-24Hendrik Tewsauto rewrite ignored
934open2006-01-24Hendrik Tewsfeature wish: mark lhs, rhs and condition in auto rewrite list
939open2006-01-24Jerry JamesCannot edit proofs with 3.3 release candidate
942open2006-01-24Hendrik TewsPVS release candidate
943open2006-01-24Hendrik Tewssuggestion list
944open2006-01-24Thomas WitkowskiPVS Release Candidate
945analyzed2006-01-24Ricky W. ButlerPVS 3.3 release candidate testing
949open2006-01-31Jerry Jamesshow-expanded-form + no region
950open2006-02-06Jerry JamesPrettyprinter removes subtype names from datatypes
955open2006-05-01Hesselinkunprovable TCC generated?!
958open2006-06-10Daniel EleniusPVS bug report
963open2006-09-26Ralph D. JeffordsMinor bug in (induct "i") using nat_induction
PVS 4.0 Released December 8, 2006
975open2007-01-10Hendrik Tewsproblem with use (might caused by varying variable order in TCCs)
999open2007-06-25Hesselinkversion 4 conflicts continued
1003open2007-08-31Alejandro TamaletProblem with "some"
1004open2007-09-26Rob VerhoevenCommands take forever
1005open2007-09-26Hesselinkrecord modification
1006open2007-09-28Hesselinkbound variables clash
PVS 4.1 Released November 1, 2007
1007open2007-11-08Hendrik TewsTCC generation changes the order of conjuncs
1008open2007-11-08Hendrik TewsCursor does not point to the error location (VII)
1009open2007-11-08Rick ButlerPVS 4.1 M-x tc --> Error: No methods applicable for generic function
1010open2007-11-09Marcus VoelpWrong variable binding with Cases in 4.0
1011open2007-11-12Cesar MunozTheory Interpretations (bug?)
1012open2007-11-12Cesar MunozTheory Interpretations (bug?)
1013open2007-11-19Hendrik Tews130 lines of comment cause 2 seconds delay
1014open2007-11-27Hendrik Tewsinstall-proof generates garbage
1015open2007-11-27Hendrik Tewsshow-expanded-form switches between AND and booleans.AND
1016open2007-11-27Hendrik Tewsgarbage output in proof buffer: Free variables in expr l
1017open2007-11-27Hendrik Tewschanging the default proof changes the cursor position
1018open2007-12-06Jeff MaddalonType check and JUDGEMENT problem
1019open2007-12-09David Naumanninstall 4.1 error
1020open2007-12-13Rick ButlerAUTO_REWRITE+ not so reliable
1021open2007-12-20Rick ButlerBreak: set-type-for-application-parameters
1022open2008-01-02Hesselink[Fwd: errTh]
1023open2008-01-15Alejandro TamaletWhen doing a prove-proofchain got "Error: something's wrong with the context"
1024open2008-01-20Alejandro TamaletUnfinished TCCs in _adt file
1025open2008-02-19Tjark Weber"Error: the assertion ... failed"
1026open2008-03-04Eddy SeagerLatex Errors
1027open2008-03-11Hendrik Tewsprettyprint-expanded dies with Found 'MEASURE' when expecting 'THEN'
1028open2008-03-11Hendrik Tewslatex-proof latex error: You can't use `macro parameter character #' in horizontal mode
1029open2008-03-11Hendrik Tewslatex-proof: That makes 100 errors; please try again.
1030open2008-03-11Hendrik Tewslatex-proof: 2 meter superlong lines
1031open2008-03-11Hendrik Tewslatex-proof: parenthesis missing
1033open2008-03-27Rick Butlersimple proof crashes PVS4.1 with "simple-error"
1034open2008-04-19Hendrik Tewsmore latex-proof errors
1035open2008-04-23Viorel Preoteasaerror when replaying a proof which worked in version 4.0
1036open2008-05-11Cesar MunozPVS Bug ?
1037open2008-05-19Hendrik TewsError: Attempt to store declaration in illegal theory
1038open2008-05-19Hendrik Tewsbin files make proof fail
1039open2008-05-19Hendrik TewsTCC in generated _adt theory
1040open2008-05-19Hendrik Tewsmore latex-proof problems II
1041open2008-05-19Hendrik TewsPVS dies with signal 11 (SIGSEGV)
1042open2008-08-05David Lester
1043open2008-10-23Kai Engelhardtmissing TCC for COND
1044open2008-11-05Verhoeven, R.H.A.PVS4.2, Error: the assertion (singleton? resolutions) failed.
1045open2009-02-04Natarajan Shankar[PVS Bug] Formal parameter conversion
1046open2009-06-05David LesterTypecheck Soundness Bug in 4.2
1047open2009-06-10=?ISO-8859-1?Q?Andr=E9ia_Avelar?=[PVS-Help] pvs 4.2 error: no methods applicable for generic function
1048open2009-08-01119aniu@sina.comquestion
1049open2009-08-12Rick ButlerAuto-rewriting of a simple definition leads to infinite loop
1050open2010-04-13Hendrik Tewsmisleading error message
1051open2010-04-14Hendrik TewsCursor does not point to the error location (VIII)
1052open2010-04-16Hendrik Tewsboolean tuples not simplified and strange simplification
1053open2010-04-16Hendrik Tewstuple not simplified
1054open2010-04-23Johannes ErikssonTranslation of unary minus to Yices
1055open2010-06-10Hesselinkerror in treatment of pairs
1056open2010-06-10Hendrik Tewsunused-by-proofs-of-formula gives No methods applicable for generic function
1057open2010-06-10Hendrik Tewsshow-expanded-form does not expand measure
1058open2010-07-21Hendrik Tewstrivial sequent not recognized as true
1059open2010-07-21Hendrik Tewsno methods applicable
1060open2010-07-21Hendrik TewsPVS doesn't recognize trivial truth
1061open2010-07-21Hendrik Tewsauto-rewrite does not work
1062open2010-07-21Hendrik Tewserror "does not uniquely resolve" with only one candidate
1063open2010-07-21Hendrik Tewsgoal sequent missing after smash
1064open2010-07-21Mu Suntype check conditions bug?
1065open2010-07-28NARKAWICZ, ANTHONY JOSEPH. (LARC-D320)Typechecker Bug
1066open2010-09-10Munoz, Cesar Augusto (LARC-D320)Soundness bug in PVS
1067open2010-09-28Butler, Ricky W. (LARC-D320)FW: Typechecker Bug
1068open2010-09-29Munoz, Cesar Augusto (LARC-D320)Typechecker Bug
1069open2010-10-02Erik Martin-Dorelfind-file completion misbehavior with PVS 4.2 + Emacs 23
1070open2010-10-02Erik Martin-DorelPretty-printer bug
1071open2010-12-27Denis Yefremov(rewrite "offset_min_shift" N)
1072open2011-05-20Victor LuchangcoSoundness bug (missing typechecking condition)
1073open2011-06-11Andrea Domenicilatex-proof does not print partial proofs
1074open2011-06-13Jean-Claude Royer"no method applicable to generic function"
1075open2011-06-19pvs-help-owner@csl.sri.comPVS-Help post from qgxu@mail.shu.edu.cn requires approval
1076open2011-09-20Jean-Claude RoyerGeneric datatype, bag, wrong argument to map
1077open2011-09-28Jean-Claude RoyerBug with induction, library and generic data types
1078open2011-10-13Victor LuchangcoProblems with X display of proof trees
1079open2011-10-18Jean-Claude Royer[PVS-Help] PVS 5 The assertion lib failed
1080open2011-10-24Peter G. Neumann["Michael Roe" : Array overrides in PVS]
1081open2011-10-26=?iso-8859-1?Q?Thiago_Mendon=E7a_Ferreira_Ramos?=[PVS-Help] An error when pvs generates tcc's
1082open2011-11-05Paul Y GloessProblem with PVS 5.0 Allegro version on Mac OS X Lion new operating system
1083open2011-11-08Victor LuchangcoBug with libraries in PVS 5.0
1084open2011-12-07pvs-devel-owner@csl.sri.comPVS-DEVEL post from anacrismarie@gmail.com requires approval
1085open2011-12-10=?koi8-r?B?7cnIwcnM?=PVS BugReport

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