This file is indexed.

/usr/share/acl2-4.3/books/bdd/benchmarks.acl2 is in acl2-books-source 4.3-3.

This file is owned by root:root, with mode 0o644.

The actual contents of the file can be viewed below.

 1
 2
 3
 4
 5
 6
 7
 8
 9
10
11
12
13
14
15
(value :q)

(lp)

(set-ld-pre-eval-print :never state)

(assign inhibit-output-lst (list (quote prove) (quote proof-tree) (quote warning) (quote observation)))

(include-book "cbf")

(write-benchmark-file "be/" state)

:u

(certify-book "benchmarks")