Fix unoptimized motor binary example

kth-step · Nov 21, 2024 · beab4b6 · beab4b6
1 parent 1a497c3
commit beab4b6
Show file tree

Hide file tree

Showing 2 changed files with 3 additions and 1 deletion.
diff --git a/examples/riscv/motor-unopt/motor_symb_execScript.sml b/examples/riscv/motor-unopt/motor_symb_execScript.sml
@@ -21,7 +21,7 @@ val _ = birs_auxLib.prepare_program_lookups bir_lift_thm;
 (* --------------------------- *)
 
 (* turn on the store-store cheater *)
-val _ = birs_simp_select := birs_simp_instancesLib.birs_simp_default_riscv_gen true;
+val _ = birs_strategiesLib.birs_simp_select := birs_simp_instancesLib.birs_simp_default_riscv_gen true birs_simpLib.birs_simp_ID_fun [];
 
 val symb_analysis_thm =
  bir_symb_analysis_thm

diff --git a/examples/riscv/motor-unopt/motor_symb_mergeScript.sml b/examples/riscv/motor-unopt/motor_symb_mergeScript.sml
@@ -1,6 +1,8 @@
 open HolKernel Parse boolLib bossLib;
 
 open birs_mergeLib;
+open birsSyntax;
+open birs_utilsLib;
 
 open motor_symb_execTheory;