Add z3new as solver type command line flag, which sets sat.smt=true.

[cp526]

Due to some previous Z3 bug, this will only work for versions newer than the as yet unpublished 4.13.4.

Even than, this flag does not currently work correctly due to some change in the z3-produced SMT models.

[yav]

I am not sure if adding Z3new to solver_extensions is the right approach for this. The idea with solver_extensions was to help us handle SMT translations that differ between the solvers (i.e., things outside the SMTLIB standard).

It looks like here we just want to initialize the solver in a different way, rather than change how things are translated.

An alternative I'd suggest is perhaps to add another option to the solver, I guess for now it could be a boolean flag, and when creating the solver we can use either SMT.z3 or SMT.z3new depending on the flag.

Longer run, I think a better design might be to remove the global flags and instead pass them as parameters to make.

[cp526]

I am not sure if adding Z3new to solver_extensions is the right approach for this. The idea with solver_extensions was to help us handle SMT translations that differ between the solvers (i.e., things outside the SMTLIB standard).

It looks like here we just want to initialize the solver in a different way, rather than change how things are translated.

An alternative I'd suggest is perhaps to add another option to the solver, I guess for now it could be a boolean flag, and when creating the solver we can use either SMT.z3 or SMT.z3new depending on the flag.

Longer run, I think a better design might be to remove the global flags and instead pass them as parameters to make.

Thanks!

Agreed. This is more a short-term experiment, to see if the sat.smt option can be made to work. In the longer term we may not want this parameter at all, but either discard it (if it doesn't help) or make it the default (if it does).

Running the above code with z3 nightly and z3new on I see line

cerberus/backend/cn/lib/simple_smt.ml

Line 605 in d8cb893

raise (UnexpectedSolverResponse ans) (* recursive *)

raising an exception. Does this mean z3 generates a model with recursive definitions?