check_assumptions via stdin/smt2?

Question

Does the SMT2 standard (or a Z3 extension of it) offer a command equivalent to the API-call "check_assumptions"? According to Josh Berdine it is often faster to work with guard literals and check_assumptions than with push-pop scopes. However, I am stuck with using Z3 via stdio for now, and using (check-assumoptions p) only yields unsupported.

Answer 1

If you are using the smt2 command language, perhaps the 'get-core' command available with 'z3 -smtc -in' will do the job? Note that I think this command is not in the SMT-LIB 2 standard.

Cheers, Josh