feat: reject multiple setup paths #351
Conversation
| // vm.assume(mode0 < 9); | ||
| // NOTE: explicitly branch over mode0, as an infeasible path with mode0 >= 9 may not be eliminated due to an extremely inefficient solver environment (e.g, github workflow) | ||
| mode0 = split_mode_up_to_9(mode0); | ||
|
|
||
| _check_call0(mode0); |
There was a problem hiding this comment.
wait what? I don't understand what's going on here
There was a problem hiding this comment.
this is not related to this pr. it's a temporary fix to a flaky test that i found.
details of the flaky test: when mode0 == 9, _check_call0() fails due to HalmosException (which is intentional). however, the goal of this test is to consider only success paths, so the assumption mode0 < 9 is provided at the beginning. however, the HalmosException path may still appear after path exploration, if the branching solver couldn't solve its infeasible path condition. this won't happen under normal circumstances, as the path condition mode0 < 9 && mode0 == 9 is obviously unsat. but in the github runner, the solver may timeout, leading to a test failure, due to the HalmosException path, even if it is infeasible. a proper fix is more involved, and will be implemented later.
balance is addressed in #352
we could add a bypass flag, or make this optional (e.g., --strict), later if this turns out to cause test failures too often. |
currently, if multiple setup paths exist, one of them is randomly selected and used for testing. since the existence of multiple setup paths are likely due to an incorrect setup(), this behavior makes debugging more challenging. to address this, now it will fail immediately when multiple setup paths are detected.
to be merged after #350