From 634e839835d9845fa09bef22cdd4df5d81b0b485 Mon Sep 17 00:00:00 2001
From: Rob Dockins <rdockins@galois.com>
Date: Thu, 20 Jan 2022 11:22:38 -0800
Subject: [PATCH] Tweak the `solveUnsafeAssert` tactic to optimize for the case
 where the values being coerced are actually convertible.

---
 .../handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v  | 1 +
 1 file changed, 1 insertion(+)

diff --git a/saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v b/saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v
index 9ee66439bc..2afacbeb1e 100644
--- a/saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v
+++ b/saw-core-coq/coq/handwritten/CryptolToCoq/CryptolPrimitivesForSAWCoreExtra.v
@@ -67,6 +67,7 @@ Ltac unfoldLets :=
   end.
 
 Ltac solveUnsafeAssert :=
+  try reflexivity;
   try (unfoldLets;
        repeat (repeat solveUnsafeAssertStep; simpl; try reflexivity; try lia);
        trivial).