Skip to content

Commit bea7f9c

Browse files
committed
fix(examples): missing hints for smt-proved goal
1 parent 3b74196 commit bea7f9c

File tree

1 file changed

+1
-1
lines changed

1 file changed

+1
-1
lines changed

examples/MEE-CBC/RCPA_CMA.ec

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -336,7 +336,7 @@ theory EtM.
336336
type leaks <- leaks,
337337
op leak <- leak,
338338
op dC (l:leaks) <- (dC l) `*` (MUnit.dunit witness<:tag>)
339-
proof * by smt.
339+
proof * by smt(dC_ll dprod_ll dunit_ll).
340340

341341
(** The black-box construction is as follows **)
342342
module EtM(E:SKEa.Enc_Scheme, M:MACa.MAC_Scheme): Enc_Scheme = {

0 commit comments

Comments
 (0)