z3prover / z3 Goto Github PK

The Z3 Theorem Prover

License: Other

C++ 88.21% C 1.90% C# 2.43% Java 1.59% OCaml 0.94% Python 3.15% Shell 0.01% SMT 0.12% CMake 0.66% Makefile 0.01% Batchfile 0.01% Dockerfile 0.01% D 0.06% TypeScript 0.92% JavaScript 0.01%

z3's Introduction

Z3

Z3 is a theorem prover from Microsoft Research. It is licensed under the MIT license.

If you are not familiar with Z3, you can start here.

Pre-built binaries for stable and nightly releases are available from here.

Z3 can be built using Visual Studio, a Makefile or using CMake. It provides bindings for several programming languages.

See the release notes for notes on various stable releases of Z3.

Build status

Azure Pipelines	Code Coverage	Open Bugs	Android Build	WASM Build	Windows Build

Docker image.

Building Z3 on Windows using Visual Studio Command Prompt

32-bit builds, start with:

python scripts/mk_make.py

or instead, for a 64-bit build:

python scripts/mk_make.py -x

then:

cd build
nmake

Z3 uses C++17. The recommended version of Visual Studio is therefore VS2019.

Building Z3 using make and GCC/Clang

Execute:

python scripts/mk_make.py
cd build
make
sudo make install

Note by default g++ is used as the C++ compiler if it is available. If you would prefer to use Clang change the mk_make.py invocation to:

CXX=clang++ CC=clang python scripts/mk_make.py

Note that Clang < 3.7 does not support OpenMP.

You can also build Z3 for Windows using Cygwin and the Mingw-w64 cross-compiler. To configure that case correctly, make sure to use Cygwin's own python and not some Windows installation of Python.

For a 64 bit build (from Cygwin64), configure Z3's sources with

CXX=x86_64-w64-mingw32-g++ CC=x86_64-w64-mingw32-gcc AR=x86_64-w64-mingw32-ar python scripts/mk_make.py

A 32 bit build should work similarly (but is untested); the same is true for 32/64 bit builds from within Cygwin32.

By default, it will install z3 executable at PREFIX/bin, libraries at PREFIX/lib, and include files at PREFIX/include, where PREFIX installation prefix is inferred by the mk_make.py script. It is usually /usr for most Linux distros, and /usr/local for FreeBSD and macOS. Use the --prefix= command line option to change the install prefix. For example:

python scripts/mk_make.py --prefix=/home/leo
cd build
make
make install

To uninstall Z3, use

sudo make uninstall

To clean Z3 you can delete the build directory and run the mk_make.py script again.

Building Z3 using CMake

Z3 has a build system using CMake. Read the README-CMake.md file for details. It is recommended for most build tasks, except for building OCaml bindings.

Building Z3 using vcpkg

vcpkg is a full platform package manager, you can easily install libzmq with vcpkg.

Execute:

git clone https://github.com/microsoft/vcpkg.git
./bootstrap-vcpkg.bat # For powershell
./bootstrap-vcpkg.sh # For bash
./vcpkg install z3

Dependencies

Z3 itself has few dependencies. It uses C++ runtime libraries, including pthreads for multi-threading. It is optionally possible to use GMP for multi-precision integers, but Z3 contains its own self-contained multi-precision functionality. Python is required to build Z3. To build Java, .Net, OCaml, Julia APIs requires installing relevant tool chains.

Z3 bindings

Z3 has bindings for various programming languages.

`.NET`

You can install a nuget package for the latest release Z3 from nuget.org.

Use the --dotnet command line flag with mk_make.py to enable building these.

See examples/dotnet for examples.

`C`

These are always enabled.

See examples/c for examples.

`C++`

These are always enabled.

See examples/c++ for examples.

`Java`

Use the --java command line flag with mk_make.py to enable building these.

See examples/java for examples.

`OCaml`

Use the --ml command line flag with mk_make.py to enable building these.

See examples/ml for examples.

`Python`

You can install the Python wrapper for Z3 for the latest release from pypi using the command

   pip install z3-solver

Use the --python command line flag with mk_make.py to enable building these.

Note that it is required on certain platforms that the Python package directory (site-packages on most distributions and dist-packages on Debian based distributions) live under the install prefix. If you use a non standard prefix you can use the --pypkgdir option to change the Python package directory used for installation. For example:

python scripts/mk_make.py --prefix=/home/leo --python --pypkgdir=/home/leo/lib/python-2.7/site-packages

If you do need to install to a non standard prefix a better approach is to use a Python virtual environment and install Z3 there. Python packages also work for Python3. Under Windows, recall to build inside the Visual C++ native command build environment. Note that the build/python/z3 directory should be accessible from where python is used with Z3 and it depends on libz3.dll to be in the path.

virtualenv venv
source venv/bin/activate
python scripts/mk_make.py --python
cd build
make
make install
# You will find Z3 and the Python bindings installed in the virtual environment
venv/bin/z3 -h
...
python -c 'import z3; print(z3.get_version_string())'
...

See examples/python for examples.

`Julia`

The Julia package Z3.jl wraps the C++ API of Z3. Information about updating and building the Julia bindings can be found in src/api/julia.

`Web Assembly` / `TypeScript` / `JavaScript`

A WebAssembly build with associated TypeScript typings is published on npm as z3-solver. Information about building these bindings can be found in src/api/js.

Smalltalk (`Pharo` / `Smalltalk/X`)

Project MachineArithmetic provides Smalltalk interface to Z3's C API. For more information, see MachineArithmetic/README.md

System Overview

Interfaces

Default input format is SMTLIB2
Other native foreign function interfaces:
C++ API
.NET API
Java API
Python API (also available in pydoc format)
Rust
C
OCaml
Julia
Smalltalk (supports Pharo and Smalltalk/X)

z3's People

Contributors

Stargazers

Watchers

Forkers

wintersteiger audreyt melted bendisposto belyaev-mikhail mrange applied-duality agurfinkel seahorn leodemoura atnnn codemac tkim johnjohnsp1 neuroradiology smilliken madars silky liuliu jslhs idkwim solualexis languagefun crowell leehoy nushio3 beronx86 g4idrijs zclfly huixue tekacs jbulow jilir rolinston prodigeni lovesuae passwind ranchoice deliangyang jiangpengnju clashthebunny rhennigan wware jam231 sashka drup thomasjball sbahra zimmski bauna confusion pcc dr1861 conceptofproof richardlford daniel-j-h benlaurie terrywingit cyberdot x4 jornason akghosh agriggio esaul somebody365 hkhlaaf jellyrepo angr cholmes3 ykram dbueno killvxk ahorn mschlaipfer odaira diepbp abduld neuroidss nikolajbjorner asmeurer jmgrosen shyamalschandra aleksandarzeljic smadhuk hasibshakur dmitriy403 mermakov greatmazinger dnunez02 akanakia xujiesi redjbishop pysmt wadaries mavenrain hgoes andrey-rybalchenko kyledewey ffengcs baha

z3's Issues

fp.isNegative does not handle NaN properly

This is on the unstable branch.

For this benchmark:

(set-option :produce-models true)
(set-logic QF_FP)
(declare-fun s0 () (_ FloatingPoint 11 53))
(assert
   (let ((s1 (and (fp.isNaN s0) (fp.isNegative s0))))
   s1))
(check-sat)
(get-value (s0))

Z3 produces:

sat
((s0 (_ NaN 11 53)))

Which suggests NaN is accepted by the predicate fp.isNegative. According to the formalization, fp.isNegative holds for -0.0 and when the number lt compares to 0 successfully, neither of which is true for NaN.

darwin build linker assertion with gcc and clang

On Yosemite with latest xcode clang and macports clang 4.7 and gcc-4.9 and gcc-5
I get the same build errors, when searching files for unresolved symbols.
I didn't get those with older builds from about a year ago.

e.g. xcode clang
$ g++ --version
Configured with: --prefix=/Applications/Xcode.app/Contents/Developer/usr --with-gxx-include-dir=/usr/include/c++/4.2.1
Apple LLVM version 6.0 (clang-600.0.57) (based on LLVM 3.5svn)
Target: x86_64-apple-darwin14.1.0
Thread model: posix

g++ -o libz3.dylib -dynamiclib api/dll/dll.o api/dll/gparams_register_modules.o api/dll/install_tactic.o api/dll/mem_initializer.o api/api_algebraic.o api/api_arith.o api/api_array.o api/api_ast.o api/api_ast_map.o api/api_ast_vector.o api/api_bv.o api/api_commands.o api/api_config_params.o api/api_context.o api/api_datalog.o api/api_datatype.o api/api_goal.o api/api_interp.o api/api_log.o api/api_log_macros.o api/api_model.o api/api_numeral.o api/api_params.o api/api_parsers.o api/api_polynomial.o api/api_quant.o api/api_rcf.o api/api_solver.o api/api_solver_old.o api/api_stats.o api/api_tactic.o api/api_user_theory.o api/z3_replayer.o parsers/smt/smtparser.a tactic/portfolio/portfolio.a tactic/ufbv/ufbv_tactic.a tactic/smtlogics/smtlogic_tactics.a muz/fp/fp.a muz/duality/duality_intf.a muz/bmc/bmc.a muz/tab/tab.a muz/clp/clp.a muz/pdr/pdr.a muz/rel/rel.a muz/transforms/transforms.a muz/base/muz.a duality/duality.a qe/qe.a tactic/sls/sls_tactic.a smt/tactic/smt_tactic.a tactic/fpa/fpa_tactics.a tactic/bv/bv_tactics.a smt/user_plugin/user_plugin.a smt/smt.a smt/proto_model/proto_model.a smt/params/smt_params.a ast/rewriter/bit_blaster/bit_blaster.a ast/pattern/pattern.a ast/macros/macros.a ast/fpa/fpa.a ast/simplifier/simplifier.a ast/proof_checker/proof_checker.a parsers/smt2/smt2parser.a cmd_context/extra_cmds/extra_cmds.a cmd_context/cmd_context.a interp/interp.a solver/solver.a tactic/aig/aig_tactic.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a tactic/arith/arith_tactics.a sat/tactic/sat_tactic.a tactic/core/core_tactics.a math/euclid/euclid.a math/grobner/grobner.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/rewriter/rewriter.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/interval/interval.a math/hilbert/hilbert.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a
ld: warning: could not create compact unwind for __Z15mk_qffpa_tacticR11ast_managerRK10params_ref: dwarf uses DW_CFA_GNU_args_size
ld: warning: could not create compact unwind for __Z15mk_qffpa_tacticR11ast_managerRK10params_ref: dwarf uses DW_CFA_GNU_args_size
ld: warning: could not create compact unwind for __ZN19elim_uncnstr_tactic3imp6rw_cfg17process_array_appEP9func_decljPKP4expr: dwarf uses DW_CFA_GNU_args_size
0  0x104b01b51  __assert_rtn + 144
1  0x104b29c99  mach_o::relocatable::Parser<x86_64>::parse(mach_o::relocatable::ParserOptions const&) + 3269
2  0x104b0d0fd  mach_o::relocatable::Parser<x86_64>::parse(unsigned char const*, unsigned long long, char const*, long, ld::File::Ordinal, mach_o::relocatable::ParserOptions const&) + 375
3  0x104b3d9cc  archive::File<x86_64>::makeObjectFileForMember(archive::File<x86_64>::Entry const*) const + 758
4  0x104b3d518  archive::File<x86_64>::justInTimeforEachAtom(char const*, ld::File::AtomHandler&) const + 122
5  0x104b5319b  ld::tool::InputFiles::searchLibraries(char const*, bool, bool, bool, ld::File::AtomHandler&) const + 215
6  0x104b5bc90  ld::tool::Resolver::resolveUndefines() + 160
7  0x104b5df63  ld::tool::Resolver::resolve() + 79
8  0x104b026c7  main + 689
A linker snapshot was created at:
    /tmp/libz3.dylib-2015-02-27-093218.ld-snapshot
ld: Assertion failed: (cfiStartsArray[i] != cfiStartsArray[i-1]), function parse, file /SourceCache/ld64/ld64-241.9/src/ld/parsers/macho_relocatable_file.cpp, line 1745.
clang: error: linker command failed with exit code 1 (use -v to see invocation)
Makefile:3514: recipe for target 'libz3.dylib' failed
gmake: *** [libz3.dylib] Error 1
gmake: *** Waiting for unfinished jobs....
0  0x10594fb51  __assert_rtn + 144
1  0x105977c99  mach_o::relocatable::Parser<x86_64>::parse(mach_o::relocatable::ParserOptions const&) + 3269
2  0x10595b0fd  mach_o::relocatable::Parser<x86_64>::parse(unsigned char const*, unsigned long long, char const*, long, ld::File::Ordinal, mach_o::relocatable::ParserOptions const&) + 375
3  0x10598b9cc  archive::File<x86_64>::makeObjectFileForMember(archive::File<x86_64>::Entry const*) const + 758
4  0x10598b518  archive::File<x86_64>::justInTimeforEachAtom(char const*, ld::File::AtomHandler&) const + 122
5  0x1059a119b  ld::tool::InputFiles::searchLibraries(char const*, bool, bool, bool, ld::File::AtomHandler&) const + 215
6  0x1059a9c90  ld::tool::Resolver::resolveUndefines() + 160
7  0x1059abf63  ld::tool::Resolver::resolve() + 79
8  0x1059506c7  main + 689
9  0x7fff8e0c85c9  start + 1
A linker snapshot was created at:
    /tmp/z3-2015-02-27-093218.ld-snapshot
ld: Assertion failed: (cfiStartsArray[i] != cfiStartsArray[i-1]), function parse, file /SourceCache/ld64/ld64-241.9/src/ld/parsers/macho_relocatable_file.cpp, line 1745.
clang: error: linker command failed with exit code 1 (use -v to see invocation)
Makefile:3197: recipe for target 'z3' failed
gmake: *** [z3] Error 1

The gcc build was with openmp, clang without. Both crashed in the same way, so it doesn't look openmp related.
Is this repro for you?

iZ3 - wrong interpolant

Here's another case where Z3 produces an incorrect interpolant (the
formula generated is not implied by A). I'm trying to understand what is
going on, but I haven't been able to identify the source of the problem
yet.

(set-logic QF_LRA)
(declare-fun t2.j.at2 () Real)
(declare-fun t1.i.at2 () Real)
(declare-fun t1.i.at1 () Real)
(declare-fun t1.k.at2 () Real)
(declare-fun t1.k.at1 () Real)
(declare-fun t1.loc_j.at2 () Real)
(declare-fun t1.loc_j.at1 () Real)
(declare-fun t2.j.at1 () Real)
(declare-fun t2.k.at2 () Real)
(declare-fun t2.k.at1 () Real)
(declare-fun t2.loc_i.at2 () Real)
(declare-fun t2.loc_i.at1 () Real)
(declare-fun t1.i.at0 () Real)
(declare-fun t1.k.at0 () Real)
(declare-fun t1.loc_j.at0 () Real)
(declare-fun t2.j.at0 () Real)
(declare-fun t2.k.at0 () Real)
(declare-fun t2.loc_i.at0 () Real)
(declare-fun t1.location.1.at2 () Bool)
(declare-fun t1.location.1.at1 () Bool)
(declare-fun t1.location.0.at2 () Bool)
(declare-fun t1.location.0.at1 () Bool)
(declare-fun t1.EVENT.0.at1 () Bool)
(declare-fun t2.EVENT.0.at1 () Bool)
(declare-fun t2.location.1.at2 () Bool)
(declare-fun t2.location.1.at1 () Bool)
(declare-fun t2.location.0.at2 () Bool)
(declare-fun t2.location.0.at1 () Bool)
(declare-fun t1.location.1.at0 () Bool)
(declare-fun t1.location.0.at0 () Bool)
(declare-fun t1.EVENT.0.at0 () Bool)
(declare-fun t2.EVENT.0.at0 () Bool)
(declare-fun t2.location.1.at0 () Bool)
(declare-fun t2.location.0.at0 () Bool)
;; A:
(define-fun .A () Bool
(let ((a!1 (not (and (= t2.k.at0 t2.k.at1)
                     (and (= t2.j.at0 t2.j.at1) (= t2.loc_i.at1 t2.loc_i.at0))
                     t2.location.1.at1
                     t2.location.0.at1)))
      (a!3 (and t2.EVENT.0.at0
                (and (not t2.location.0.at0) (not t2.location.1.at0))
                (not (<= 5 t2.k.at0))
                (not (and (= t2.k.at0 t2.k.at1)
                          (= t2.j.at0 t2.j.at1)
                          (= t1.i.at0 t2.loc_i.at1)
                          t2.location.1.at1
                          (not t2.location.0.at1)))))
      (a!4 (= (+ t2.j.at0 (* (- 1) t2.j.at1) t2.loc_i.at0) 0))
      (a!6 (= (+ t2.k.at0 (* (- 1) t2.k.at1)) (- 1)))
      (a!8 (not (and (not (and t2.location.0.at0 t2.location.0.at1))
                     (or t2.location.0.at0 t2.location.0.at1))))
      (a!9 (not (and (not (and t2.location.1.at0 t2.location.1.at1))
                     (or t2.location.1.at0 t2.location.1.at1))))
      (a!10 (and t1.EVENT.0.at0
                 (not (<= 5 t1.k.at0))
                 (and (not t1.location.0.at0) (not t1.location.1.at0))
                 (not (and (= t1.k.at0 t1.k.at1)
                           (= t1.i.at0 t1.i.at1)
                           (= t2.j.at0 t1.loc_j.at1)
                           t1.location.1.at1
                           (not t1.location.0.at1)))))
      (a!11 (= (+ t1.i.at0 (* (- 1) t1.i.at1) t1.loc_j.at0) 0))
      (a!13 (not (and (= t1.k.at0 t1.k.at1)
                      (and (= t1.i.at0 t1.i.at1) (= t1.loc_j.at1 t1.loc_j.at0))
                      t1.location.1.at1
                      t1.location.0.at1)))
      (a!15 (= (+ t1.k.at0 (* (- 1) t1.k.at1)) (- 1)))
      (a!17 (not (and (not (and t1.location.0.at0 t1.location.0.at1))
                      (or t1.location.0.at0 t1.location.0.at1))))
      (a!18 (not (and (not (and t1.location.1.at0 t1.location.1.at1))
                      (or t1.location.1.at0 t1.location.1.at1)))))
(let ((a!2 (not (and t2.EVENT.0.at0
                     (<= 5 t2.k.at0)
                     (and (not t2.location.0.at0) (not t2.location.1.at0))
                     a!1)))
      (a!5 (and t2.EVENT.0.at0
                (not t2.location.0.at0)
                t2.location.1.at0
                (not (and (= t2.k.at0 t2.k.at1)
                          (= t2.loc_i.at1 t2.loc_i.at0)
                          a!4
                          t2.location.0.at1
                          (not t2.location.1.at1)))))
      (a!7 (not (and a!6
                     (and (= t2.j.at0 t2.j.at1) (= t2.loc_i.at1 t2.loc_i.at0))
                     (not t2.location.0.at1)
                     (not t2.location.1.at1))))
      (a!12 (and t1.EVENT.0.at0
                 (not t1.location.0.at0)
                 t1.location.1.at0
                 (not (and (= t1.k.at0 t1.k.at1)
                           (= t1.loc_j.at1 t1.loc_j.at0)
                           a!11
                           t1.location.0.at1
                           (not t1.location.1.at1)))))
      (a!14 (not (and t1.EVENT.0.at0
                      (<= 5 t1.k.at0)
                      (and (not t1.location.0.at0) (not t1.location.1.at0))
                      a!13)))
      (a!16 (not (and a!15
                      (and (= t1.i.at0 t1.i.at1) (= t1.loc_j.at1 t1.loc_j.at0))
                      (not t1.location.0.at1)
                      (not t1.location.1.at1)))))
  (and true
       (= t1.i.at0 1)
       (= t1.k.at0 0)
       (not t1.location.0.at0)
       (not t1.location.1.at0)
       (= t2.j.at0 1)
       (= t2.k.at0 0)
       (not t2.location.0.at0)
       (not t2.location.1.at0)
       (<= t1.i.at0 144)
       (<= t2.j.at0 144)
       a!2
       (not a!3)
       (not a!5)
       (not (and t2.EVENT.0.at0 t2.location.0.at0 (not t2.location.1.at0) a!7))
       (not (and t2.EVENT.0.at0 a!1 t2.location.0.at0 t2.location.1.at0))
       (or t2.EVENT.0.at0
           (and (= t2.loc_i.at1 t2.loc_i.at0)
                (= t2.k.at0 t2.k.at1)
                (= t2.j.at0 t2.j.at1)
                a!8
                a!9))
       (not a!10)
       (not (and t1.EVENT.0.at0 t2.EVENT.0.at0))
       (or t1.EVENT.0.at0 t2.EVENT.0.at0)
       (not a!12)
       a!14
       (not (and t1.EVENT.0.at0 t1.location.0.at0 (not t1.location.1.at0) a!16))
       (not (and t1.EVENT.0.at0 a!13 t1.location.0.at0 t1.location.1.at0))
       (or t1.EVENT.0.at0
           (and (= t1.loc_j.at1 t1.loc_j.at0)
                (= t1.k.at0 t1.k.at1)
                (= t1.i.at0 t1.i.at1)
                a!17
                a!18))))))
;; B:
(define-fun .B () Bool
(let ((a!1 (not (and (= t2.k.at1 t2.k.at2)
                     (and (= t2.j.at1 t2.j.at2) (= t2.loc_i.at1 t2.loc_i.at2))
                     t2.location.1.at2
                     t2.location.0.at2)))
      (a!3 (and t2.EVENT.0.at1
                (and (not t2.location.0.at1) (not t2.location.1.at1))
                (not (<= 5 t2.k.at1))
                (not (and (= t2.k.at1 t2.k.at2)
                          (= t2.j.at1 t2.j.at2)
                          (= t1.i.at1 t2.loc_i.at2)
                          t2.location.1.at2
                          (not t2.location.0.at2)))))
      (a!4 (= (+ t2.j.at1 t2.loc_i.at1 (* (- 1) t2.j.at2)) 0))
      (a!6 (= (+ t2.k.at1 (* (- 1) t2.k.at2)) (- 1)))
      (a!8 (not (and (not (and t2.location.0.at1 t2.location.0.at2))
                     (or t2.location.0.at1 t2.location.0.at2))))
      (a!9 (not (and (not (and t2.location.1.at1 t2.location.1.at2))
                     (or t2.location.1.at1 t2.location.1.at2))))
      (a!10 (and t1.EVENT.0.at1
                 (and (not t1.location.0.at1) (not t1.location.1.at1))
                 (not (<= 5 t1.k.at1))
                 (not (and (= t1.k.at1 t1.k.at2)
                           (= t1.i.at1 t1.i.at2)
                           (= t2.j.at1 t1.loc_j.at2)
                           t1.location.1.at2
                           (not t1.location.0.at2)))))
      (a!11 (= (+ t1.i.at1 t1.loc_j.at1 (* (- 1) t1.i.at2)) 0))
      (a!13 (not (and (= t1.k.at1 t1.k.at2)
                      (and (= t1.i.at1 t1.i.at2) (= t1.loc_j.at1 t1.loc_j.at2))
                      t1.location.1.at2
                      t1.location.0.at2)))
      (a!15 (= (+ t1.k.at1 (* (- 1) t1.k.at2)) (- 1)))
      (a!17 (not (and (not (and t1.location.0.at1 t1.location.0.at2))
                      (or t1.location.0.at1 t1.location.0.at2))))
      (a!18 (not (and (not (and t1.location.1.at1 t1.location.1.at2))
                      (or t1.location.1.at1 t1.location.1.at2)))))
(let ((a!2 (not (and t2.EVENT.0.at1
                     (and (not t2.location.0.at1) (not t2.location.1.at1))
                     (<= 5 t2.k.at1)
                     a!1)))
      (a!5 (and t2.EVENT.0.at1
                t2.location.1.at1
                (not t2.location.0.at1)
                (not (and (= t2.k.at1 t2.k.at2)
                          (= t2.loc_i.at1 t2.loc_i.at2)
                          a!4
                          t2.location.0.at2
                          (not t2.location.1.at2)))))
      (a!7 (not (and a!6
                     (and (= t2.j.at1 t2.j.at2) (= t2.loc_i.at1 t2.loc_i.at2))
                     (not t2.location.0.at2)
                     (not t2.location.1.at2))))
      (a!12 (and t1.EVENT.0.at1
                 t1.location.1.at1
                 (not t1.location.0.at1)
                 (not (and (= t1.k.at1 t1.k.at2)
                           (= t1.loc_j.at1 t1.loc_j.at2)
                           a!11
                           t1.location.0.at2
                           (not t1.location.1.at2)))))
      (a!14 (not (and t1.EVENT.0.at1
                      (and (not t1.location.0.at1) (not t1.location.1.at1))
                      (<= 5 t1.k.at1)
                      a!13)))
      (a!16 (not (and a!15
                      (and (= t1.i.at1 t1.i.at2) (= t1.loc_j.at1 t1.loc_j.at2))
                      (not t1.location.0.at2)
                      (not t1.location.1.at2)))))
  (and true
       t2.location.1.at1
       (not t2.location.0.at1)
       (not t1.location.1.at1)
       (not t1.location.0.at1)
       (= t1.i.at1 1)
       (= t1.k.at1 0)
       (= t2.j.at1 1)
       (= t2.k.at1 0)
       (<= t1.i.at1 144)
       (<= t2.j.at1 144)
       a!2
       (not a!3)
       (not a!5)
       (not (and t2.EVENT.0.at1 t2.location.0.at1 (not t2.location.1.at1) a!7))
       (not (and t2.EVENT.0.at1 t2.location.1.at1 t2.location.0.at1 a!1))
       (or t2.EVENT.0.at1
           (and (= t2.loc_i.at1 t2.loc_i.at2)
                (= t2.k.at1 t2.k.at2)
                (= t2.j.at1 t2.j.at2)
                a!8
                a!9))
       (not a!10)
       (not (and t1.EVENT.0.at1 t2.EVENT.0.at1))
       (or t1.EVENT.0.at1 t2.EVENT.0.at1)
       (not a!12)
       a!14
       (not (and t1.EVENT.0.at1 t1.location.0.at1 (not t1.location.1.at1) a!16))
       (not (and t1.EVENT.0.at1 t1.location.1.at1 t1.location.0.at1 a!13))
       (or t1.EVENT.0.at1
           (and (= t1.loc_j.at1 t1.loc_j.at2)
                (= t1.k.at1 t1.k.at2)
                (= t1.i.at1 t1.i.at2)
                a!17
                a!18))
       (not (= t2.j.at2 1))
       (not (<= t2.j.at2 144))))))
;; interpolant computed:
(define-fun .I () Bool
(or (not (= 0 t2.k.at1))
    (not (= 1 t2.j.at1))
    (not (= 0 t1.k.at1))
    (not (= 1 t1.i.at1))))

(compute-interpolant (and (interp .A) .B))
(exit)

(push 1)
(assert (and .A (not .I)))
(check-sat)
(pop 1)
(exit)

Not sure if it's an error, but this is not working

from symbolic.args import *
@symbolic(a=0xdeaddeaddeaddead,b=beefbeefbeefbeef)

def expandKey(a,b):
i=0;
passkeyn=[a,b]

expandedkey=[]
while i<6:
    expandedkey=expandedkey+passkeyn
    i=i+1
    v1=passkeyn[0]
    v2=passkeyn[1]
    v3=(v1>>0x30)|(((v1>>0x20)&0xffff)<<0x10)|(((v1>>0x10)&0xffff)<<0x20)|((v1&0xffff)<<0x30)
    v4=(v2>>0x30)|(((v2>>0x20)&0xffff)<<0x10)|(((v2>>0x10)&0xffff)<<0x20)|((v2&0xffff)<<0x30)
    v5 = ((v4 & 0xFFFFFF8000000000) >> 39) | ((v3 << 25)&0xffffffffffffffff);
    v6 = ((v3 & 0xFFFFFF8000000000) >> 39) | ((v4 << 25)&0xffffffffffffffff);
    v1=(v5>>0x30)|(((v5>>0x20)&0xffff)<<0x10)|(((v5>>0x10)&0xffff)<<0x20)|(((v4 & 0xFFFFFF8000000000) >> 39)<<0x30)
    v2=(v6>>0x30)|(((v6>>32)&0xffff)<<0x10)|(((v6>>0x10)&0xffff)<<0x20)|(((v3 & 0xFFFFFF8000000000) >> 39)<<0x30)
    passkeyn=[v1,v2]
expandedkey=expandedkey+passkeyn
if expandedkey==[16045725885737590445, 13758425323549998831, 7044313620519854103485, 8215411798635391606653, 8245388070021240879798, 3384596836810669685695, 9287860625795901259255, 4527376222128629444341, 4093654381503457390331, 4647353382867023162077, 8665057901351565392853, 8816957627389395711965, 6783497306152038280055, 9291067819851303074799]:
    return 1
return 2

How does Z3 handle SMT-LIB scripts with absent set-logic command ?

It has been my experience that Z3 is able to work glitch-free with SMT-LIB scripts, even when they do not sport an initial (set-logic) command, even though this is mandated by the standard.

For example the minimal script below yields (correctly of course) unsat:

;;(set-logic QF_IDL)
(assert (< 2 1))
(check-sat)

What does Z3 do in such cases (they might be much more complicated) ? Does it try to infer the minimal logic needed ? Or does it load the most general capacities (such as treating AUFNIRA) and goes from there ?

resource limit in addition to time limit

Hello,

This is a request for a feature that would be very important for us to use Z3 with the SPARK tools (spark-2014.org).

The idea is a command-line option which allows to specify a "resource limit" instead of (or in addition to) currently available memory and time limits. The "resource" is just some internal counter, which gets increased in Z3 on specific deterministic moments, like finding a conflict or deciding on a literal or some such. When the counter hits the specified limit, Z3 stops just as it does when it hits the time or memory limit.

Such a limit allows to get reproducible behavior of a prover even under heavy load or across machines, sometimes even across platforms. This is essential for our nightly testing, and for users of our tools, for their nightly testing.

The two other SMT solvers we currently use, Alt-Ergo and CVC4, both have such an option: -steps-bound for Alt-Ergo, and --rlimit for CVC4. We have worked with the two development teams to improve these options - mostly finding time-intensive modules where the internal counter was not updated, basically allowing the prover to exceed the limit.

Or maybe there already is a way in Z3 to achieve what we want?

Thanks for considering this request.

Johannes

Receiving the value of an array

I am implementing a symbolic execution for fun using Z3(master branch) as the constraint solver. Since there is no "String" sort I am trying to implement strings using an integer array. However, I cannot figure out how to receive the value of the array.

(set-option :produce-models true)
(declare-const ia (Array Int Int))
(assert (= ia (store (store (store (store ((as const(Array Int Int)) 0) 0 99) 1 111) 2 111) 3 108)))
(check-sat)
(get-value (ia))
(get-model)

Result:

sat
((ia (_ as-array k!4)))
(model 
  (define-fun ia () (Array Int Int)
    (_ as-array k!4))
  (define-fun k!3 ((x!1 Int)) Int
    (ite (= x!1 2) 111
    (ite (= x!1 1) 111
    (ite (= x!1 0) 99
      0))))
  (define-fun k!0 ((x!1 Int)) Int
    0)
  (define-fun k!4 ((x!1 Int)) Int
    (ite (= x!1 3) 108
    (ite (= x!1 2) 111
    (ite (= x!1 1) 111
    (ite (= x!1 0) 99
      0)))))
  (define-fun k!1 ((x!1 Int)) Int
    (ite (= x!1 0) 99
      0))
  (define-fun k!2 ((x!1 Int)) Int
    (ite (= x!1 1) 111
    (ite (= x!1 0) 99
      0)))
)

(Since I am new to SMTLib) is it correct that I have to note what the output of get-value is and then look up the correct value through get-model? Is there an easier way to receive the value of the array? I could not find anything useful via Google besides the Z3 guide http://rise4fun.com/z3/tutorialcontent/guide

Also, since this is all new to me. Is this the correct way of implementing a constraint for a string? Is there an easier way of defining an array? I would really appreciate it if you have some guidance or reading material for me.

OCaml installation is broken

(follow up of https://z3.codeplex.com/discussions/473552 since codeplex doesn't want to let me add messages anymore)

So, the issue is that it was trying to use an outdated system z3 instead of the libz3.so installed through make ocamlfind_install. If I remove the system z3, it doesn't work anymore at all and can't find the libz3.so installed by make ocamlfind_install.

I wonder if you could produce only one .so containing everything, That would avoid the issue entirely.

Improve Python bindings

Hi!
I just played a little with the FP support in the unstable branch (in Python), and while doing so, I noticed some things that I think could be improved:

the fpTo* functions that convert FP values to something else return FPRefs instead of what they convert to. This is a problem because some functions and operators don't work correctly this way if for example both of their arguments are fpToIEEEBV(foo)
there are fpTo* functions that actually convert from something to FP (like fpToFPUnsigned) and the naming makes this pretty confusing (something like UBVToFp would be much clearer, mirroring fpToUBV)
this is mostly the expansion of the previous item; it would be nice if all the conversion functions would be consistently named.

That is all for now, If I notice anything else I'll add it. If I'm wrong about something, please do tell me :)

Segmentation fault using z3 fixedpoints in unstable

Z3 Version: 4.4.0
OS: Ubuntu 14.04 AMD64
git-commit: dd0d0a9

If the following is given to Z3 on stdin it will result in a segfault:

(declare-rel T (Int Real Int Real))
(declare-rel REACH (Int Real))
(declare-var x Int)
(declare-var c Real)
(declare-var nx Int)
(declare-var nc Real)
(declare-var delay Real)
(rule (! (=> (and (= x 0) (> c 2.0)) (T x c 1 c)) :named stepint))
(rule (! (=> (and (REACH x c) (T x c nx nc)) (REACH nx nc)) :named tstep))
(rule (! (=> (and (= c 0.0) (= x 0)) (REACH x c)) :named initialstates))
(rule (! (let ((a!1 (and (>= delay 0.0) (= nc (+ c delay)) (or (not (= x 0)) (< nc 5.0)))))
(=> a!1 (T x c x nc))) :named TICK))

(query (and (REACH x c) (= x 1) (= c 3.0))
:print-certificate true)

This same input works correctly (i.e., produces the expected result) if run on rise4fun.

Thanks.

P.S., If you have the time I have a related question on stackoverflow concerning z3's output on fixedpoint problems:

http://stackoverflow.com/questions/29704976/z3-fixedpoints-what-is-the-meaning-of-formula-false-in-model

format of model generated by z3

Hi,

Is there a documented grammar specification for the model generated by z3 on a satisfying instance ?

And thanks for releasing z3 under MIT license - its a great service to the community !

--Susmit

Segfault in fixpoint engine when built with g++-4.9.2

On at least the master, unstable, and opt branches, z3 segfaults on the following input when it is built with g++-4.9.2 on Debian Jessie for x86-64:

(declare-rel reach (Int Int))
(declare-var x Int)
(declare-var y Int)


(rule (reach x x))
(rule (=> (and (reach (div x 2) y) (= (mod x 2) 0)) (reach x y)))
(rule (=> (and (reach (+ (* x 3) 1) y) (= (mod x 2) 1)) (reach x y)))

(query (reach 3 1) :print-answer true)

Backtrace:

#0  0x00000000010947a3 in memory::deallocate(void*) ()
#1  0x00000000006d1777 in datalog::mk_slice::get_predicate_slice(func_decl*) ()
#2  0x00000000006d1f18 in datalog::mk_slice::init_vars(app*, bool, bool) ()
#3  0x00000000006d209b in datalog::mk_slice::init_vars(datalog::rule&) ()
#4  0x00000000006d2259 in datalog::mk_slice::prune_rule(datalog::rule&) ()
#5  0x00000000006d3cab in datalog::mk_slice::operator()(datalog::rule_set const&) ()
#6  0x000000000072e99b in datalog::rule_transformer::operator()(datalog::rule_set&)
    ()
#7  0x0000000000735236 in datalog::context::transform_rules(datalog::rule_transformer&) ()
#8  0x000000000058931c in pdr::dl_interface::query(expr*) ()
#9  0x00000000005386c4 in dl_query_cmd::execute(cmd_context&) ()
#10 0x0000000000b94276 in smt2::parser::parse_ext_cmd() ()
#11 0x0000000000b9548c in smt2::parser::operator()() ()
#12 0x0000000000b86178 in parse_smt2_commands(cmd_context&, std::istream&, bool, params_ref const&) ()
#13 0x0000000000422ee6 in read_smtlib2_commands(char const*) ()
#14 0x000000000040ded3 in main ()

However, if I compile z3 on Debian Wheezy with g++-4.7.2 and then copy the binary onto my Debian Jessie system and run it there with the same input, it works fine!

iZ3 - wrong interpolant from Farkas proof

Z3 computes a wrong interpolant for the example below.

I think this is due to the "rounding off" done in order to deal with
integer inequalities, which is performed regardless of whether the input
inequality is over the integer or over the rationals.

I'm also attaching a tentative patch for the issue.

Here's an SMT-LIB2 example showing the problem:

(set-logic QF_LRA)

(declare-fun x () Real)
(declare-fun y () Real)
(declare-fun z () Real)

(define-fun A () Bool
  (and
   (not (<= x 0.0))
   (>= (+ (* 10.0 y) (* (- 9.0) x)) 0.0)
   )
  )

(define-fun B () Bool
  (and (>= z 0.0)
       (<= (+ (* 10.0 y) (* 9.0 z)) 0.0))
  )

(compute-interpolant (and (interp A) B))
(exit)

;; computed wrong interpolant:
(define-fun I () Bool
  (>= y (/ 9.0 10.0)))
;; a correct interpolant is: (not (<= y 0.0))

(assert (or (and A (not I)) (and B I)))
(check-sat)

Here's a tentative patch:

diff --git a/src/interp/iz3proof_itp.cpp b/src/interp/iz3proof_itp.cpp
--- a/src/interp/iz3proof_itp.cpp
+++ b/src/interp/iz3proof_itp.cpp
@@ -2590,6 +2590,9 @@
         if(pstrict && qstrict && round_off)
             Qrhs = make(Sub,Qrhs,make_int(rational(1)));
 #else
+        if (round_off && get_type(Qrhs) != int_type()) {
+            round_off = false;
+        }
         bool pstrict = op(P) == Lt;
         if(qstrict && round_off && (pstrict || !(c == make_int(rational(1))))){
             Qrhs = make(Sub,Qrhs,make_int(rational(1)));

iZ3 - Segmentation fault

I found that Z3 segfaults on the following input

(set-option :produce-interpolants true)
(declare-fun a () Int)
(declare-fun b () Int)
(declare-fun c () Int)
(declare-fun d () Int)
(declare-fun e () Int)
(declare-fun f () Int)
(declare-fun g () Int)
(declare-fun h () Int)
(declare-fun i () Int)
(declare-fun j () (Array Int Int))
(declare-fun k () (Array Int Int))
(declare-fun l () (Array Int Int))
(declare-fun m () (Array Int Int))
(declare-fun n () (Array Int Int))
(declare-fun o () (Array Int (Array Int Int)))
(declare-fun p () (Array Int (Array Int Int)))
(push 1)
  (assert (! (< (select l g) 0) :named g0))
  (assert (! (= m (store j g 0)) :named g1))
  (assert (! (= p (store o (select n i) (store (select o (select n i)) 1 d))) :named g2))
  (assert (! (= f h) :named g3))
  (assert (! (= b 0) :named g4))
  (assert (! (= c (select (select p (select n f)) b)) :named g5))
  (assert (! (= a (select k c)) :named g6))
  (assert (! (= e (+ a 1)) :named g7))
  (assert (! (not (< (select m c) e)) :named g8))
  (assert (! (let ((a!1 (= d (select (select o (select n i)) 0)))) (and (= k (store l g 0)) (forall ((%0 Int) (%1 Int)) (! (let ((a!1 (= d (select (select o (select n i)) 0))) (a!2 (= (select (select o (select n i)) 0) %1)) (a!3 (<= (+ (select j %1) (* (- 1) (select l %0))) 0)) (a!6 (= %0 (select (select o (select n i)) 0)))) (let ((a!4 (or (not (or (not a!2) a!3)))) (a!8 (not (or a!1 (not (= d %0)))))) (let ((a!5 (or a!1 a!4))) (let ((a!7 (or (not (or (not a!5) (not a!6))) (not (= h i))))) (or (not a!7) a!8))))) :pattern ((select l %0) (select j %1)) :qid itp)))) :named g9))
  (compute-interpolant (and g1 g9) (and g0 g2 g3 g4 g5 g6 g7 g8))
(pop 1)

What are the prerequisites to build z3?

I know of: python (is it a specific version we need?), a c++ compiler, make.
Are there any others I should know about?
Any library for example?
I am trying to create an opam (a source-based installer for OCaml programs) package for z3 so I should know.
Thanks a lot,
F.

valid_assignment() assertion violation

To get a better feeing for z3 I wanted to do constraint-based layouting.
https://gist.github.com/daniel-j-h/499c50455929ab6aa755

Surprisingly though, I stumbled upon a strange assertion.
This is triggered only when I set the enclosing box to a resolution of 1366,768 and use the area function (i.e. multiplication). Setting the box to 1365,768 or switching the area constraint with width and height constraints does give me a valid model.

ASSERTION VIOLATION
File: ../src/smt/theory_arith_aux.h
Line: 1996
valid_assignment()
(C)ontinue, (A)bort, (S)top, (T)hrow exception, Invoke (G)DB
A

I could only trace it back to theory_arith_inv.h's valid_assignment, and then satisfy_integrality. I can see no reason why this assertion could happen. Would you be so kind and have a look at it? Is the multiplication the problem? As far as I read the Ints theory spec, there is an (* Int Int Int :left-assoc) symbol.

This is tested with

Z3 [version 4.4.0 - 64 bit - build hashcode bd162588b28c1ca38980bfd0df040539df176370].

and also with the latest (as of now)

Z3 [version 4.4.0 - 64 bit - build hashcode 3ba2e712b21bb5c8e987243c118adbd8b30b185d]

Thanks,
Daniel

Simulating a parse-only mode with Z3 for SMT-LIB v2

This is not a bug and more a want for explanation. If there is a better medium fot that kind of exchange (e-mail?), please feel free to indicate it.

I am running some benchmarks on various tools about SMT-LIB. One of the measuring stick is of course Z3. I am mostly interested as of now in the parsing time / AST construction.

Am I mistaken if I say that I can simulate/approximate a parse-only mode for Z3/SMT-LIB v2 by commenting line 2017 in src/parsers/smt2/smt2parser.cpp ? This is this line:

m_ctx.check_sat(expr_stack().size() - spos, expr_stack().c_ptr() + spos);

I am trying to not trigger the SMT solving engine of Z3 and just have something close to simple AST construction.

Use of InterpolationContext in Java causes JVM SIGSEGV

I was trying to use the Java interpolation API from z3-unstable to construct some simple examples. Unfortunately using an InterpolationContext crashes the JVM. Here is the offending code:

System.out.print("Z3 Major Version: ");
System.out.println(Version.getMajor());
System.out.print("Z3 Full Version: ");
System.out.println(Version.getString());

HashMap<String, String> cfg = new HashMap<String, String>();
InterpolationContext ictx = new InterpolationContext(cfg);
System.out.println("SimpleInterpExample1");
IntExpr x = ictx.mkIntConst("x"); //Causes SIGSEGV in JVM

Here is the JVM output:

Z3 Major Version: 4
Z3 Full Version: 4.4.0.0
SimpleInterpExample1

A fatal error has been detected by the Java Runtime Environment:

SIGSEGV (0xb) at pc=0x00007f712b0098c2, pid=19251, tid=140124041512704

JRE version: Java(TM) SE Runtime Environment (8.0_31-b13) (build 1.8.0_31-b13)
Java VM: Java HotSpot(TM) 64-Bit Server VM (25.31-b07 mixed mode linux-amd64 compressed oops)
Problematic frame:
C [libc.so.6+0x7e8c2]# [ timer expired, abort... ]

The rest of the Java Z3 API seems to work fine in the unstable branch: All the examples in JavaExample.java work.

Any ideas on what the issue could be?

sorts inhabited by default?

Hi all,

on the VC below Z3 answers "unsat" although one could argue that it's not ... the critical question is whether sorts are always inhabited or not. Clearly Z3 assumes that yes, but the SMTlib standard doesn't say anything about this as far as I can see. And other SMT-solvers (I tried CVC4 and Alt-ergo) don't exploit this.

So what is your opinion on this? Thanks in advance,

Johannes

================ VC below ===================

(declare-sort t 0)

(define-fun in_range ((x Int)) Bool (and (<= 1 x) (<= x 0)))

(declare-fun to_rep (t) Int)

;; range_axiom
(assert (forall ((x t)) (in_range (to_rep x))))

(check-sat)

nuZ's minimized result does not match get-model's model

How can be that the minimize command returns a value that is not possible with the result from get-model? Or: how do I get a model for the minimized result?

In this example, minimize returns: 46 as (correctly) minimized result:
https://gist.github.com/daniel-j-h/1d661f6a7e299a47725f

But once I try to generate a model, i.e. using get-model or eval, the output is different.
In this case, the output is 83 for the model (take a look at the output; first line is minimized result, 6th line is actual schedule, from 0 to 83). The model is not the optimal one, as you can clearly see from the schedule and for example at the time from 3 to 38 where nothing is done.

Is this the correct behavior? Is it due to me not using soft-constraints for the intervals to be optimized?
Could you give a quick explanation how something like this could happen at all?

Thanks,
Daniel

iZ3 - Segmentation faults

We use Z3 with the C interface as a library inside CPAchecker (for solving and interpolation). We have several cases where Z3 segfaults. Here are Z3 logfiles for three of them:

http://students.fim.uni-passau.de/~wendler/Problem14_label50_true-unreach-call.c.z3.log.bz2
http://students.fim.uni-passau.de/~wendler/elevator_spec13_product23_true-unreach-call.cil.c.z3.log.bz2
http://students.fim.uni-passau.de/~wendler/s3_srvr_8_true-unreach-call.cil.c.z3.log.bz2

When replaying, each of the log files gives the message "invalid pointer", thus it seems like a bug in Z3 to us.
The Z3 version used was 7f6ef0b.

Enhancement: Use operator overloading in the .NET API

Instead of MkAnd the .NET API should use operator overloading to support && instead.
Instead of MkLE the .NET API should support >=
...

This would make my code much easier to read.

Could you tag the software?

So that people can package it for source-based package managers.

Z3_get_interpolant fails (always returns "true")

This bug is caused by not collecting the assertions from the solver or proof, which had the side effect of treating all assertions in the pattern as "background".

Opt-branch, incorrectly returns "infinity"

For the following query:

(declare-fun |main::k@2| () Int)
(declare-fun |main::k@3| () Int)
(declare-fun |main::n@3| () Int)
(declare-fun |main::j@2| () Int)
(declare-fun |main::j@3| () Int)
(assert (and
    (<= (* (- 1) |main::k@2|) 0)
    (<= |main::k@2| 1)
    (<= (+ (+ (* (- 1) |main::j@2|) (* (- 1) |main::k@2|)) |main::n@3|) 0)
    (= |main::k@3| (+ (- 1) |main::k@2|))
    (= |main::j@3| (+ 1 |main::j@2|))
))

(maximize (+ (* (- 1) |main::j@3|) (* (- 1) |main::k@3|) |main::n@3|))
(set-option :opt.optsmt_engine basic)
(set-option :opt.priority box)
(check-sat)

I get the bound "oo".

What's more interesting, if we drop the constraints 0 <= k@2 <= 1 opt-Z3 correctly returns a bound of 0.

Not installable via `pip` or `easy_install`

It seems that it should not be impossible for Z3 to be available in an automatable, one-click manner via PyPI. Native libraries and extensions can be built on-target for all operating systems, Linux and OSX being the easiest among them.

Are there any plans to make Z3 available via PyPI?

Interpolation queries after check-sat, push, pop

Hello,

is it expected, that Z3 produces different outputs for the attached smt2 inputs, which differ in placement of "(check-sat)", "(push 1)(pop 1)"?

Input 1:

(set-option :produce-interpolants true)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(assert (! (= x1 0) :named g0))
(assert (! (= x2 (+ x1 1)) :named g1))
(assert (! (= x2 2) :named g2))

; Nothing

(assert (! (= x2 1) :named g3))
(push 1)
  (check-sat)
  (get-interpolant g3 g2)
(pop 1)
(exit)

Input 2:

(set-option :produce-interpolants true)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(assert (! (= x1 0) :named g0))
(assert (! (= x2 (+ x1 1)) :named g1))
(assert (! (= x2 2) :named g2))

(push 1)
(pop 1)

(assert (! (= x2 1) :named g3))
(push 1)
  (check-sat)
  (get-interpolant g3 g2)
(pop 1)
(exit)

Input 3:

(set-option :produce-interpolants true)
(declare-fun x1 () Int)
(declare-fun x2 () Int)
(assert (! (= x1 0) :named g0))
(assert (! (= x2 (+ x1 1)) :named g1))
(assert (! (= x2 2) :named g2))

(check-sat)

(assert (! (= x2 1) :named g3))
(push 1)
  (check-sat)
  (get-interpolant g3 g2)
(pop 1)
(exit)

Missing code in complex.py example

Not sure if this is correct (it surely doesn't run for me as-is), but the complex.py code example is missing the body for the function pow @ line 69. I'd certainly love to provide a fix for this, but I have no clue what goes here :)

Possible wrong answer in QF_BV

On problem https://gist.github.com/dddejan/89f6b9d3bc8084438178

z3: sat
yices2: unsat
cvc4: unsat

compile error Visual Studio 2008 Windows 7 32 bit

Getting a build error on Windows 7 32 bit machine.

>nmake

Microsoft (R) Program Maintenance Utility Version 9.00.30729.01
Copyright (C) Microsoft Corporation.  All rights reserved.

api_interp.cpp
z3-master\src\interp\iz3mgr.h(133) : error C2143: syntax error : missing ';' before '<'
z3-master\src\interp\iz3mgr.h(133) : error C2913: explicit specialization; 'std::less' is not a specialization of a class template
z3-master\src\interp\iz3mgr.h(133) : error C2059: syntax error : '<'
z3-master\src\interp\iz3mgr.h(133) : error C2143: syntax error : missing ';' before '{'
z3-master\src\interp\iz3mgr.h(133) : error C2447: '{' : missing function header (old-style formal list?)
NMAKE : fatal error U1077: '"\Programs\Common\Microsoft\Visual C++ for Python\9.0\VC\Bin\cl.EXE"' : return code '0x2'
Stop.

z3py's Solver.check does not accept assumptions

>>> import z3
>>> solver = z3.Solver()
>>> x = z3.Int('x')
>>> solver.add(x == 0)
>>> solver.check()  # works
sat
>>> solver.check(x == 0)  # fails
WARNING: an assumption must be a propositional variable or the negation of one
unknown

I observed it both in binary release of 4.3.2 on windows with python 2.7 and in recent linux build of unstable branch at 6c1a539 with python 3.4.

Compile error Visual Studio 2010

Took sources revision ac21ffe

d:\z3-master>c:\python27\python scripts/mk_make.py
New component: 'util'
New component: 'polynomial'
New component: 'sat'
New component: 'nlsat'
New component: 'hilbert'
New component: 'interval'
New component: 'realclosure'
New component: 'subpaving'
New component: 'ast'
New component: 'rewriter'
New component: 'normal_forms'
New component: 'model'
New component: 'tactic'
New component: 'substitution'
New component: 'parser_util'
New component: 'grobner'
New component: 'euclid'
New component: 'core_tactics'
New component: 'sat_tactic'
New component: 'arith_tactics'
New component: 'nlsat_tactic'
New component: 'subpaving_tactic'
New component: 'aig_tactic'
New component: 'solver'
New component: 'interp'
New component: 'cmd_context'
New component: 'extra_cmds'
New component: 'smt2parser'
New component: 'proof_checker'
New component: 'simplifier'
New component: 'fpa'
New component: 'macros'
New component: 'pattern'
New component: 'bit_blaster'
New component: 'smt_params'
New component: 'proto_model'
New component: 'smt'
New component: 'user_plugin'
New component: 'bv_tactics'
New component: 'fuzzing'
New component: 'fpa_tactics'
New component: 'smt_tactic'
New component: 'sls_tactic'
New component: 'qe'
New component: 'duality'
New component: 'muz'
New component: 'transforms'
New component: 'rel'
New component: 'pdr'
New component: 'clp'
New component: 'tab'
New component: 'bmc'
New component: 'duality_intf'
New component: 'fp'
New component: 'smtlogic_tactics'
New component: 'ufbv_tactic'
New component: 'portfolio'
New component: 'smtparser'
New component: 'api'
New component: 'shell'
New component: 'test'
New component: 'api_dll'
New component: 'dotnet'
New component: 'java'
New component: 'cpp'
Python bindings directory was detected.
New component: 'cpp_example'
New component: 'iz3'
New component: 'z3_tptp'
New component: 'c_example'
New component: 'maxsat'
New component: 'dotnet_example'
New component: 'java_example'
New component: 'py_example'
Generated 'src\util\version.h'
Updated 'src\api\dotnet\Properties\AssemblyInfo'
Generated 'src\api\dll\api_dll.def'
Generated 'src\ast\pp_params.hpp'
Generated 'src\ast\normal_forms\nnf_params.hpp'
Generated 'src\ast\pattern\pattern_inference_params_helper.hpp'
Generated 'src\ast\rewriter\arith_rewriter_params.hpp'
Generated 'src\ast\rewriter\array_rewriter_params.hpp'
Generated 'src\ast\rewriter\bool_rewriter_params.hpp'
Generated 'src\ast\rewriter\bv_rewriter_params.hpp'
Generated 'src\ast\rewriter\poly_rewriter_params.hpp'
Generated 'src\ast\rewriter\rewriter_params.hpp'
Generated 'src\ast\simplifier\arith_simplifier_params_helper.hpp'
Generated 'src\ast\simplifier\array_simplifier_params_helper.hpp'
Generated 'src\ast\simplifier\bv_simplifier_params_helper.hpp'
Generated 'src\interp\interp_params.hpp'
Generated 'src\math\polynomial\algebraic_params.hpp'
Generated 'src\math\realclosure\rcf_params.hpp'
Generated 'src\model\model_evaluator_params.hpp'
Generated 'src\model\model_params.hpp'
Generated 'src\muz\base\fixedpoint_params.hpp'
Generated 'src\nlsat\nlsat_params.hpp'
Generated 'src\parsers\util\parser_params.hpp'
Generated 'src\sat\sat_asymm_branch_params.hpp'
Generated 'src\sat\sat_params.hpp'
Generated 'src\sat\sat_scc_params.hpp'
Generated 'src\sat\sat_simplifier_params.hpp'
Generated 'src\smt\params\smt_params_helper.hpp'
Generated 'src\solver\combined_solver_params.hpp'
Generated 'src\tactic\sls\sls_params.hpp'
Generated 'src\ast\pattern\database.h'
Generated 'src\shell\install_tactic.cpp'
Generated 'src\test\install_tactic.cpp'
Generated 'src\api\dll\install_tactic.cpp'
Generated 'src\shell\mem_initializer.cpp'
Generated 'src\test\mem_initializer.cpp'
Generated 'src\api\dll\mem_initializer.cpp'
Generated 'src\shell\gparams_register_modules.cpp'
Generated 'src\test\gparams_register_modules.cpp'
Generated 'src\api\dll\gparams_register_modules.cpp'
Generated 'src\api\python\z3consts.py'
Generated 'src\api\dotnet\Enumerations.cs'
Generated 'src\api\api_log_macros.h'
Generated 'src\api\api_log_macros.cpp'
Generated 'src\api\api_commands.cpp'
Generated 'src\api\python\z3core.py'
Generated 'src\api\dotnet\Native.cs'
Listing src\api\python ...
Compiling src\api\python\z3.py ...
Compiling src\api\python\z3consts.py ...
Compiling src\api\python\z3core.py ...
Compiling src\api\python\z3num.py ...
Compiling src\api\python\z3poly.py ...
Compiling src\api\python\z3printer.py ...
Compiling src\api\python\z3rcf.py ...
Compiling src\api\python\z3test.py ...
Compiling src\api\python\z3types.py ...
Compiling src\api\python\z3util.py ...
Copied 'z3.py'
Copied 'z3consts.py'
Copied 'z3core.py'
Copied 'z3num.py'
Copied 'z3poly.py'
Copied 'z3printer.py'
Copied 'z3rcf.py'
Copied 'z3test.py'
Copied 'z3types.py'
Copied 'z3util.py'
Generated 'z3.pyc'
Generated 'z3consts.pyc'
Generated 'z3core.pyc'
Generated 'z3num.pyc'
Generated 'z3poly.pyc'
Generated 'z3printer.pyc'
Generated 'z3rcf.pyc'
Generated 'z3test.pyc'
Generated 'z3types.pyc'
Generated 'z3util.pyc'
64-bit: True
Writing build\Makefile
Copied Z3Py example 'example.py' to 'build'
Makefile was successfully generated.
compilation mode: Release
platform: x86
To build Z3, open a [Visual Studio Command Prompt], then
type 'cd d:\z3-master\build && nmake'

Remark: to open a Visual Studio Command Prompt, go to: "Start > All Programs > V
isual Studio > Visual Studio Tools"

d:\z3-master>cd d:\z3-master\build && nmake

gparams_register_modules.cpp
d:\z3-master\src\util\z3_omp.h(23) : fatal error C1083: Cannot open include file
: 'omp.h': No such file or directory
NMAKE : fatal error U1077: '"C:\Program Files (x86)\Microsoft Visual Studio 10.0
\VC\BIN\cl.EXE"' : return code '0x2'
Stop.

d:\z3-master\build>

fp.isSubnormal is buggy

This is on the unstable branch.

The following benchmark:

(set-option :produce-models true)
(set-logic QF_FP)
(declare-fun s0 () (_ FloatingPoint 11 53))
(assert
   (let ((s1 (fp.isSubnormal s0)))
   s1))
(check-sat)
(get-value (s0))

Results in:

sat
((s0 (_ +zero 11 53)))

which suggests +0 is a sub-normal number, which isn't true.

Nonterminating with QF_LIA, Success with LIA

On the following script z3 d01c349 does not terminate. After changing the logic to (the more difficult!) LIA I obtain a result within a second.

(set-option :produce-models true)
(set-option :produce-unsat-cores true)
(set-logic QF_LIA)
(set-info :source |
    SMT script generated on 2015/04/26 by Ultimate. http://ultimate.informatik.uni-freiburg.de/
|)
(set-info :smt-lib-version 2.0)
(set-info :category "industrial")
(declare-fun |c___VERIFIER_nondet_int_#res| () Int)
(declare-fun |c___VERIFIER_nondet_int_#res_primed| () Int)
(declare-fun |c___VERIFIER_assert_#in~cond| () Int)
(declare-fun |c___VERIFIER_assert_#in~cond_primed| () Int)
(declare-fun c___VERIFIER_assert_~cond () Int)
(declare-fun c___VERIFIER_assert_~cond_primed () Int)
(declare-fun |c_main_#t~nondet0| () Int)
(declare-fun |c_main_#t~nondet0_primed| () Int)
(declare-fun |c_main_#t~nondet1| () Int)
(declare-fun |c_main_#t~nondet1_primed| () Int)
(declare-fun |c_main_#t~nondet2| () Int)
(declare-fun |c_main_#t~nondet2_primed| () Int)
(declare-fun c_main_~x~5 () Int)
(declare-fun c_main_~x~5_primed () Int)
(declare-fun c_main_~y~5 () Int)
(declare-fun c_main_~y~5_primed () Int)
(declare-fun c_main_~z~5 () Int)
(declare-fun c_main_~z~5_primed () Int)
(declare-fun main_~x~5_4 () Int)
(declare-fun main_~y~5_4 () Int)
(declare-fun main_~z~5_4 () Int)
(declare-fun |main_#t~nondet0_3| () Int)
(declare-fun |main_#t~nondet2_3| () Int)
(declare-fun |main_#t~nondet1_3| () Int)
(declare-fun |main_#t~nondet0_6| () Int)
(declare-fun main_~x~5_6 () Int)
(declare-fun main_~y~5_6 () Int)
(declare-fun main_~z~5_6 () Int)
(declare-fun |main_#t~nondet2_6| () Int)
(declare-fun |main_#t~nondet1_6| () Int)
(declare-fun |__VERIFIER_assert_#in~cond_7| () Int)
(declare-fun __VERIFIER_assert_~cond_8 () Int)
(declare-fun |main_#t~nondet0_13| () Int)
(declare-fun main_~x~5_13 () Int)
(declare-fun main_~y~5_13 () Int)
(declare-fun main_~z~5_13 () Int)
(declare-fun |main_#t~nondet2_13| () Int)
(declare-fun |main_#t~nondet1_13| () Int)
(declare-fun |__VERIFIER_assert_#in~cond_14| () Int)
(declare-fun __VERIFIER_assert_~cond_15 () Int)
(declare-fun |main_#t~nondet0_20| () Int)
(declare-fun main_~x~5_20 () Int)
(declare-fun main_~y~5_20 () Int)
(declare-fun main_~z~5_20 () Int)
(declare-fun |main_#t~nondet2_20| () Int)
(declare-fun |main_#t~nondet1_20| () Int)
(declare-fun |__VERIFIER_assert_#in~cond_21| () Int)
(declare-fun __VERIFIER_assert_~cond_22 () Int)
(declare-fun |main_#t~nondet0_27| () Int)
(declare-fun main_~x~5_27 () Int)
(declare-fun main_~y~5_27 () Int)
(declare-fun main_~z~5_27 () Int)
(declare-fun |main_#t~nondet2_27| () Int)
(declare-fun |main_#t~nondet1_27| () Int)
(declare-fun |__VERIFIER_assert_#in~cond_28| () Int)
(declare-fun __VERIFIER_assert_~cond_29 () Int)
(declare-fun |main_#t~nondet0_34| () Int)
(declare-fun main_~x~5_34 () Int)
(declare-fun main_~y~5_34 () Int)
(declare-fun main_~z~5_34 () Int)
(declare-fun |main_#t~nondet2_34| () Int)
(declare-fun |main_#t~nondet1_34| () Int)
(declare-fun |__VERIFIER_assert_#in~cond_35| () Int)
(declare-fun __VERIFIER_assert_~cond_36 () Int)
(declare-fun |main_#t~nondet0_41| () Int)
(declare-fun main_~x~5_41 () Int)
(declare-fun main_~y~5_41 () Int)
(declare-fun main_~z~5_41 () Int)
(declare-fun |main_#t~nondet2_41| () Int)
(declare-fun |main_#t~nondet1_41| () Int)
(declare-fun |__VERIFIER_assert_#in~cond_42| () Int)
(declare-fun __VERIFIER_assert_~cond_43 () Int)
(declare-fun |main_#t~nondet0_48| () Int)
(declare-fun main_~x~5_48 () Int)
(declare-fun main_~y~5_48 () Int)
(declare-fun main_~z~5_48 () Int)
(declare-fun |main_#t~nondet2_48| () Int)
(declare-fun |main_#t~nondet1_48| () Int)
(declare-fun |__VERIFIER_assert_#in~cond_49| () Int)
(declare-fun __VERIFIER_assert_~cond_50 () Int)
(declare-fun |main_#t~nondet0_55| () Int)
(declare-fun main_~x~5_55 () Int)
(declare-fun main_~y~5_55 () Int)
(declare-fun main_~z~5_55 () Int)
(declare-fun |main_#t~nondet2_55| () Int)
(declare-fun |main_#t~nondet1_55| () Int)
(declare-fun |__VERIFIER_assert_#in~cond_56| () Int)
(declare-fun __VERIFIER_assert_~cond_57 () Int)
(declare-fun |main_#t~nondet0_62| () Int)
(declare-fun main_~x~5_62 () Int)
(declare-fun main_~y~5_62 () Int)
(declare-fun main_~z~5_62 () Int)
(declare-fun |main_#t~nondet2_62| () Int)
(declare-fun |main_#t~nondet1_62| () Int)
(declare-fun |__VERIFIER_assert_#in~cond_63| () Int)
(declare-fun __VERIFIER_assert_~cond_64 () Int)
(declare-fun |main_#t~nondet0_69| () Int)
(declare-fun main_~x~5_69 () Int)
(declare-fun main_~y~5_69 () Int)
(declare-fun main_~z~5_69 () Int)
(declare-fun |main_#t~nondet2_69| () Int)
(declare-fun |main_#t~nondet1_69| () Int)
(declare-fun |__VERIFIER_assert_#in~cond_70| () Int)
(declare-fun __VERIFIER_assert_~cond_71 () Int)
(assert (! true :named ssa_precond_conjunct0))
(assert (! (not false) :named ssa_postcond))
(assert (! true :named ssa_0_GlobVarAssigCall_conjunct0))
(assert (! true :named ssa_0_LocVarAssigCall_conjunct0))
(assert (! true :named ssa_0_OldVarAssigCall_conjunct0))
(assert (! true :named ssa_1_conjunct0))
(assert (! true :named ssa_2_return_conjunct0))
(assert (! true :named ssa_3_GlobVarAssigCall_conjunct0))
(assert (! true :named ssa_3_LocVarAssigCall_conjunct0))
(assert (! true :named ssa_3_OldVarAssigCall_conjunct0))
(assert (! (<= main_~x~5_4 0) :named ssa_4_conjunct0))
(assert (! (>= main_~x~5_4 0) :named ssa_4_conjunct1))
(assert (! (<= main_~y~5_4 0) :named ssa_4_conjunct2))
(assert (! (>= main_~y~5_4 0) :named ssa_4_conjunct3))
(assert (! (<= main_~z~5_4 0) :named ssa_4_conjunct4))
(assert (! (>= main_~z~5_4 0) :named ssa_4_conjunct5))
(assert (! true :named ssa_5_conjunct0))
(assert (! (<= main_~x~5_6 (+ main_~x~5_4 (* 2 |main_#t~nondet0_3|))) :named ssa_6_conjunct0))
(assert (! (>= main_~x~5_6 (+ main_~x~5_4 (* 2 |main_#t~nondet0_3|))) :named ssa_6_conjunct1))
(assert (! (<= main_~y~5_6 (+ main_~y~5_4 (* 4 |main_#t~nondet1_3|))) :named ssa_6_conjunct2))
(assert (! (>= main_~y~5_6 (+ main_~y~5_4 (* 4 |main_#t~nondet1_3|))) :named ssa_6_conjunct3))
(assert (! (<= main_~z~5_6 (+ main_~z~5_4 (* 8 |main_#t~nondet2_3|))) :named ssa_6_conjunct4))
(assert (! (>= main_~z~5_6 (+ main_~z~5_4 (* 8 |main_#t~nondet2_3|))) :named ssa_6_conjunct5))
(assert (! true :named ssa_7_GlobVarAssigCall_conjunct0))
(assert (! (<= |__VERIFIER_assert_#in~cond_7| (ite (not (= (+ (+ (* 4 main_~x~5_6) (* 2 main_~y~5_6)) main_~z~5_6) 4)) 1 0)) :named ssa_7_LocVarAssigCall_conjunct0))
(assert (! (>= |__VERIFIER_assert_#in~cond_7| (ite (not (= (+ (+ (* 4 main_~x~5_6) (* 2 main_~y~5_6)) main_~z~5_6) 4)) 1 0)) :named ssa_7_LocVarAssigCall_conjunct1))
(assert (! true :named ssa_7_OldVarAssigCall_conjunct0))
(assert (! (<= __VERIFIER_assert_~cond_8 |__VERIFIER_assert_#in~cond_7|) :named ssa_8_conjunct0))
(assert (! (>= __VERIFIER_assert_~cond_8 |__VERIFIER_assert_#in~cond_7|) :named ssa_8_conjunct1))
(assert (! (not (= __VERIFIER_assert_~cond_8 0)) :named ssa_9_conjunct0))
(assert (! true :named ssa_10_conjunct0))
(assert (! true :named ssa_11_return_conjunct0))
(assert (! true :named ssa_12_conjunct0))
(assert (! (<= main_~x~5_13 (+ main_~x~5_6 (* 2 |main_#t~nondet0_6|))) :named ssa_13_conjunct0))
(assert (! (>= main_~x~5_13 (+ main_~x~5_6 (* 2 |main_#t~nondet0_6|))) :named ssa_13_conjunct1))
(assert (! (<= main_~y~5_13 (+ main_~y~5_6 (* 4 |main_#t~nondet1_6|))) :named ssa_13_conjunct2))
(assert (! (>= main_~y~5_13 (+ main_~y~5_6 (* 4 |main_#t~nondet1_6|))) :named ssa_13_conjunct3))
(assert (! (<= main_~z~5_13 (+ main_~z~5_6 (* 8 |main_#t~nondet2_6|))) :named ssa_13_conjunct4))
(assert (! (>= main_~z~5_13 (+ main_~z~5_6 (* 8 |main_#t~nondet2_6|))) :named ssa_13_conjunct5))
(assert (! true :named ssa_14_GlobVarAssigCall_conjunct0))
(assert (! (<= |__VERIFIER_assert_#in~cond_14| (ite (not (= (+ (+ (* 4 main_~x~5_13) (* 2 main_~y~5_13)) main_~z~5_13) 4)) 1 0)) :named ssa_14_LocVarAssigCall_conjunct0))
(assert (! (>= |__VERIFIER_assert_#in~cond_14| (ite (not (= (+ (+ (* 4 main_~x~5_13) (* 2 main_~y~5_13)) main_~z~5_13) 4)) 1 0)) :named ssa_14_LocVarAssigCall_conjunct1))
(assert (! true :named ssa_14_OldVarAssigCall_conjunct0))
(assert (! (<= __VERIFIER_assert_~cond_15 |__VERIFIER_assert_#in~cond_14|) :named ssa_15_conjunct0))
(assert (! (>= __VERIFIER_assert_~cond_15 |__VERIFIER_assert_#in~cond_14|) :named ssa_15_conjunct1))
(assert (! (not (= __VERIFIER_assert_~cond_15 0)) :named ssa_16_conjunct0))
(assert (! true :named ssa_17_conjunct0))
(assert (! true :named ssa_18_return_conjunct0))
(assert (! true :named ssa_19_conjunct0))
(assert (! (<= main_~x~5_20 (+ main_~x~5_13 (* 2 |main_#t~nondet0_13|))) :named ssa_20_conjunct0))
(assert (! (>= main_~x~5_20 (+ main_~x~5_13 (* 2 |main_#t~nondet0_13|))) :named ssa_20_conjunct1))
(assert (! (<= main_~y~5_20 (+ main_~y~5_13 (* 4 |main_#t~nondet1_13|))) :named ssa_20_conjunct2))
(assert (! (>= main_~y~5_20 (+ main_~y~5_13 (* 4 |main_#t~nondet1_13|))) :named ssa_20_conjunct3))
(assert (! (<= main_~z~5_20 (+ main_~z~5_13 (* 8 |main_#t~nondet2_13|))) :named ssa_20_conjunct4))
(assert (! (>= main_~z~5_20 (+ main_~z~5_13 (* 8 |main_#t~nondet2_13|))) :named ssa_20_conjunct5))
(assert (! true :named ssa_21_GlobVarAssigCall_conjunct0))
(assert (! (<= |__VERIFIER_assert_#in~cond_21| (ite (not (= (+ (+ (* 4 main_~x~5_20) (* 2 main_~y~5_20)) main_~z~5_20) 4)) 1 0)) :named ssa_21_LocVarAssigCall_conjunct0))
(assert (! (>= |__VERIFIER_assert_#in~cond_21| (ite (not (= (+ (+ (* 4 main_~x~5_20) (* 2 main_~y~5_20)) main_~z~5_20) 4)) 1 0)) :named ssa_21_LocVarAssigCall_conjunct1))
(assert (! true :named ssa_21_OldVarAssigCall_conjunct0))
(assert (! (<= __VERIFIER_assert_~cond_22 |__VERIFIER_assert_#in~cond_21|) :named ssa_22_conjunct0))
(assert (! (>= __VERIFIER_assert_~cond_22 |__VERIFIER_assert_#in~cond_21|) :named ssa_22_conjunct1))
(assert (! (not (= __VERIFIER_assert_~cond_22 0)) :named ssa_23_conjunct0))
(assert (! true :named ssa_24_conjunct0))
(assert (! true :named ssa_25_return_conjunct0))
(assert (! true :named ssa_26_conjunct0))
(assert (! (<= main_~x~5_27 (+ main_~x~5_20 (* 2 |main_#t~nondet0_20|))) :named ssa_27_conjunct0))
(assert (! (>= main_~x~5_27 (+ main_~x~5_20 (* 2 |main_#t~nondet0_20|))) :named ssa_27_conjunct1))
(assert (! (<= main_~y~5_27 (+ main_~y~5_20 (* 4 |main_#t~nondet1_20|))) :named ssa_27_conjunct2))
(assert (! (>= main_~y~5_27 (+ main_~y~5_20 (* 4 |main_#t~nondet1_20|))) :named ssa_27_conjunct3))
(assert (! (<= main_~z~5_27 (+ main_~z~5_20 (* 8 |main_#t~nondet2_20|))) :named ssa_27_conjunct4))
(assert (! (>= main_~z~5_27 (+ main_~z~5_20 (* 8 |main_#t~nondet2_20|))) :named ssa_27_conjunct5))
(assert (! true :named ssa_28_GlobVarAssigCall_conjunct0))
(assert (! (<= |__VERIFIER_assert_#in~cond_28| (ite (not (= (+ (+ (* 4 main_~x~5_27) (* 2 main_~y~5_27)) main_~z~5_27) 4)) 1 0)) :named ssa_28_LocVarAssigCall_conjunct0))
(assert (! (>= |__VERIFIER_assert_#in~cond_28| (ite (not (= (+ (+ (* 4 main_~x~5_27) (* 2 main_~y~5_27)) main_~z~5_27) 4)) 1 0)) :named ssa_28_LocVarAssigCall_conjunct1))
(assert (! true :named ssa_28_OldVarAssigCall_conjunct0))
(assert (! (<= __VERIFIER_assert_~cond_29 |__VERIFIER_assert_#in~cond_28|) :named ssa_29_conjunct0))
(assert (! (>= __VERIFIER_assert_~cond_29 |__VERIFIER_assert_#in~cond_28|) :named ssa_29_conjunct1))
(assert (! (not (= __VERIFIER_assert_~cond_29 0)) :named ssa_30_conjunct0))
(assert (! true :named ssa_31_conjunct0))
(assert (! true :named ssa_32_return_conjunct0))
(assert (! true :named ssa_33_conjunct0))
(assert (! (<= main_~x~5_34 (+ main_~x~5_27 (* 2 |main_#t~nondet0_27|))) :named ssa_34_conjunct0))
(assert (! (>= main_~x~5_34 (+ main_~x~5_27 (* 2 |main_#t~nondet0_27|))) :named ssa_34_conjunct1))
(assert (! (<= main_~y~5_34 (+ main_~y~5_27 (* 4 |main_#t~nondet1_27|))) :named ssa_34_conjunct2))
(assert (! (>= main_~y~5_34 (+ main_~y~5_27 (* 4 |main_#t~nondet1_27|))) :named ssa_34_conjunct3))
(assert (! (<= main_~z~5_34 (+ main_~z~5_27 (* 8 |main_#t~nondet2_27|))) :named ssa_34_conjunct4))
(assert (! (>= main_~z~5_34 (+ main_~z~5_27 (* 8 |main_#t~nondet2_27|))) :named ssa_34_conjunct5))
(assert (! true :named ssa_35_GlobVarAssigCall_conjunct0))
(assert (! (<= |__VERIFIER_assert_#in~cond_35| (ite (not (= (+ (+ (* 4 main_~x~5_34) (* 2 main_~y~5_34)) main_~z~5_34) 4)) 1 0)) :named ssa_35_LocVarAssigCall_conjunct0))
(assert (! (>= |__VERIFIER_assert_#in~cond_35| (ite (not (= (+ (+ (* 4 main_~x~5_34) (* 2 main_~y~5_34)) main_~z~5_34) 4)) 1 0)) :named ssa_35_LocVarAssigCall_conjunct1))
(assert (! true :named ssa_35_OldVarAssigCall_conjunct0))
(assert (! (<= __VERIFIER_assert_~cond_36 |__VERIFIER_assert_#in~cond_35|) :named ssa_36_conjunct0))
(assert (! (>= __VERIFIER_assert_~cond_36 |__VERIFIER_assert_#in~cond_35|) :named ssa_36_conjunct1))
(assert (! (not (= __VERIFIER_assert_~cond_36 0)) :named ssa_37_conjunct0))
(assert (! true :named ssa_38_conjunct0))
(assert (! true :named ssa_39_return_conjunct0))
(assert (! true :named ssa_40_conjunct0))
(assert (! (<= main_~x~5_41 (+ main_~x~5_34 (* 2 |main_#t~nondet0_34|))) :named ssa_41_conjunct0))
(assert (! (>= main_~x~5_41 (+ main_~x~5_34 (* 2 |main_#t~nondet0_34|))) :named ssa_41_conjunct1))
(assert (! (<= main_~y~5_41 (+ main_~y~5_34 (* 4 |main_#t~nondet1_34|))) :named ssa_41_conjunct2))
(assert (! (>= main_~y~5_41 (+ main_~y~5_34 (* 4 |main_#t~nondet1_34|))) :named ssa_41_conjunct3))
(assert (! (<= main_~z~5_41 (+ main_~z~5_34 (* 8 |main_#t~nondet2_34|))) :named ssa_41_conjunct4))
(assert (! (>= main_~z~5_41 (+ main_~z~5_34 (* 8 |main_#t~nondet2_34|))) :named ssa_41_conjunct5))
(assert (! true :named ssa_42_GlobVarAssigCall_conjunct0))
(assert (! (<= |__VERIFIER_assert_#in~cond_42| (ite (not (= (+ (+ (* 4 main_~x~5_41) (* 2 main_~y~5_41)) main_~z~5_41) 4)) 1 0)) :named ssa_42_LocVarAssigCall_conjunct0))
(assert (! (>= |__VERIFIER_assert_#in~cond_42| (ite (not (= (+ (+ (* 4 main_~x~5_41) (* 2 main_~y~5_41)) main_~z~5_41) 4)) 1 0)) :named ssa_42_LocVarAssigCall_conjunct1))
(assert (! true :named ssa_42_OldVarAssigCall_conjunct0))
(assert (! (<= __VERIFIER_assert_~cond_43 |__VERIFIER_assert_#in~cond_42|) :named ssa_43_conjunct0))
(assert (! (>= __VERIFIER_assert_~cond_43 |__VERIFIER_assert_#in~cond_42|) :named ssa_43_conjunct1))
(assert (! (not (= __VERIFIER_assert_~cond_43 0)) :named ssa_44_conjunct0))
(assert (! true :named ssa_45_conjunct0))
(assert (! true :named ssa_46_return_conjunct0))
(assert (! true :named ssa_47_conjunct0))
(assert (! (<= main_~x~5_48 (+ main_~x~5_41 (* 2 |main_#t~nondet0_41|))) :named ssa_48_conjunct0))
(assert (! (>= main_~x~5_48 (+ main_~x~5_41 (* 2 |main_#t~nondet0_41|))) :named ssa_48_conjunct1))
(assert (! (<= main_~y~5_48 (+ main_~y~5_41 (* 4 |main_#t~nondet1_41|))) :named ssa_48_conjunct2))
(assert (! (>= main_~y~5_48 (+ main_~y~5_41 (* 4 |main_#t~nondet1_41|))) :named ssa_48_conjunct3))
(assert (! (<= main_~z~5_48 (+ main_~z~5_41 (* 8 |main_#t~nondet2_41|))) :named ssa_48_conjunct4))
(assert (! (>= main_~z~5_48 (+ main_~z~5_41 (* 8 |main_#t~nondet2_41|))) :named ssa_48_conjunct5))
(assert (! true :named ssa_49_GlobVarAssigCall_conjunct0))
(assert (! (<= |__VERIFIER_assert_#in~cond_49| (ite (not (= (+ (+ (* 4 main_~x~5_48) (* 2 main_~y~5_48)) main_~z~5_48) 4)) 1 0)) :named ssa_49_LocVarAssigCall_conjunct0))
(assert (! (>= |__VERIFIER_assert_#in~cond_49| (ite (not (= (+ (+ (* 4 main_~x~5_48) (* 2 main_~y~5_48)) main_~z~5_48) 4)) 1 0)) :named ssa_49_LocVarAssigCall_conjunct1))
(assert (! true :named ssa_49_OldVarAssigCall_conjunct0))
(assert (! (<= __VERIFIER_assert_~cond_50 |__VERIFIER_assert_#in~cond_49|) :named ssa_50_conjunct0))
(assert (! (>= __VERIFIER_assert_~cond_50 |__VERIFIER_assert_#in~cond_49|) :named ssa_50_conjunct1))
(assert (! (not (= __VERIFIER_assert_~cond_50 0)) :named ssa_51_conjunct0))
(assert (! true :named ssa_52_conjunct0))
(assert (! true :named ssa_53_return_conjunct0))
(assert (! true :named ssa_54_conjunct0))
(assert (! (<= main_~x~5_55 (+ main_~x~5_48 (* 2 |main_#t~nondet0_48|))) :named ssa_55_conjunct0))
(assert (! (>= main_~x~5_55 (+ main_~x~5_48 (* 2 |main_#t~nondet0_48|))) :named ssa_55_conjunct1))
(assert (! (<= main_~y~5_55 (+ main_~y~5_48 (* 4 |main_#t~nondet1_48|))) :named ssa_55_conjunct2))
(assert (! (>= main_~y~5_55 (+ main_~y~5_48 (* 4 |main_#t~nondet1_48|))) :named ssa_55_conjunct3))
(assert (! (<= main_~z~5_55 (+ main_~z~5_48 (* 8 |main_#t~nondet2_48|))) :named ssa_55_conjunct4))
(assert (! (>= main_~z~5_55 (+ main_~z~5_48 (* 8 |main_#t~nondet2_48|))) :named ssa_55_conjunct5))
(assert (! true :named ssa_56_GlobVarAssigCall_conjunct0))
(assert (! (<= |__VERIFIER_assert_#in~cond_56| (ite (not (= (+ (+ (* 4 main_~x~5_55) (* 2 main_~y~5_55)) main_~z~5_55) 4)) 1 0)) :named ssa_56_LocVarAssigCall_conjunct0))
(assert (! (>= |__VERIFIER_assert_#in~cond_56| (ite (not (= (+ (+ (* 4 main_~x~5_55) (* 2 main_~y~5_55)) main_~z~5_55) 4)) 1 0)) :named ssa_56_LocVarAssigCall_conjunct1))
(assert (! true :named ssa_56_OldVarAssigCall_conjunct0))
(assert (! (<= __VERIFIER_assert_~cond_57 |__VERIFIER_assert_#in~cond_56|) :named ssa_57_conjunct0))
(assert (! (>= __VERIFIER_assert_~cond_57 |__VERIFIER_assert_#in~cond_56|) :named ssa_57_conjunct1))
(assert (! (not (= __VERIFIER_assert_~cond_57 0)) :named ssa_58_conjunct0))
(assert (! true :named ssa_59_conjunct0))
(assert (! true :named ssa_60_return_conjunct0))
(assert (! true :named ssa_61_conjunct0))
(assert (! (<= main_~x~5_62 (+ main_~x~5_55 (* 2 |main_#t~nondet0_55|))) :named ssa_62_conjunct0))
(assert (! (>= main_~x~5_62 (+ main_~x~5_55 (* 2 |main_#t~nondet0_55|))) :named ssa_62_conjunct1))
(assert (! (<= main_~y~5_62 (+ main_~y~5_55 (* 4 |main_#t~nondet1_55|))) :named ssa_62_conjunct2))
(assert (! (>= main_~y~5_62 (+ main_~y~5_55 (* 4 |main_#t~nondet1_55|))) :named ssa_62_conjunct3))
(assert (! (<= main_~z~5_62 (+ main_~z~5_55 (* 8 |main_#t~nondet2_55|))) :named ssa_62_conjunct4))
(assert (! (>= main_~z~5_62 (+ main_~z~5_55 (* 8 |main_#t~nondet2_55|))) :named ssa_62_conjunct5))
(assert (! true :named ssa_63_GlobVarAssigCall_conjunct0))
(assert (! (<= |__VERIFIER_assert_#in~cond_63| (ite (not (= (+ (+ (* 4 main_~x~5_62) (* 2 main_~y~5_62)) main_~z~5_62) 4)) 1 0)) :named ssa_63_LocVarAssigCall_conjunct0))
(assert (! (>= |__VERIFIER_assert_#in~cond_63| (ite (not (= (+ (+ (* 4 main_~x~5_62) (* 2 main_~y~5_62)) main_~z~5_62) 4)) 1 0)) :named ssa_63_LocVarAssigCall_conjunct1))
(assert (! true :named ssa_63_OldVarAssigCall_conjunct0))
(assert (! (<= __VERIFIER_assert_~cond_64 |__VERIFIER_assert_#in~cond_63|) :named ssa_64_conjunct0))
(assert (! (>= __VERIFIER_assert_~cond_64 |__VERIFIER_assert_#in~cond_63|) :named ssa_64_conjunct1))
(assert (! (not (= __VERIFIER_assert_~cond_64 0)) :named ssa_65_conjunct0))
(assert (! true :named ssa_66_conjunct0))
(assert (! true :named ssa_67_return_conjunct0))
(assert (! true :named ssa_68_conjunct0))
(assert (! (<= main_~x~5_69 (+ main_~x~5_62 (* 2 |main_#t~nondet0_62|))) :named ssa_69_conjunct0))
(assert (! (>= main_~x~5_69 (+ main_~x~5_62 (* 2 |main_#t~nondet0_62|))) :named ssa_69_conjunct1))
(assert (! (<= main_~y~5_69 (+ main_~y~5_62 (* 4 |main_#t~nondet1_62|))) :named ssa_69_conjunct2))
(assert (! (>= main_~y~5_69 (+ main_~y~5_62 (* 4 |main_#t~nondet1_62|))) :named ssa_69_conjunct3))
(assert (! (<= main_~z~5_69 (+ main_~z~5_62 (* 8 |main_#t~nondet2_62|))) :named ssa_69_conjunct4))
(assert (! (>= main_~z~5_69 (+ main_~z~5_62 (* 8 |main_#t~nondet2_62|))) :named ssa_69_conjunct5))
(assert (! true :named ssa_70_GlobVarAssigCall_conjunct0))
(assert (! (<= |__VERIFIER_assert_#in~cond_70| (ite (not (= (+ (+ (* 4 main_~x~5_69) (* 2 main_~y~5_69)) main_~z~5_69) 4)) 1 0)) :named ssa_70_LocVarAssigCall_conjunct0))
(assert (! (>= |__VERIFIER_assert_#in~cond_70| (ite (not (= (+ (+ (* 4 main_~x~5_69) (* 2 main_~y~5_69)) main_~z~5_69) 4)) 1 0)) :named ssa_70_LocVarAssigCall_conjunct1))
(assert (! true :named ssa_70_OldVarAssigCall_conjunct0))
(assert (! (<= __VERIFIER_assert_~cond_71 |__VERIFIER_assert_#in~cond_70|) :named ssa_71_conjunct0))
(assert (! (>= __VERIFIER_assert_~cond_71 |__VERIFIER_assert_#in~cond_70|) :named ssa_71_conjunct1))
(assert (! (<= __VERIFIER_assert_~cond_71 0) :named ssa_72_conjunct0))
(assert (! (>= __VERIFIER_assert_~cond_71 0) :named ssa_72_conjunct1))
(assert (! true :named ssa_73_conjunct0))
(check-sat)
(get-unsat-core)

Install error

In d7e6ca7

After successful make, install doesn't work

dejan@pup:~/workspace/z3-unstable/build$ make install
cp: cannot stat ‘libz3java.so’: No such file or directory
make: *** [install] Error 1

Configured with

python scripts/mk_make.py --prefix=/homes/dejan/Software

debug build fails

When trying to compile z3 (unstable branch) with mk_make.py -d, it fails with:

g++ -o z3  shell/main.o shell/dimacs_frontend.o shell/z3_log_frontend.o shell/mem_initializer.o shell/datalog_frontend.o shell/smtlib_frontend.o shell/install_tactic.o shell/gparams_register_modules.o api/api.a parsers/smt/smtparser.a tactic/portfolio/portfolio.a tactic/ufbv/ufbv_tactic.a tactic/smtlogics/smtlogic_tactics.a muz/fp/fp.a muz/duality/duality_intf.a muz/bmc/bmc.a muz/tab/tab.a muz/clp/clp.a muz/pdr/pdr.a muz/rel/rel.a muz/transforms/transforms.a muz/base/muz.a duality/duality.a qe/qe.a tactic/sls/sls_tactic.a tactic/fpa/fpa_tactics.a smt/tactic/smt_tactic.a tactic/bv/bv_tactics.a smt/user_plugin/user_plugin.a smt/smt.a smt/proto_model/proto_model.a smt/params/smt_params.a ast/rewriter/bit_blaster/bit_blaster.a ast/pattern/pattern.a ast/macros/macros.a ast/fpa/fpa.a ast/simplifier/simplifier.a ast/proof_checker/proof_checker.a parsers/smt2/smt2parser.a cmd_context/extra_cmds/extra_cmds.a cmd_context/cmd_context.a interp/interp.a solver/solver.a tactic/aig/aig_tactic.a math/subpaving/tactic/subpaving_tactic.a nlsat/tactic/nlsat_tactic.a tactic/arith/arith_tactics.a sat/tactic/sat_tactic.a tactic/core/core_tactics.a math/euclid/euclid.a math/grobner/grobner.a parsers/util/parser_util.a ast/substitution/substitution.a tactic/tactic.a model/model.a ast/normal_forms/normal_forms.a ast/rewriter/rewriter.a ast/ast.a math/subpaving/subpaving.a math/realclosure/realclosure.a math/interval/interval.a math/hilbert/hilbert.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a  -lpthread -Wl,-O1,--sort-common,--as-needed,-z,relro -fopenmp -lrt
parsers/smt/smtparser.a(smtparser.o): In function `proto_region::~proto_region()':
smtparser.cpp:(.text._ZN12proto_regionD2Ev[_ZN12proto_regionD5Ev]+0x12a): undefined reference to `region::reset()'
parsers/smt/smtparser.a(smtparser.o): In function `smtparser::make_expression(symbol_table<idbuilder*>&, proto_expr*, obj_ref<expr, ast_manager>&)':
smtparser.cpp:(.text._ZN9smtparser15make_expressionER12symbol_tableIP9idbuilderEP10proto_exprR7obj_refI4expr11ast_managerE[_ZN9smtparser15make_expressionER12symbol_tableIP9idbuilderEP10proto_exprR7obj_refI4expr11ast_managerE]+0x50): undefined reference to `region::region()'
parsers/smt/smtparser.a(smtparser.o): In function `smtparser::read_patterns(unsigned int, symbol_table<idbuilder*>&, proto_expr* const*&, ref_buffer<expr, ast_manager, 16u>&, ref_buffer<expr, ast_manager, 16u>&, int&, symbol&, symbol&)':
smtparser.cpp:(.text._ZN9smtparser13read_patternsEjR12symbol_tableIP9idbuilderERPKP10proto_exprR10ref_bufferI4expr11ast_managerLj16EESE_RiR6symbolSH_[_ZN9smtparser13read_patternsEjR12symbol_tableIP9idbuilderERPKP10proto_exprR10ref_bufferI4expr11ast_managerLj16EESE_RiR6symbolSH_]+0x8e): undefined reference to `region::region()'
parsers/smt/smtparser.a(smtparser.o): In function `smtparser::parse_string(char const*)':
smtparser.cpp:(.text._ZN9smtparser12parse_stringEPKc[_ZN9smtparser12parse_stringEPKc]+0x1f0): undefined reference to `region::region()'
parsers/smt/smtparser.a(smtparser.o): In function `smtparser::parse_stream(std::istream&)':
smtparser.cpp:(.text._ZN9smtparser12parse_streamERSi[_ZN9smtparser12parse_streamERSi]+0x42): undefined reference to `region::region()'
collect2: error: ld returned 1 exit status
Makefile:3216: recipe for target 'z3' failed
make: *** [z3] Error 1

Questions about and suggestions for build system

The build system currently fails with python3 as the default python interpreter (which is the case e.g. for debian jessie, gentoo, arch, ..), since the mk/* scripts use deprecated python2 syntax.

I saw comments about the python2 requirement being added and then again removed from the readme; but as far as I see it, python2 is still required. Is this intended? What are the assumptions about the target platforms? python2 and optionally python3? If so, which versions do you want to support?

There is also at least one argument mismatch that I encountered: --help lists the "--makefiles" flag, but if you specify it, the script fails. Looking through the source reveals why: "--onlymakefiles" is the flag's name and not "--makefiles".

Now after trying "--onlymakefiles" the script still fails, this time because it's unable to find a c++ file, rendering this flag completely useless.

Is there a reason for not using e.g. python's argparse and calling it a day?

Please don't see this as criticism, I just want to understand the reasons behind the build system's design. I'm more than glad to help out with the Linux specific parts, if you need any help -- but for this I need a more precise specification of what you actually want :)

Opt-branch, optimization times out on a relatively simple query

Hi, I have an unexpected optimization timeout on a query with no disjunctions and some UF's:

[(= |[0]_main::n@3| |BOUND_[0]_[main::n]|), (<= |[0]_main::n@2| |BOUND_[0]_[main::n]|), (= (+ |[0]_main::i@4| |[0]_main::n@3|) |BOUND_[0]_[main::i + main::n]|), (<= (+ (* (- 1) |[0]_main::k@3|) (* (- 1) |[0]_main::n@2|))
    |BOUND_[0]_[ - main::k - main::n]|), (<= (+ (* (- 1) |[0]_main::k@3|) |[0]_main::i@3|)
    |BOUND_[0]_[main::i - main::k]|), (<= |[0]_main::k@3| |BOUND_[0]_[main::k]|), (<= (+ (* (- 1) |[0]_main::k@3|) |[0]_main::n@2|)
    |BOUND_[0]_[ - main::k + main::n]|), (<= (* (- 1) |[0]_main::i@3|) |BOUND_[0]_[ - main::i]|), (<= (+ (* (- 1) |[0]_main::i@3|) |[0]_main::n@2|)
    |BOUND_[0]_[ - main::i + main::n]|), (= (+ |[0]_main::k@3| |[0]_main::n@3|) |BOUND_[0]_[main::k + main::n]|), (<= (* (- 1) |[0]_main::k@3|) |BOUND_[0]_[ - main::k]|), (= |[0]_main::i@4| |BOUND_[0]_[main::i]|), (<= (+ |[0]_main::k@3| |[0]_main::n@2|) |BOUND_[0]_[main::k 
+ main::n]|), (<= (+ |[0]_main::i@3| |[0]_main::n@2|) |BOUND_[0]_[main::i + main::n]|), (<= (+ |[0]_main::k@3| |[0]_main::i@3|) |BOUND_[0]_[main::i + main::k]|), (<= (+ |[0]_main::k@3| (* (- 1) |[0]_main::n@2|))
    |BOUND_[0]_[main::k - main::n]|), (<= (+ (* (- 1) |[0]_main::k@3|) (* (- 1) |[0]_main::i@3|))
    |BOUND_[0]_[ - main::i - main::k]|), (<= (+ |[0]_main::k@3| (* (- 1) |[0]_main::i@3|))
    |BOUND_[0]_[ - main::i + main::k]|), (<= |[0]_main::i@3| |BOUND_[0]_[main::i]|), (<= (* (- 1) |[0]_main::n@2|) |BOUND_[0]_[ - main::n]|), (<= (+ (* (- 1) |[0]_main::i@3|) (* (- 1) |[0]_main::n@2|))
    |BOUND_[0]_[ - main::i - main::n]|), (<= (+ |[0]_main::i@3| (* (- 1) |[0]_main::n@2|))
    |BOUND_[0]_[main::i - main::n]|), (let ((a!1 (ite (>= |[0]_main::i@3| 0)
                (and (>= (|[0]_Integer__%_| |[0]_main::i@3| 2) 0)
                     (<= (|[0]_Integer__%_| |[0]_main::i@3| 2) |[0]_main::i@3|))
                (and (<= (|[0]_Integer__%_| |[0]_main::i@3| 2) 0)
                     (>= (|[0]_Integer__%_| |[0]_main::i@3| 2) |[0]_main::i@3|)))))
  (and (= |[0]___INITIAL_LOCATION| 0)
       (not (<= (* 2 |[0]_main::k@3|) |[0]_main::i@3|))
       (= (|[0]_Integer__%_| |[0]_main::i@3| 2) 0)
       (= (|[0]_Integer__%_| |[0]_main::i@3| 2)
          (+ |[0]_main::i@3| (* 2 |[0]___CONGRUENCE_0|)))
       a!1
       (not (<= 2 (|[0]_Integer__%_| |[0]_main::i@3| 2)))
       (= |[0]_main::n@3| (+ 1 |[0]_main::n@2|))
       (= |[0]_main::i@4| (+ 1 |[0]_main::i@3|)))), (= (+ |[0]_main::k@3| |[0]_main::i@4|) |BOUND_[0]_[main::i + main::k]|)]

Where all variables are integers.
Maximizing for BOUND_[0]_[main::i], ...i+n, ...n and ...k+n works just fine, but optimization for BOUND_[0]_[main::i + main::k] times out.
The replayable log can be found @ http://metaworld.me/timeout_opt.log

InterpolationContext in InterpolationContext.cs is not public

As far as I can see, this is an oversight, as the equivalent class in the java API is indeed public.
On the dotnet side, this makes it impossible to use interpolation, unless I overlooked something.

FP to real and back conversions don't seem to be operational

This is on the unstable branch.

I'm experimenting with floating-point to real (fp.to_real) and back-conversions ((_ to_fp eb sb)). It appears Z3 is always producing unknown or going away forever for queries that involve these conversions. Is something wrong with the way I've constructed the benchmarks (logic-selection comes to mind), or is this just not quite working well yet?

Here's an example benchmark that causes Z3 to run forever. (Well, I just killed it after a while)

; Automatically generated by SBV. Do not edit.
(set-option :produce-models true)
(set-logic QF_FP)
; --- uninterpreted sorts ---
; --- literal constants ---
(define-fun s_2 () Bool false)
(define-fun s_1 () Bool true)
; --- skolem constants ---
(declare-fun s0 () Real)
(declare-fun s1 () RoundingMode)
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(assert ; no quantifiers
   (let ((s2 ((_ to_fp 8 24) s1 s0)))
   (let ((s3 (fp.to_real s2)))
   (let ((s4 (distinct s0 s3)))
   s4))))
(check-sat)

And this one causes Z3 to issue unknown:

; Automatically generated by SBV. Do not edit.
(set-option :produce-models true)
(set-logic QF_FP)
; --- uninterpreted sorts ---
; --- literal constants ---
(define-fun s_2 () Bool false)
(define-fun s_1 () Bool true)
; --- skolem constants ---
(declare-fun s0 () Real)
(declare-fun s1 () RoundingMode)
(declare-fun s2 () RoundingMode)
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(assert ; no quantifiers
   (let ((s3 ((_ to_fp 8 24) s1 s0)))
   (let ((s4 ((_ to_fp 8 24) s2 s0)))
   (let ((s5 (not (fp.eq s3 s4))))
   s5))))
(check-sat)

reserved identifier violation

I would like to point out that identifiers like "_API_AST_MAP_H_" and "_SOLVER_H_" do eventually not fit to the expected naming convention of the C++ language standard.
Would you like to adjust your selection for unique names?

C API: Z3_mk_distinct() doesn't do type checking

All n-ary functions (mk_distinct, mk_and, mk_or, etc) are not type checked when created through the API.
Like the other functions, the API calls check_sorts(), which ends up in ast_manager::check_sorts_core(), but this method only checks unary and binary function applications.

BTW, is_well_sorted() does verify functions with any arity. Can't these 2 functions be merged?
This function is currently used in assertions in goal/solver/tactics, for example.

crash in del_inactive_lemmas2

The following code crashes Z3:

from z3 import *

cond = BitVec('cond', 1)
p = BitVec('p', 32)
mem0 = Array('mem0', BitVecSort(32), BitVecSort(8))

fml = And(If(cond == 1, 0, p) != 0,
          mem0[If(cond == 1, 0, p) + 1] != mem0[p + 1])

s = Solver()
s.add(fml)
print s.check()

Trace:

#0  0x00aae767 in smt::context::del_inactive_lemmas2 (this=0x801f7534)
    at ../src/smt/smt_context.cpp:2636
#1  0x00ab6835 in del_inactive_lemmas (this=0x801f7534)
    at ../src/smt/smt_context.cpp:2538
#2  smt::context::bounded_search (this=this@entry=0x801f7534)
    at ../src/smt/smt_context.cpp:3317
#3  0x00ab691a in smt::context::search (this=this@entry=0x801f7534)
    at ../src/smt/smt_context.cpp:3180
#4  0x00ab6ec8 in smt::context::setup_and_check (this=0x801f7534,
    reset_cancel=reset_cancel@entry=true) at ../src/smt/smt_context.cpp:2985
#5  0x00aca699 in setup_and_check (this=<optimized out>)
    at ../src/smt/smt_kernel.cpp:87
#6  smt::kernel::setup_and_check (this=this@entry=0x8018254c)
    at ../src/smt/smt_kernel.cpp:249
#7  0x00e4009f in smt_tactic::operator() (this=0x8023c324, in=..., result=...,
    mc=..., pc=..., core=...) at ../src/smt/tactic/smt_tactic.cpp:220
#8  0x00fee5c4 in and_then_tactical::operator() (this=0x8023c62c, in=...,
    result=..., mc=..., pc=..., core=...) at ../src/tactic/tactical.cpp:167
#9  0x00fee5c4 in and_then_tactical::operator() (this=0x80242e7c, in=...,
    result=..., mc=..., pc=..., core=...) at ../src/tactic/tactical.cpp:167
#10 0x00c691a5 in exec (t=..., in=..., result=..., mc=..., pc=..., core=...)
    at ../src/tactic/tactic.cpp:179
#11 0x00c69632 in check_sat (t=..., g=..., md=..., pr=..., core=...,
    reason_unknown=...) at ../src/tactic/tactic.cpp:201

Bug, rational produced where an integer is expected.

Malte Schwerhoff has previously reported a bug on stackoverflow:

http://stackoverflow.com/questions/28088487/unexpected-error-message-reproduction-apparently-very-fragile-bug

Internally a rational is produced where an integer is expected.

Bug in either FP conversion or addition

This is on the unstable branch.

The following benchmark is essentially asking Z3 to compute the addition of the following two numbers:

   15749125 / 64
   268632143 / 1024

represented as single-precision floating point numbers.

With roundNearestTiesToEven, these numbers in decimal are:

246080.08
16255.999

So, addition should produce

262336.06

But it appears Z3 is producing a value that equals

2.1885552e-38

which is nowhere even close. I'm not sure if the bug is in the conversion of the constants, which I believe you recently modified, or in the actual fp.add routine.

Here's the benchmark:

; Automatically generated by SBV. Do not edit.
(set-option :produce-models true)
(set-logic QF_FP)
; --- uninterpreted sorts ---
; --- literal constants ---
(define-fun s_2 () Bool false)
(define-fun s_1 () Bool true)
(define-fun s1 () RoundingMode roundNearestTiesToEven)
(define-fun s2 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 15749125 64)))
(define-fun s3 () (_ FloatingPoint  8 24) ((_ to_fp 8 24) roundNearestTiesToEven (/ 16646143 1024)))
; --- skolem constants ---
(declare-fun s0 () (_ FloatingPoint  8 24))
; --- constant tables ---
; --- skolemized tables ---
; --- arrays ---
; --- uninterpreted constants ---
; --- user given axioms ---
; --- formula ---
(assert ; no quantifiers
   (let ((s4 (fp.add s1 s2 s3)))
   (let ((s5 (fp.eq s0 s4)))
   s5)))
(check-sat)
(get-value (s0))

Z3 responds:

sat
((s0 (fp #b0 #x01 #b11011100101000000000100)))

which is the internal representation for 2.1885552E-38

Can you merge the new ML API from the unstable branch into the master branch?

Segfault in IDL

On problem https://gist.github.com/dddejan/80537e542611c0f7cfea

Compiling a to a statically linked binary

With a tiny change to the build system it's possible to compile to a statically linked binary. The issue is that -lrt needs to appear before -lpthread in the linker options on linux. Here's a fix that allows that:

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 4641a7b..3ece506 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1613,7 +1613,7 @@ def mk_config():
         config.write('LINK=%s\n' % CXX)
         config.write('LINK_FLAGS=\n')
         config.write('LINK_OUT_FLAG=-o \n')
-        config.write('LINK_EXTRA_FLAGS=-lpthread %s\n' % LDFLAGS)
+        config.write('LINK_EXTRA_FLAGS=%s -lpthread\n' % LDFLAGS)
         config.write('SO_EXT=%s\n' % SO_EXT)
         config.write('SLINK=%s\n' % CXX)
         config.write('SLINK_FLAGS=%s\n' % SLIBFLAGS)

With the change applied, the following steps allow building the statically linked binary:

LDFLAGS="-static-libstdc++ -static-libgcc -static" CXXFLAGS="-static-libstdc++ -static-libgcc -static" python2 scripts/mk_make.py
cd build; make -j4 as usual

The motivation for linking statically is to make it easy to pass around the binary and to be able to use it in small docker images, such as wunderseltsam/constraint-solvers.

I'd be happy to submit a pull-request against master or unstable if the change is useful.

segmentation fault when creating constant in c++ api

The following c++ api code for z3 results in Segmentation fault: 11 (z3 version 4.4.0 running on Mac OS 10.10.2) (also asked this as a question at stackoverflow)

#include "../z3/include/z3++.h"

int main() {
  z3::context c;

  z3::sort A = z3::sort(c);
  z3::expr x = c.constant("x", A);
}

segfault in mk_unit_resolution

Hi,

I encounter a segfault inside mk_unit_resolution.

Unfortunately, the replayable log I have for the problem is rather large (143MB): http://metaworld.me/segfault.log .
I can compile Z3 in debug mode and look at the stack trace to try to isolate the problem if required.

z3prover / z3 Goto Github PK

z3's Introduction

Z3

Build status

Building Z3 on Windows using Visual Studio Command Prompt

Building Z3 using make and GCC/Clang

Building Z3 using CMake

Building Z3 using vcpkg

Dependencies

Z3 bindings

.NET

C

C++

Java

OCaml

Python

Julia

Web Assembly / TypeScript / JavaScript

Smalltalk (Pharo / Smalltalk/X)

System Overview

Interfaces

z3's People

Contributors

Stargazers

Watchers

Forkers

z3's Issues

Here's an SMT-LIB2 example showing the problem:

Here's a tentative patch:

Recommend Projects

Recommend Topics

Recommend Org

`.NET`

`C`

`C++`

`Java`

`OCaml`

`Python`

`Julia`

`Web Assembly` / `TypeScript` / `JavaScript`

Smalltalk (`Pharo` / `Smalltalk/X`)