Weirdness with tactic failures and --trace_error

```fstar
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.

Start by reproducing the example in Bug.fst with bin/fstar.exe, both with and without --trace_error, and compare the reported verification result. Trace the error-reporting path for tactic failures; done means the second failure is handled consistently and the command never reports successful verification when an error occurred.

Written by the indexing model from the issue text.