z3 fail -> build fail about z3guide HOT 7 CLOSED

All errors are now rendered in the front-end, so examining the errors by hand on the website is feasible

from z3guide.

Incomplete "Arithmetic" section: looks like you are missing .md suffixes for some files

from z3guide.

Snippet cannot be processed => something with syntax error?

eval_smtlib2_string guarantees to return a string, meaning the error messages will be part of stdout if an error occurs. I think we want the syntax errors for debugging/changing the snippets?

from z3guide.

I guess the expectation is that I fix the errors unless it is obvious.
There are other errors that don't require me in the critical loop:

• I wonder what happend to the "Arithmetic" section. It looks incomplete. It has "Division" but no other subsections.
• I ended up fixing various low hanging issues. For example, _ should be escaped in markdown mode.
  So overall a lot of quality control left at this point, not considering the new material on Sequences I have been adding today.

from z3guide.

meaning the error messages will be part of stdout if an error occurs

Note that you can call Z3.get_error_code right after calling Z3.eval_smtlib2_string to determine if there was an error without needing to parse the output, as in console.log('had error?', Z3.get_error_code(ctx) !== Z3_error_code.Z3_OK). You'll need to import Z3_error_code in the same place you import init.

There's also Z3.get_error_msg but unfortunately it will include the rest of the output from eval_smtlib2_string. I haven't checked if this is a bug in the wasm frontend or if that's just what Z3 itself does.

from z3guide.

in smtlib2 mode (where it interprets a string) the errors are printed to the output string. There can be multiple errors.
This is what is relevant to the SMTLIB2 interpreter mode.
Those errors are not accessible from the error code or message.

from z3guide.

close?

from z3guide.