API tools faq
paste
Guest User

Untitled

a guest
Feb 24th, 2018
96
0
Never
Add comment
Not a member of Pastebin yet? Sign Up, it unlocks many cool features!
text 14.05 KB | None | 0 0
raw download clone embed print report
  1. ACL2 executable is /Users/penny/Software/acl2/saved_acl2
  2. System books directory is /Users/penny/Software/acl2/books
  3. make -j 1 -f Makefile-tmp --no-builtin-rules all-cert-pl-certs
  4. Making /Users/penny/Software/acl2/books/centaur/aig/aig-sat-tests.cert on 12-Feb-2018 22:42:06
  5. ls: aig-sat-tests.cert: No such file or directory
  6. **CERTIFICATION FAILED** for /Users/penny/Software/acl2/books/centaur/aig/aig-sat-tests.lisp
  7.  
  8. | + WARNING: This is NOT an ACL2 release; it is a development snapshot +
  9. | + (git commit hash: dfd8ee0360499658d7d4cffaaebaaaf2755c6b80). +
  10. | + On rare occasions development snapshots may be incomplete, fragile, +
  11. | + or unable to pass the usual regression tests. +
  12. | +++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++++
  13. |
  14. | Initialized with (INITIALIZE-ACL2 'INCLUDE-BOOK *ACL2-PASS-2-FILES*).
  15. | See the documentation topic note-8-0 for recent changes.
  16. | Note: We have modified the prompt in some underlying Lisps to further
  17. | distinguish it from the ACL2 prompt.
  18. |
  19. | ACL2 Version 8.0. Level 1. Cbd
  20. | "/Users/penny/Software/acl2/books/centaur/aig/".
  21. | System books directory "/Users/penny/Software/acl2/books/".
  22. | Type :help for help.
  23. | Type (good-bye) to quit completely out of ACL2.
  24. |
  25. | ACL2 !>
  26. | Exiting the ACL2 read-eval-print loop. To re-enter, execute (LP).
  27. | ? #<Package "ACL2">
  28. | ? PROVE
  29. | ? CERTIFY-BOOK-FN
  30. | ?
  31. | ACL2 Version 8.0. Level 1. Cbd
  32. | "/Users/penny/Software/acl2/books/centaur/aig/".
  33. | System books directory "/Users/penny/Software/acl2/books/".
  34. | Type :help for help.
  35. | Type (good-bye) to quit completely out of ACL2.
  36. |
  37. | ACL2 !><state>
  38. | ACL2 !> "ACL2"
  39. | ACL2 !> (:EXIT 1)
  40. | ACL2 !> (PROVE PROOF-TREE
  41. | WARNING OBSERVATION EVENT HISTORY)
  42. | ACL2 !> T
  43. | ACL2 !>NIL
  44. | ACL2 !>
  45. | Summary
  46. | Form: ( INCLUDE-BOOK "portcullis" ...)
  47. | Rules: NIL
  48. | Time: 0.38 seconds (prove: 0.00, print: 0.00, other: 0.38)
  49. | "/Users/penny/Software/acl2/books/centaur/aig/portcullis.lisp"
  50. | ACL2 !> T
  51. | ACL2 !>
  52. | ACL2 Version 8.0. Level 2. Cbd
  53. | "/Users/penny/Software/acl2/books/centaur/aig/".
  54. | System books directory "/Users/penny/Software/acl2/books/".
  55. | Type :help for help.
  56. | Type (good-bye) to quit completely out of ACL2.
  57. |
  58. | ACL2 !>> "ACL2"
  59. | ACL2 !>>
  60. | Summary
  61. | Form: ( INCLUDE-BOOK "portcullis" ...)
  62. | Rules: NIL
  63. | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
  64. | :REDUNDANT
  65. | ACL2 !>>
  66. | Summary
  67. | Form: ( INCLUDE-BOOK "cowles/portcullis" ...)
  68. | Rules: NIL
  69. | Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
  70. | "/Users/penny/Software/acl2/books/cowles/portcullis.lisp"
  71. | ACL2 !>>
  72. | Summary
  73. | Form: ( INCLUDE-BOOK "data-structures/portcullis" ...)
  74. | Rules: NIL
  75. | Time: 0.04 seconds (prove: 0.00, print: 0.00, other: 0.04)
  76. | "/Users/penny/Software/acl2/books/data-structures/portcullis.lisp"
  77. | ACL2 !>>
  78. | Summary
  79. | Form: ( DEFPKG "ACL2-HACKER" ...)
  80. | Rules: NIL
  81. | Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
  82. | "ACL2-HACKER"
  83. | ACL2 !>>
  84. | Summary
  85. | Form: ( INCLUDE-BOOK "std/typed-lists/portcullis" ...)
  86. | Rules: NIL
  87. | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
  88. | "/Users/penny/Software/acl2/books/std/typed-lists/portcullis.lisp"
  89. | ACL2 !>>
  90. | Summary
  91. | Form: ( INCLUDE-BOOK "centaur/truth/portcullis" ...)
  92. | Rules: NIL
  93. | Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
  94. | "/Users/penny/Software/acl2/books/centaur/truth/portcullis.lisp"
  95. | ACL2 !>>
  96. | Summary
  97. | Form: ( INCLUDE-BOOK "projects/sat/lrat/portcullis" ...)
  98. | Rules: NIL
  99. | Time: 0.02 seconds (prove: 0.00, print: 0.00, other: 0.02)
  100. | "/Users/penny/Software/acl2/books/projects/sat/lrat/portcullis.lisp"
  101. | ACL2 !>>Bye.
  102. | :EOF
  103. | ACL2 !>
  104. | ACL2 Version 8.0. Level 2. Cbd "/Users/penny/Software/acl2/books/misc/".
  105. | System books directory "/Users/penny/Software/acl2/books/".
  106. | Type :help for help.
  107. | Type (good-bye) to quit completely out of ACL2.
  108. |
  109. | ACL2 !>> "ACL2"
  110. | ACL2 !>>
  111. | Summary
  112. | Form: ( INCLUDE-BOOK "std/portcullis" ...)
  113. | Rules: NIL
  114. | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
  115. | :REDUNDANT
  116. | ACL2 !>>Bye.
  117. | :EOF
  118. | ACL2 !> :CONTINUE
  119. | ACL2 !>
  120. | TTAG NOTE (for included book): Adding ttag :HASH-STOBJS from book /Users/penny/Software/acl2/books/add-ons/hash-stobjs.
  121. |
  122. | ACL2 Warning [Ttags] in ( INCLUDE-BOOK "aig-sat" ...): The ttag note
  123. | just printed to the terminal indicates a modification to ACL2. To
  124. | avoid this warning, supply an explicit :TTAGS argument when including
  125. | the book "/Users/penny/Software/acl2/books/centaur/aig/aig-sat".
  126. |
  127. |
  128. | TTAG NOTE (for included book): Adding ttag :REDEF+ from book /Users/penny/Software/acl2/books/add-ons/hash-stobjs.
  129. |
  130. | ACL2 Warning [Ttags] in ( INCLUDE-BOOK "aig-sat" ...): The ttag note
  131. | just printed to the terminal indicates a modification to ACL2. To
  132. | avoid this warning, supply an explicit :TTAGS argument when including
  133. | the book "/Users/penny/Software/acl2/books/centaur/aig/aig-sat".
  134. |
  135. |
  136. | TTAG NOTE (for included book): Adding ttag :FAST-CONS-MEMO from book /Users/penny/Software/acl2/books/centaur/misc/fast-cons-memo.
  137. |
  138. | ACL2 Warning [Ttags] in ( INCLUDE-BOOK "aig-sat" ...): The ttag note
  139. | just printed to the terminal indicates a modification to ACL2. To
  140. | avoid this warning, supply an explicit :TTAGS argument when including
  141. | the book "/Users/penny/Software/acl2/books/centaur/aig/aig-sat".
  142. |
  143. |
  144. | TTAG NOTE (for included book): Adding ttag :AIG-VARS from book /Users/penny/Software/acl2/books/centaur/aig/aig-vars-fast.
  145. |
  146. | ACL2 Warning [Ttags] in ( INCLUDE-BOOK "aig-sat" ...): The ttag note
  147. | just printed to the terminal indicates a modification to ACL2. To
  148. | avoid this warning, supply an explicit :TTAGS argument when including
  149. | the book "/Users/penny/Software/acl2/books/centaur/aig/aig-sat".
  150. |
  151. |
  152. | TTAG NOTE (for included book): Adding ttag :OSLIB from book /Users/penny/Software/acl2/books/oslib/getpid.
  153. |
  154. | ACL2 Warning [Ttags] in ( INCLUDE-BOOK "aig-sat" ...): The ttag note
  155. | just printed to the terminal indicates a modification to ACL2. To
  156. | avoid this warning, supply an explicit :TTAGS argument when including
  157. | the book "/Users/penny/Software/acl2/books/centaur/aig/aig-sat".
  158. |
  159. |
  160. | TTAG NOTE (for included book): Adding ttag :QUICKLISP from book /Users/penny/Software/acl2/books/quicklisp/base.
  161. |
  162. | ACL2 Warning [Ttags] in ( INCLUDE-BOOK "aig-sat" ...): The ttag note
  163. | just printed to the terminal indicates a modification to ACL2. To
  164. | avoid this warning, supply an explicit :TTAGS argument when including
  165. | the book "/Users/penny/Software/acl2/books/centaur/aig/aig-sat".
  166. |
  167. |
  168. | TTAG NOTE (for included book): Adding ttag :QUICKLISP.SHELLPOOL from book /Users/penny/Software/acl2/books/quicklisp/shellpool.
  169. |
  170. | ACL2 Warning [Ttags] in ( INCLUDE-BOOK "aig-sat" ...): The ttag note
  171. | just printed to the terminal indicates a modification to ACL2. To
  172. | avoid this warning, supply an explicit :TTAGS argument when including
  173. | the book "/Users/penny/Software/acl2/books/centaur/aig/aig-sat".
  174. |
  175. |
  176. | TTAG NOTE (for included book): Adding ttag :TSHELL from book /Users/penny/Software/acl2/books/centaur/misc/tshell.
  177. |
  178. | ACL2 Warning [Ttags] in ( INCLUDE-BOOK "aig-sat" ...): The ttag note
  179. | just printed to the terminal indicates a modification to ACL2. To
  180. | avoid this warning, supply an explicit :TTAGS argument when including
  181. | the book "/Users/penny/Software/acl2/books/centaur/aig/aig-sat".
  182. |
  183. |
  184. | TTAG NOTE (for included book): Adding ttag :SATLINK from book /Users/penny/Software/acl2/books/centaur/satlink/top.
  185. |
  186. | ACL2 Warning [Ttags] in ( INCLUDE-BOOK "aig-sat" ...): The ttag note
  187. | just printed to the terminal indicates a modification to ACL2. To
  188. | avoid this warning, supply an explicit :TTAGS argument when including
  189. | the book "/Users/penny/Software/acl2/books/centaur/aig/aig-sat".
  190. |
  191. | Note (from clause-processors/equality): disabling DISJOIN, DISJOIN2,
  192. | CONJOIN and CONJOIN2.
  193. |
  194. |
  195. | Summary
  196. | Form: ( INCLUDE-BOOK "aig-sat" ...)
  197. | Rules: NIL
  198. | Warnings: Ttags
  199. | Time: 9.89 seconds (prove: 0.00, print: 0.01, other: 9.88)
  200. | "/Users/penny/Software/acl2/books/centaur/aig/aig-sat.lisp"
  201. |
  202. | Summary
  203. | Form: ( INCLUDE-BOOK "misc/assert" ...)
  204. | Rules: NIL
  205. | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
  206. | :REDUNDANT
  207. |
  208. | Summary
  209. | Form: ( DEFUN MY-GLUCOSE-CONFIG ...)
  210. | Rules: ((:EXECUTABLE-COUNTERPART SATLINK::CONFIG)
  211. | (:TYPE-PRESCRIPTION SATLINK::CONFIG)
  212. | (:TYPE-PRESCRIPTION SATLINK::CONSP-OF-CONFIG))
  213. | Time: 0.00 seconds (prove: 0.00, print: 0.00, other: 0.00)
  214. | MY-GLUCOSE-CONFIG
  215. | NIL
  216. |
  217. | Summary
  218. | Form: ( DEFUN TEST-AIG-SAT ...)
  219. | Rules: ((:FAKE-RUNE-FOR-TYPE-SET NIL))
  220. | Time: 0.01 seconds (prove: 0.00, print: 0.00, other: 0.01)
  221. | TEST-AIG-SAT
  222. | Alist: NIL:SUCCESS
  223. | c
  224. | WARNING! DIMACS header mismatch: wrong number of variables.
  225. | c This is glucose 4.0 -- based on MiniSAT (Many thanks to MiniSAT team)
  226. | c
  227. | c ========================================[ Problem Statistics ]===========================================
  228. | c | |
  229. | c | Number of variables: 0 |
  230. | c | Number of clauses: 0 |
  231. | c | Parse time: 0.00 s |
  232. | c | |
  233. | c | Preprocesing is fully done
  234. | c | Simplification time: 0.00 s |
  235. | c | |
  236. | c ========================================[ MAGIC CONSTANTS ]==============================================
  237. | c | Constants are supposed to work well together :-) |
  238. | c | however, if you find better choices, please let us known... |
  239. | c |-------------------------------------------------------------------------------------------------------|
  240. | c | | | |
  241. | c | - Restarts: | - Reduce Clause DB: | - Minimize Asserting: |
  242. | c | * LBD Queue : 50 | * First : 2000 | * size < 30 |
  243. | c | * Trail Queue : 5000 | * Inc : 300 | * lbd < 6 |
  244. | c | * K : 0.80 | * Special : 1000 | |
  245. | c | * R : 1.40 | * Protected : (lbd)< 30 | |
  246. | c | | | |
  247. | c ==================================[ Search Statistics (every 10000 conflicts) ]=========================
  248. | c | |
  249. | c | RESTARTS | ORIGINAL | LEARNT | Progress |
  250. | c | NB Blocked Avg Cfc | Vars Clauses Literals | Red Learnts LBD2 Removed | |
  251. | c =========================================================================================================
  252. | c last restart ## conflicts : 0 0
  253. | c =========================================================================================================
  254. | c restarts : 1 (0 conflicts in avg)
  255. | c blocked restarts : 0 (multiple: 0)
  256. | c last block at restart : 0
  257. | c nb ReduceDB : 0
  258. | c nb removed Clauses : 0
  259. | c nb learnts DL2 : 0
  260. | c nb learnts size 2 : 0
  261. | c nb learnts size 1 : 0
  262. | c conflicts : 0 (0 /sec)
  263. | c decisions : 1 (0.00 % random) (1350 /sec)
  264. | c propagations : 0 (0 /sec)
  265. | c conflict literals : 0 ( nan % deleted)
  266. | c nb reduced Clauses : 0
  267. | c CPU time : 0.000741 s
  268. |
  269. | s SATISFIABLE
  270. | SATLINK: solver says SAT but we didn't find a 0 in variable lines?Alist: NIL
  271. |
  272. | HARD ACL2 ERROR in ASSERT!: Assertion failed:
  273. | (TEST-AIG-SAT T :SAT)
  274. |
  275. |
  276. |
  277. |
  278. | ACL2 Error in ( MAKE-EVENT (LET ...) ...): Evaluation aborted. To
  279. | debug see :DOC print-gv, see :DOC trace, and see :DOC wet.
  280. |
  281. |
  282. | Summary
  283. | Form: ( PROGN (INCLUDE-BOOK "aig-sat" ...) ...)
  284. | Rules: NIL
  285. | Warnings: Ttags
  286. | Time: 10.04 seconds (prove: 0.00, print: 0.01, other: 10.03)
  287. |
  288. | ACL2 Error in ( PROGN (INCLUDE-BOOK "aig-sat" ...) ...): See :DOC
  289. | failure.
  290. |
  291. | ******** FAILED ********
  292. |
  293. | Summary
  294. | Form: (CERTIFY-BOOK "aig-sat-tests" ...)
  295. | Rules: NIL
  296. | Warnings: Ttags
  297. | Time: 10.05 seconds (prove: 0.00, print: 0.01, other: 10.04)
  298. |
  299. | ACL2 Error in (CERTIFY-BOOK "aig-sat-tests" ...): See :DOC failure.
  300. |
  301. | ******** FAILED ********
  302. | ; (EV-REC *RETURN-LAST-ARG3* ...) took
  303. | ; 10.05 seconds realtime, 9.89 seconds runtime
  304. | ; (796,677,392 bytes allocated).
  305. | ACL2 !>Bye.
  306. | Exit code from ACL2 is 0
  307. | aig-sat-tests.cert seems to be missing
  308.  
  309.  
  310. **CERTIFICATION FAILED** for /Users/penny/Software/acl2/books/centaur/aig/aig-sat-tests.lisp
  311.  
  312. make: *** [aig-sat-tests.cert] Error 1
Add Comment
Please, Sign In to add comment
Public Pastes
We use cookies for various purposes including analytics. By continuing to use Pastebin, you agree to our use of cookies as described in the Cookies Policy.  OK, I Understand
Not a member of Pastebin yet?
Sign Up, it unlocks many cool features!