1

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.

Zoe
  • 27,060
  • 21
  • 118
  • 148
Malte Schwerhoff
  • 12,684
  • 4
  • 41
  • 71

1 Answers1

2

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

Josh Berdine
  • 326
  • 1
  • 1
  • Thanks, that does the trick! It is indeed not mentioned in the SMT-LIB2 standard, but I currently only target Z3 anyway. – Malte Schwerhoff Feb 27 '12 at 12:44
  • Quick note: -smtc option enables a deprecated parser (it is not compliant with the SMT 2.0 standard). This front-end will be removed in future versions of Z3. Please see: http://stackoverflow.com/questions/8439556/soft-hard-constraints-in-z3 for unsat cores extraction in the new SMT 2.0 parser. – Leonardo de Moura Feb 27 '12 at 15:32