CODEWITHSUNDEEP
z3sat
zell
zell

Reputation: 10204

How to let z3 command line output the mode (or unsat core) rather than sat/unsat?

z3 -smt2 <filename> only outputs 'sat' or 'unsat'. I would like that Z3 outputs the model if the constraint is satisfied, or the unsat core if unsatisfied. Which options of Z3 should I use?

Upvotes: 0

Views: 458

Answers (1)

Christoph Wintersteiger
Christoph Wintersteiger

Reputation: 8393

There are no command line options for this as in SMTLIB2 they are separate commands, (get-model) and (get-unsat-core), both only defined when (check-sat) returns sat or unsat respectively.

The options model and unsat-core have to be enabled irrespective of whether those or other commands are used, just to make the solver tracks the right information, otherwise the (get-model) and (get-unsat-core) commands may fail later.

Upvotes: 2

Related Questions