Contract Violation using provided Modular ACL2 Demo code

[racket-bug-submit]

Originally submitted by Jason Hemann on: Thu Mar 15 10:40:01 -0400 2012

Walking through Modular ACL2 example from documentation, received the following:

dracula-state-done: contract violation, expected: (and/c dracula-state-active? (not/c dracula-state-error?)), given '#s(dracula-state #f #s(proof-table (mtriple mdouble) #f #hasheq((mtriple . #s(proof-state #s(loc unsaved-editor25110 174 270) 4 #f #hash((0 . #s(term-state #s(loc unsaved-editor25110 174 174) #f #f #f)) (1 . #s(term-state #s(loc unsaved-editor25110 192..., which isn't dracula-state-active?
  contract from: 
    <planet>/cce/dracula.plt/8/22/drscheme/dracula-state.rkt
  blaming: 
    <planet>/cce/dracula.plt/8/22/drscheme/dracula-proof-panel.rkt
  contract: 
    (->
     (and/c
      dracula-state-active?
      (not/c dracula-state-error?))
     (and/c
      dracula-state?
      (not/c dracula-state-active?)))
  at: <planet>/cce/dracula.plt/8/22/drscheme/dracula-state.rkt:420.2

Steps to Reproduce:

Win 7, DrRacket 5.2.1, ACL2 3.2

Open DrRacket, select Modular ACL2, copy the "double triple" example, click the drop down menu perhaps an absurd number of times while the proof is updating, also click around to other areas including the box itself.

Release:

5.2.1

Environment:

windows "Windows NT 6.1 (Build 7601) Service Pack 1" (win32\x86_64\3m) (get-display-depth)
 = 32
Human Language: english
(current-memory-use) 231257136
Links: (links) = (); (links #:user? #f) = (); (links #:root? #t) = (); (links #:user? #f
 #:root? #t) = ()

Collections:
("C:\\Users\\Jason\\AppData\\Roaming\\Racket\\5.2.1\\collects"
 (non-existent-path))
("C:\\Program Files\\Racket\\collects"
 ("2htdp" "algol60" "at-exp" "browser" "combinator-parser" "compiler" "config" "data"
 "datalog" "db" "defaults" "deinprogramm" "drracket" "drscheme" "dynext" "embedded-gui"
 "eopl" "errortrace" "ffi" "file" "framework" "frtime" "games" "graphics" "gui-debugger"
 "help" "hierlist" "htdp" "html" "icons" "images" "info-domain" "lang" "launcher" "lazy"
 "macro-debugger" "make" "mred" "mrlib" "mysterx" "mzcom" "mzlib" "mzscheme" "net"
 "openssl" "parser-tools" "picturing-programs" "plai" "planet" "plot" "preprocessor"
 "profile" "r5rs" "r6rs" "racket" "racklog" "rackunit" "raco" "reader" "readline" "redex"
 "rnrs" "s-exp" "scheme" "schemeunit" "scribble" "scribblings" "scriblib" "setup" "sgl"
 "slatex" "slideshow" "srfi" "stepper" "string-constants" "swindle" "syntax"
 "syntax-color" "teachpack" "test-box-recovery" "test-engine" "tex2page" "texpict" "trace"
 "typed" "typed-racket" "typed-scheme" "unstable" "version" "web-server" "wxme" "xml"
 "xrepl"))

Computer Language: (("Determine language from source") (#(#t print mixed-fraction-e #f #t
 debug) (default) #() "#lang racket\n" #t #t))

This bug was converted from Gnats bug 12634.

[anon-submit; jhemann at indiana dot edu]