FAQ (Frequently Asked Questions)

• Are you going to support plataform X?
  
  We only provide full support for Windows, but we build Z3 for other platforms (Linux and OSX). For example, we have a Linux binary for the SMT competition. The latest version of this can be downloaded here.

• Are you going to release Z3 source code?
  
  We do not know yet.

• Can I use the Z3 DLL with gcc?
  
  The subdirectory examples\C_API contains the shell script build.sh to build the test application using gcc.

• What is the calling convention used in the Z3 DLL?
  
  We use the native calling convention of C/C++ (__cdecl).

• What is the difference between z3.dll and z3_dbg.dll?
  
  z3_dbg.dll contains assertion checking. You can use it to check whether you are using the API correctly or not.

• Which API should I use?
  
  If you are using C/C++ or a programming language that is not available in the .NET framework, you should use the C API. Otherwise, you should use the Managed (.NET) API. We also provide OCaml and Python APIs.

• What is the license for Z3?The non-commercial license text is available from the download location. The commercial license is available here.

• Can I use Z3 for commercial purposes?
  
  The Z3 download on this site is available for non-commercial use only (e.g., research projects, prototypes, evaluations, etc). Z3 is available for commercial use at the Microsoft Store (commercial license). For more information about commercial licensing, contact the Behrooz Chitsaz.

• Why can small modifications in the input formula produce significant runtime differences?
  
  Z3 can be used to solve many intractable problems (from NP-complete to undecidable). So, it is heavily based on heuristics. For example, let us consider the satisfiability of propositional formulas. You can pass propositional formulas where Z3 can immediately identify a satisfying assignment because the search happened to initially choose the right assignments, or Z3 may be able to identify a small proof quickly because it performed the right case splits early. But if Z3 does not start with the right assignments or case splits it is possible that search may take a long time. The input format influences the initial assignments and case split order. You can pertube the case split order by using the options /rd: and /rs. These options control the randomization in Z3. Example:

   z3 -rd:5 -rs:100 -st withOpt.smt2 
  

• Why does Z3 return unknown in some problems containing quantifiers?
  
  Z3 is complete for various quantifier free fragments, so it will give correct answers when the formulas are quantifier free, but when the formulas contain quantifiers, Z3 may return unknown. Recall that there is no sound and complete procedure for first-order logic formulas of linear arithmetic with uninterpreted function symbols.

• How can I extract an unsatisfiable core?
  
  You can used named assertions as defined in the SMT2 language. Example:

           (set-option :produce-unsat-cores true)
           (declare-fun x () (_ BitVec 32))
           (declare-fun y () (_ BitVec 32))
           (assert (! (not (not (= x #x00000000))) :named a1))
           (assert (! (not (= y #x00000000)) :named a2))
           (assert (! (not (= x #x00000000)) :named a3))
           (check-sat)
           (get-unsat-core)