I'm marking this down to "wish" and changing the title because this is not currently meant to be thoroughly error-checked.

I suggest that we either mark this as resolved in the sense of "we're not going to change this" or change the issue to adding (perhaps optional) error-checking of the SAS+ input file across the board, not just for this specific problem.

Unless someone plans to work on this, my preference is for the former for now. But perhaps we should improve documentation to make the status of this clearer.

> I'm not sure, but I expect we'd even interpret every non-integer token (e.g.
> the word "bla") as the number 0 without complaining.

Yes, I think this is the problem in this case: the second "begin_operator" is parsed as 0 and that is then interpreted as "there are no axioms". After the axiom section, there is nothing left to parse, so the parser returns and the search starts.

Ah, I see. Generally speaking, I think we're doing very little to check the validity of the output.sas files, which are treated mostly as internal. But of course we do document the format and occasionally encourage people to generate it themselves, so perhaps this lack of checks is something we should change.

For example, we document line breaks but I think we don't care about them at all except perhaps around magic words where we might use line-based input rather than token-based input. I don't think we range-check any of the integers except perhaps via assertions, which are a debug feature rather than an input validation feature. I'm not sure, but I expect we'd even interpret every non-integer token (e.g. the word "bla") as the number 0 without complaining. There are also more semantic things like affecting the same variable twice with non-conditional effects, which we don't allow.

That doesn't mean I'd be against introducing checks that people find useful. But then perhaps we should consider doing this consistently while we're looking at this part of the planner.

All the mentioned possible deficiencies are from memory. Perhaps we do actually check the input and I forgot. :-)

I had already deleted the file, but it's not too complicated. With "declared", I meant the number above the first "begin_operator" that says how many operators there will be. It is 1 in this case, but then there two blocks of "begin_operator ... end_operator" (and no axiom section).

I think no file was attached, can you add it? Not sure what you mean with "declared" vs. "defined", looking forward to seeing the file. :-)

In the attached file, one operator is declared but then two are defined. I would have expected the parser to parse the first operator and then try to parse the axiom section and fail because instead of a number of axioms, it gets "begin_operator". But instead, the parser accepts the file.