Assumed function should block tactic

[mtzguido]

This should not work. It finishes correctly in either Dv or Tot.

assume val loop () : Dv unit

let _ = assert True by begin
  loop ();
  ()
end