Weirdness with tactic failures and --trace_error

[mtzguido]

open FStar.Tactics.V2

[@@expect_failure]
let _ = assert True by begin
  fail "fail"
end

let _ = assert True by begin
  fail "fail"
end

This module rightly fails:

$ ./bin/fstar.exe Bug.fst 
proof-state: State dump @ depth 0 (at the time of failure):
Location: Bug.fst(7,2-7,13)
Goal 1/1:
 |- _ : Prims.squash Prims.l_True

proof-state: State dump @ depth 0 (at the time of failure):
Location: Bug.fst(11,2-11,13)
Goal 1/1:
 |- _ : Prims.squash Prims.l_True

* Error 228 at Bug.fst(10,8-10,14):
  - Tactic failed
  - fail
  - See also Bug.fst(11,2-11,13)

1 error was reported (see above)

But ends up claiming success if --trace_error is given...

$ ./bin/fstar.exe Bug.fst --trace_error 
proof-state: State dump @ depth 0 (at the time of failure):
Location: Bug.fst(7,2-7,13)
Goal 1/1:
 |- _ : Prims.squash Prims.l_True

Verified module: Bug
All verification conditions discharged successfully

Of course it didn't actually check the second tactic, but it's worrisome still. I think this may be stopping since we have logged an error in the first definition, so the second tactic is prevented from running. But in no case should we report success.