Updates

src/theory/tools/symbexec/bir_symb_simpScript.sml

@@ -294,6 +294,14 @@ Proof
   subexpression_simp_TAC
 QED
 
+Theorem birs_simplification_And_left_thm:
+  !pcond symbexp1 symbexp1' symbexp2.
+  (birs_simplification pcond symbexp1 symbexp1') ==>
+  (birs_simplification pcond (BExp_BinExp BIExp_And symbexp1 symbexp2) (BExp_BinExp BIExp_And symbexp1' symbexp2))
+Proof
+  subexpression_simp_TAC
+QED
+
 Theorem birs_simplification_Minus_left_thm:
   !pcond symbexp1 symbexp1' symbexp2.
   (birs_simplification pcond symbexp1 symbexp1') ==>

src/tools/symbexec/birs_mergeLib.sml

@@ -270,9 +270,11 @@ in (* local *)
       val _ = if num_Pi_el > 1 then () else
               raise ERR "birs_Pi_merge_2_RULE" "Pi has to have at least two states";
 
-      (* get the env mapped strings, make sure they have the same ones in each *)
+      (* get the env mapped strings, check that bpc_label is the same for both, make sure they have the same ones in each *)
       val Pi_sys1_tm = List.nth(Pi_tms, 0);
       val Pi_sys2_tm = List.nth(Pi_tms, 1);
+      val _ = if identical (dest_birs_state_pc Pi_sys1_tm) (dest_birs_state_pc Pi_sys2_tm) then () else
+        raise ERR "birs_Pi_merge_2_RULE" "the two states have to agree in their label terms";
       val varnames = birs_env_varnames Pi_sys1_tm;
       val _ = if list_eq_contents gen_eq varnames (birs_env_varnames Pi_sys2_tm) then () else
               raise ERR "birs_Pi_merge_2_RULE" "the two states do not have the same variables mapped in the environment";

src/tools/symbexec/birs_simp_instancesLib.sml

@@ -253,7 +253,8 @@ fun birs_simp_store_cheater simp_tm =
      birs_simplification_Load_addr_thm,
      birs_simplification_Plus_right_thm,
      birs_simplification_Plus_left_thm,
-     birs_simplification_Minus_left_thm]@
+     birs_simplification_Minus_left_thm,
+     birs_simplification_And_left_thm]@
     subexp_cast_thms;
 
 (* ----------------------------------------------------------------------------------- *)

src/tools/symbexec/birs_stepLib.sml

@@ -693,7 +693,7 @@ val birs_symbval_concretizations_oracle_CONV =
    in
     if
       identical tm ((fst o dest_eq o concl) res_thm)
-      handle _ => (print_thm res_thm; raise ERR "birs_symbval_concretizations_oracle_CONV" "failed to resolve single jump target, not an equality theorem")
+      handle _ => (print_thm res_thm; print "\n\n"; print_term tm; print "\n\n"; raise ERR "birs_symbval_concretizations_oracle_CONV" "failed to resolve single jump target, not an equality theorem")
     then res_thm else
     raise ERR "birs_symbval_concretizations_oracle_CONV" "failed to resolve single jump target"
    end);

src/tools/symbexec/birs_strategiesLib.sml

@@ -109,6 +109,7 @@ in (* local *)
             SOME thm
           end
           handle _ => acc);
+        (* val postproc = fn x => let val y = postproc x; in print_thm y; y end; *)
       in
         Option.map postproc (List.foldl foldfun NONE sums_pc)
       end