easyuc / EasyUC

Experiments with Universal Composability in EasyCrypt
30 stars 1 forks source link

proof general weirdnesses #33

Closed alleystoughton closed 11 months ago

alleystoughton commented 11 months ago

In the SMC2 testing script, I couldn't undo the second finish. The first one was undoable.

If I use goto-point, sometimes the final version of goal is not updated.

01tomislav commented 11 months ago

Could not reproduce goto-point problem. I used goto-point, the goal was updated as expected.