CODEWITHSUNDEEP
parsingruntime-errorz3
Antonio Morgado
Antonio Morgado

Reputation: 63

Z3 c++, how to parse smt-competition unsat core instances

I am trying to use Z3 with c++ api (version Z3 4.1.0.0), namely i am trying to parse the instances from smt-competition unsat core track. I wrote (based on the examples) the following code:

context c;
Z3_ast f;
f = Z3_parse_smtlib2_file(c, "smtlib_uc/QF_IDL/queens_bench/n_queen/queen3-1.smt2.uc.smt2", 0, 0, 0, 0, 0, 0);
expr r = to_expr(c, f);
solver s(c);
s.add(r);
std::cout << s << "\n";

but i get the following error:

(error "line 1 column 34: error setting ':produce-unsat-cores', option value cannot be modified after initialization")

(error "line 220 column 15: unsat core construction is not enabled, use command (set-option :produce-unsat-cores true)")

unexpected error: parser error

Does anybody knows how to overcome this error ?

Upvotes: 3

Views: 345

Answers (1)

pad
pad

Reputation: 41290

Z3_parse_smtlib* functions are for parsing formulas only; therefore, a lot of options will not work with them.

You can simply delete the line of (set-option :produce-unsat-cores true) in the input file and set that option when initializing context. You can retrieve an unsat core by using Z3_solver_get_unsat_core.

If you don't want to modify input files, you should use Z3 binary instead. These options will be parsed successfully with Z3 binary.

Upvotes: 2

Related Questions