Skip to content

Commit

Permalink
Fix
Browse files Browse the repository at this point in the history
  • Loading branch information
andreaslindner committed Oct 18, 2024
1 parent 83dd54c commit 42ac97a
Showing 1 changed file with 1 addition and 1 deletion.
2 changes: 1 addition & 1 deletion examples/riscv/aes/test-aes.sml
Original file line number Diff line number Diff line change
Expand Up @@ -12,7 +12,7 @@ open aes_symb_execTheory;
(* for now we just have a leightweight check; this is to include aes into the test *)
val _ = print "checking aes_symb_analysis_thm:\n";

val _ = if term_size (concl aes_symb_analysis_thm) = 23403 then () else
val _ = if term_size (concl aes_symb_analysis_thm) = 23173 then () else
raise Fail "term size of aes symbolic execution theorem is not as expected";

val triple_tm = ((snd o dest_comb o concl) aes_symb_analysis_thm);
Expand Down

0 comments on commit 42ac97a

Please sign in to comment.