e.g. the one suggested in this warning:
WARNING: For problems containing quantifiers, the model finding capabilities of Z3 work better when the formula does not
contain nested quantifiers. You can use PULL_NESTED_QUANTIFIERS=true to eliminate nested quantifiers.
there are some settings to consider.
e.g. the one suggested in this warning: WARNING: For problems containing quantifiers, the model finding capabilities of Z3 work better when the formula does not contain nested quantifiers. You can use PULL_NESTED_QUANTIFIERS=true to eliminate nested quantifiers.