Commit 5f1705a0 authored by Heiko Becker's avatar Heiko Becker

Fix checkerbinaryscript to compile correct thm

parent aa571dab
......@@ -3,6 +3,10 @@ open preamble compilationLib transTheory
val _ = new_theory "checkerBinary"
val checker_compiled = save_thm("checker_compiled",
compile_x64 500 500 "checker" transTheory.entire_program_def);
compile_x64
1000 (* stack size in MB *)
1000 (* heap size in MB *)
"checker"
main_prog_def);
val _ = export_theory ();
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment