Z3 parse smt2 file returns Erorr

[mm95]

Hello,

I ran cbmc for comm.c file in coreutils of linux and get smt2 file with inserting '--smt2' option and then use Z3_parse_smtlib2string function of z3 to parse resulted smt2 formula with z3 parser but get parse error. all files were attached.

cbmc comm.c -I .. --smt2 --outfile result.smt2 --unwind 2

Z3_parse_smtlib2_string(*ctx, smt_formula_stream.str().c_str(), 0, 0, 0, 0, 0, 0);

thanks very much.

comm.c.txt
z3-parse-Error.txt
result.smt2.txt

[NlightNFotis]

Apologies, I am unable to reproduce this issue (given that it also depends on a number of includes that have not been provided as part of this report).

Given that this is a very old issue and a number of changes have happened to both z3 and cbmc, I'm going to go ahead and close the issue for now.

If you do find that this remains to be an error, please let us know, and we'll reopen and investigate further.

It's also worth knowing that this is using the old SMT backend, and we are now working on a redesign of that. Once that's finished (admittedly, will take some time) the old SMT backend will be deprecated.