diff --git a/InteractionTrees b/InteractionTrees
index 8e28e2ee0..dda104937 160000
--- a/InteractionTrees
+++ b/InteractionTrees
@@ -1 +1 @@
-Subproject commit 8e28e2ee08496c696e03916a22d93c39559a9715
+Subproject commit dda104937d79e2052d1a26f6cbe89429245ff743
diff --git a/fcf b/fcf
index f775e6326..f1bd5f390 160000
--- a/fcf
+++ b/fcf
@@ -1 +1 @@
-Subproject commit f775e6326c0f28e43e03c4429fe7cc988cfa6af5
+Subproject commit f1bd5f3903771d78c85ba48f30c6e155aed2b48f
diff --git a/floyd/forward.v b/floyd/forward.v
index 134fe5cde..3d006c796 100644
--- a/floyd/forward.v
+++ b/floyd/forward.v
@@ -2099,11 +2099,14 @@ Lemma typed_true_ptr' :
   typed_true (tptr t) v -> isptr v.
 Proof. intros ? ?. apply typed_true_ptr. Qed.
 
+
 Ltac do_repr_inj H :=
    simpl typeof in H;  (* this 'simpl' should be fine, since its argument is just clightgen-produced ASTs *)
+   cbv delta [Int64.zero Int.zero] in H;
    lazymatch type of H with
       | typed_true _ ?A => 
            change (typed_true tuint) with (typed_true tint) in H;
+           change (typed_true tulong) with (typed_true tlong) in H;
           let B := eval hnf in A in change A with B in H;
           try first
                [ simple apply typed_true_of_bool' in H
@@ -2115,20 +2118,23 @@ Ltac do_repr_inj H :=
                | simple apply typed_true_Ceq_eq' in H
                | apply typed_true_nullptr4 in H
                | simple apply typed_true_Cne_neq' in H
+               | simple apply typed_true_tlong_Vlong in H
               ]
       | typed_false _ ?A => 
            change (typed_false tuint) with (typed_false tint) in H;
+           change (typed_false tulong) with (typed_false tlong) in H;
            let B := eval hnf in A in change A with B in H;
            try first
                [ simple apply typed_false_of_bool' in H
                | simple apply typed_false_ptr_e in H
-               | simple apply typed_false_negb_bool_val_p in H; [| solve [auto]]
+               | simple apply typed_false_negb_bool_val_p in H; [| solve [auto ] ]
                | apply typed_false_negb_bool_val_p' in H
                | simple apply typed_false_tint_Vint in H
                | apply typed_false_nullptr3 in H
                | simple apply typed_false_Ceq_neq' in H
                | apply typed_false_nullptr4 in H
                | simple apply typed_false_Cne_eq' in H
+               | simple apply typed_false_tlong_Vlong in H
                ]
      | _ => idtac
     end;
@@ -2152,6 +2158,8 @@ Ltac do_repr_inj H :=
   end;
   first [ simple apply repr_inj_signed in H; [ | rep_lia | rep_lia ]
          | simple apply repr_inj_unsigned in H; [ | rep_lia | rep_lia ]
+         | simple apply repr_inj_signed64 in H; [ | rep_lia | rep_lia ]
+         | simple apply repr_inj_unsigned64 in H; [ | rep_lia | rep_lia ]
          | simple apply repr_inj_signed' in H; [ | rep_lia | rep_lia ]
          | simple apply repr_inj_unsigned' in H; [ | rep_lia | rep_lia ]
          | simple apply ltu_repr in H; [ | rep_lia | rep_lia]
diff --git a/floyd/functional_base.v b/floyd/functional_base.v
index 273b07a7d..17639b40e 100644
--- a/floyd/functional_base.v
+++ b/floyd/functional_base.v
@@ -724,6 +724,18 @@ rewrite <- (Int.signed_repr j) by rep_lia.
 congruence.
 Qed.
 
+Lemma repr_inj_signed64:
+  forall i j,
+    Int64.min_signed <= i <= Int.max_signed ->
+    Int64.min_signed <= j <= Int.max_signed ->
+    Int64.repr i = Int64.repr j -> i=j.
+Proof.
+intros.
+rewrite <- (Int64.signed_repr i) by rep_lia.
+rewrite <- (Int64.signed_repr j) by rep_lia.
+congruence.
+Qed.
+
 Lemma repr_inj_unsigned:
   forall i j,
     0 <= i <= Int.max_unsigned ->
diff --git a/floyd/val_lemmas.v b/floyd/val_lemmas.v
index ba12e1083..1e24c7102 100644
--- a/floyd/val_lemmas.v
+++ b/floyd/val_lemmas.v
@@ -447,6 +447,15 @@ pose proof (Int64.eq_spec v Int64.zero).
 destruct (Int64.eq v Int64.zero); auto. inv H.
 Qed.
 
+Lemma typed_false_tlong_Vlong:
+  forall v, typed_false tlong (Vlong v) -> v = Int64.zero.
+Proof.
+intros.
+unfold typed_false, strict_bool_val in H. simpl in H.
+pose proof (Int64.eq_spec v Int64.zero).
+destruct (Int64.eq v Int64.zero); auto. discriminate.
+Qed.
+
 Ltac intro_redundant P :=
  match goal with H: P |- _ => idtac end.