Options iteration when tracing is enabled

[aytey]

When running with BTORAPITRACE, Boolector crashes on any functionality that iterates over options (e.g., running --help or using the Python API).

The flow is (similar) to this:

• export BTORAPITRACE="temp"

• run boolector --help

• main -> boolector_main -> print_help

• print_help iterates over the options, and hits: boolector_next_opt (for the last option) and then goes around the loop and tries to run boolector_has_opt with o == BTOR_OPT_NUM_OPTS

• If tracing is enabled, then boolector_has_opt calls btor_opt_get_lng, which in turn calls btor_opt_is_valid -- if the option is not strictly less than BTOR_OPT_NUM_OPTS, then there is an assertion failure!

This bug is more obviously exposed when using the Python API. When using the Python API, creating a Boolector() instance leads to an instantiation of BoolectorOptions, which is iterated over to construct self._option_names in the Boolector class (pyboolector.pyx). Eventually this iteration gets close enough to BTOR_OPT_NUM_OPTS, that the same assertion fails.

The solution here was to make boolector_has_opt check if the current option is BTOR_OPT_NUM_OPTS before calling btor_opt_get_lng.

[mpreiner]

Good catch @andrewvaughanj! The only issue is that this breaks untracing via btoruntrace. This seems to be a general issue with tracing the options in the C API. As soon as an invalid option is passed it can't print the name of the option for the trace. I'll try to figure out a fix asap. Thanks again for reporting!

[aytey]

@mpreiner ah, I guess maybe this would have been better as an issue then.

Do you want me to leave this PR open as a reminder, or close and create an issue?

[mpreiner]

No worries, yes please open an issue.

[aniemetz]

Fixed in https://github.com/Boolector/boolector/commit/5a3b5c88ea9c9dcf4232e33546f69d80d7424b13.