Fix CI tests

kth-step · Jan 31, 2025 · 2c0d089 · 2c0d089
1 parent ee762f6
commit 2c0d089
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 88 deletions.
diff --git a/examples/riscv/aes/test-aes.sml b/examples/riscv/aes/test-aes.sml
@@ -14,7 +14,7 @@ val _ = print "checking aes_symb_analysis_thm:\n";
 
 val term_sz = term_size (concl aes_symb_analysis_thm);
 val _ = print ("\nterm size = " ^ (Int.toString term_sz) ^ "\n\n");
-val expected_term_sz = 25198;
+val expected_term_sz = 21001;
 
 val _ = if term_sz = expected_term_sz then () else
         raise Fail "term size of aes symbolic execution theorem is not as expected";

diff --git a/src/tools/symbexec/examples/test-birs_compose.sml b/src/tools/symbexec/examples/test-birs_compose.sml
@@ -92,12 +92,13 @@ val bprog_tm = bprog;
 *)
 fun execute_two_steps bprog_tm birs_state_init_tm =
  let
-  val birs_rule_STEP_thm = birs_rule_STEP_prog_fun (birs_auxLib.get_prog_no_halt_thm bprog_tm);
+  val (birs_rule_STEP_thms, _) =
+    birs_rule_STEP_prog_fun (birs_auxLib.get_prog_no_halt_thm bprog_tm);
 
   fun birs_post_step_fun (t, _) = (
     birs_rule_tryjustassert_fun false
   ) t;
-  val birs_rule_STEP_fun_spec = birs_post_step_fun o birs_rule_STEP_fun birs_rule_STEP_thm;
+  val birs_rule_STEP_fun_spec = birs_post_step_fun o birs_rule_STEP_fun birs_rule_STEP_thms;
   (* ........................... *)
 
   (* first step *)

diff --git a/src/tools/symbexec/examples/test-freesymb.sml b/src/tools/symbexec/examples/test-freesymb.sml