Home	•	Docs	•	Download	•	Mail	•	FAQ	•	Awards	•	Status	•	MSR

An Efficient SMT Solver

FAQ (Frequently Asked Questions)

• Are you going to support plataform X?
  
  We only support Windows. A Linux binary can be downloaded from the SMT-COMP website.

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

• Why is Z3 1.0 (1.1) slower than Z3 0.1 on the SMT-LIB benchmarks?
  
  It is not, you should use the option AUTO_CONFIG=true with Z3 1.0. In SMT-COMP'07, Z3 0.1 used this option by default. Example:

   z3 AUTO_CONFIG=true -st QF_BV\spear\inn_v2.4.3\innd_innd_vc32473.smt 
  

• Why does Z3 1.2 ignore some of my command line options?
  
  AUTO_CONFIG is enabled by default starting at Z3 1.2. You should use the option AUTO_CONFIG=false if you want to tune Z3 manually.

• AUTO_CONFIG does not work with Simplify and Z3 formats.
  
  AUTO_CONFIG is only supported in the SMT-LIB front-end.

• 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 an OCaml API.

• What is the license for Z3?
  
  The license text is available from the download location.

• Can I use Z3 for commercial purposes?
  
  The Z3 download on this site is available for non-commercial use only. For more information about commercial licensing, contact the Microsoft Research Licensing Group.

• Why can small modifications in the input formula produce significant runtime differences?
  
  Z3 solves problem instances that are co-NP complete. In particular, you can pass 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.smt 
  

• What is the meaning of (bvudiv x bv0[32])?
  
  SMT-LIB does not specify its value. That is, bvudiv(x, y) is uninterpreted when y = 0, one can also say that bvudiv is under-specified. For example, (= (bvudiv x bv0[32]) bv3[32]) is satisfiable. Z3 produces an interpretation for (bvudiv x bv0[32]). The default interpretation is: (bvudiv x bv0[32]) equals zero for every x. Z3 will display the intepretation for (bvudiv x bv0[32]) only when it is not the default one. Z3 uses the same approach to handle other under-specified functions such as: bvsdiv, bvurem, bvsrem, and bvsmod. Note: if you don't like this semantics, you can wrap each occurence of bvudiv with an if-then-else term: (ite (= y 0) [whatever_you_want] (bvudiv x y)).

• Why does Z3 fail to prove (EXISTS (x) (EQ x 0))?
  
  Indeed the fomula is valid, but the handling of quantifiers is incomplete in Z3. So the proof search simply terminates inconclusively, and Z3 states that the formula was invalid. 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, only answers of the form Valid or unsat are conclusive. In the SMT-LIB front-end, Z3 will return unknown for satisfiable formulas that contain quantifiers. {Are there restrictions on what terms can be used in patterns?, Yes\, Z3 does not support patterns with interpreted function symbols. That is\, you cannot use functions such as +\, or relations <=\, <. As an exception, array functions select and store can be used in patterns. There is a simple trick to avoid the interpreted function symbols in patterns\, but still allow you to have the benefit of matching with them: For every interpreted function symbol add a ghost function. For example\, for <= add the function my_LEQ. Add axioms for them: (forall (x y) { (my_LEQ x y) } (iff (my_LEQ x y) (<= x y))). Use the ghost functions everywhere else. }