From 2947d8772104c0828aecb1876a3e162079331837 Mon Sep 17 00:00:00 2001
From: Brian Huffman <huffman@galois.com>
Date: Thu, 12 Nov 2020 16:08:58 -0800
Subject: [PATCH] Reinstate group_red_aux subproof in ecdsa-crucible.saw.

It was previously stubbed out to avoid a bug that no longer occurs.
---
 examples/ecdsa/ecdsa-crucible.saw | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/examples/ecdsa/ecdsa-crucible.saw b/examples/ecdsa/ecdsa-crucible.saw
index 0591432515..2fe6fc4832 100644
--- a/examples/ecdsa/ecdsa-crucible.saw
+++ b/examples/ecdsa/ecdsa-crucible.saw
@@ -1171,8 +1171,7 @@ group_red_aux_ov <- method "group_red_aux" []
     ecdsa_assign_arr384 pr {{ res.gra_r }};
     jvm_return (jvm_term {{ res.gra_b }});
   }
-  //z3; //FIXME: This has problems due to a bug (in SBV?) where the wrong right-shift instruction is generated.
-  assume_unsat;
+  z3;
 
 group_red_ov <- method "group_red" [sub_ov2, group_red_aux_ov]
   do {