WIP on processBlocks

GaloisInc · Aug 15, 2022 · c18c121 · c18c121
1 parent 3c77374
commit c18c121
Showing 1 changed file with 5 additions and 4 deletions.
diff --git a/heapster-saw/examples/sha512_mr_solver.saw b/heapster-saw/examples/sha512_mr_solver.saw
@@ -27,7 +27,8 @@ monadify_term {{ processBlock_spec }};
 monadify_term {{ processBlocks_loop_spec }};
 monadify_term {{ processBlocks_spec }};
 
-mr_solver_prove round_00_15 {{ round_00_15_spec }};
-mr_solver_prove round_16_80 {{ round_16_80_spec }};
-mr_solver_prove processBlock {{ processBlock_spec }};
-// mr_solver_prove processBlocks {{ processBlocks_spec }};
+mr_solver_set_debug_level 3;
+mr_solver_assume round_00_15 {{ round_00_15_spec }};
+mr_solver_assume round_16_80 {{ round_16_80_spec }};
+mr_solver_assume processBlock {{ processBlock_spec }};
+mr_solver_prove processBlocks {{ processBlocks_spec }};