From 55b0b13e0fc242139a5fcf0ad580bee36ee5ec31 Mon Sep 17 00:00:00 2001 From: Andreas Lindner Date: Thu, 15 Aug 2024 19:23:40 +0200 Subject: [PATCH] Fix environment shape in final states after symbolic execution (birs_gen_env) --- examples/riscv/common/bir_symbLib.sml | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/examples/riscv/common/bir_symbLib.sml b/examples/riscv/common/bir_symbLib.sml index b5ce33260..1e04268cc 100644 --- a/examples/riscv/common/bir_symbLib.sml +++ b/examples/riscv/common/bir_symbLib.sml @@ -107,7 +107,7 @@ fun bir_symb_analysis_thm bir_prog_def bprog_tm birs_state_init_lbl_tm birs_state_end_tm_lbls birs_env_tm birs_pcond_tm; val _ = holba_miscLib.timer_stop (fn delta_s => print ("\n======\n > bir_symb_analysis_thm took " ^ delta_s ^ "\n")) timer; - val symb_analysis_fix_thm = REWRITE_RULE [GSYM birs_env_thm] symb_analysis_thm; + val symb_analysis_fix_thm = CONV_RULE (RAND_CONV (LAND_CONV (REWRITE_CONV [GSYM birs_env_thm]))) symb_analysis_thm; in (bsysprecond_thm, symb_analysis_fix_thm) end (* let *)