Reinstate group_red_aux subproof in ecdsa-crucible.saw.

It was previously stubbed out to avoid a bug that no longer occurs.
GaloisInc · Nov 16, 2020 · 2947d87 · 2947d87
1 parent 001b046
commit 2947d87
Showing 1 changed file with 1 addition and 2 deletions.
diff --git 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 {