In the presence of a datatype declaration in the root theory (argument theoryref in the unusedby-proofs-of-formulas LISP function) the assertion (assert th) in the unused-by-proofs-of LISP function fails.
An simple way to reproduce is to add the following to Examples/sum.pvs
dummy_dt: DATATYPE
BEGIN
dummy: dummy?
END dummy_dt
then open this theory in emacs and run
M-x tcp
M-x unsedby-proofs-of-formulas
Formula: closed_form
Formula:
Root theory to use as context: (default: sum):
The assertion will show in the pvs buffer.
Reproduced in PVS 6.0 with Allegro and PVS 7.0 (from git) with SBCL.
In the presence of a datatype declaration in the root theory (argument theoryref in the unusedby-proofs-of-formulas LISP function) the assertion (assert th) in the unused-by-proofs-of LISP function fails. An simple way to reproduce is to add the following to Examples/sum.pvs
then open this theory in emacs and run
The assertion will show in the pvs buffer. Reproduced in PVS 6.0 with Allegro and PVS 7.0 (from git) with SBCL.