diff --git a/theories/simulang/na_inv/examples/data_races.v b/theories/simulang/na_inv/examples/data_races.v
index c6e4aa0786fc14fe7421009038a17225f63acd2c..21672c1e5ae90a6aa61079835ba7d75e8a48fc19 100644
--- a/theories/simulang/na_inv/examples/data_races.v
+++ b/theories/simulang/na_inv/examples/data_races.v
@@ -152,7 +152,7 @@ Section data_race.
       rewrite bool_decide_eq_true_2; last done.
       sim_pures. iApply sim_expr_base. iLeft. iApply lift_post_val.
 
-      sim_pures. source_load. target_load. to_sim. sim_pures.
+      sim_pures. source_load. target_load. sim_pures.
       (* cleanup *)
       source_free. source_free. target_free. target_free. sim_pures.
       iApply (sim_bij_release (NaRead q) with "Hbij Hc Hl_t Hl_s [//]").
diff --git a/theories/simulang/tactics.v b/theories/simulang/tactics.v
index bdf8b9751114340c7f091babeec174208a629fbc..0e21457af7afab9fd7337a709368fa8c80fc769f 100644
--- a/theories/simulang/tactics.v
+++ b/theories/simulang/tactics.v
@@ -384,10 +384,14 @@ Ltac simpl_subst :=
       let e' := W.of_expr e in
       simple refine (W.tac_to_expr_subst _ _ _ _ e' _ _ _ _); [ shelve
       | simpl; rewrite ?list_to_map_to_list; reflexivity
-      | simpl; compute_done
+      | 
+          (* FIXME: really hacky hack to speed up goals on which [compute_done] takes forever due to evars, 
+              but where [simpl] would suffice...*)
+          first [timeout 1 compute_done | simpl; reflexivity]
       |];
       simple refine (W.tac_to_expr_combine_subst_map _ _ _ _ _); [ shelve |
-      simpl; compute_done | ];
+      (* FIXME *)
+      first [timeout 1 compute_done | simpl; reflexivity] | ];
       simpl
     end.
 Arguments subst : simpl never.