z3 →
4.4.0-2 →
armhf → 2015-07-25 08:30:40
sbuild (Debian sbuild) 0.65.2 (24 Mar 2015) on bm-wb-04
╔══════════════════════════════════════════════════════════════════════════════╗
║ z3 4.4.0-2 (armhf) 25 Jul 2015 06:46 ║
╚══════════════════════════════════════════════════════════════════════════════╝
Package: z3
Version: 4.4.0-2
Source Version: 4.4.0-2
Distribution: stretch-staging
Machine Architecture: armhf
Host Architecture: armhf
Build Architecture: armhf
I: NOTICE: Log filtering will replace 'build/z3-i230Te/z3-4.4.0' with '«PKGBUILDDIR»'
I: NOTICE: Log filtering will replace 'build/z3-i230Te' with '«BUILDDIR»'
I: NOTICE: Log filtering will replace 'var/lib/schroot/mount/stretch-staging-armhf-sbuild-9e196be8-8e33-4369-bd97-f88caee86d43' with '«CHROOT»'
┌──────────────────────────────────────────────────────────────────────────────┐
│ Update chroot │
└──────────────────────────────────────────────────────────────────────────────┘
Get:1 http://172.17.0.1 stretch-staging InRelease [11.3 kB]
Get:2 http://172.17.0.1 stretch-staging/main Sources [8141 kB]
Get:3 http://172.17.0.1 stretch-staging/main armhf Packages [10.0 MB]
Ign http://172.17.0.1 stretch-staging/main Translation-en
Fetched 18.2 MB in 34s (534 kB/s)
Reading package lists...
┌──────────────────────────────────────────────────────────────────────────────┐
│ Fetch source files │
└──────────────────────────────────────────────────────────────────────────────┘
Check APT
─────────
Checking available source versions...
Download source files with APT
──────────────────────────────
Reading package lists...
Building dependency tree...
Need to get 3466 kB of source archives.
Get:1 http://172.17.0.1/private/ stretch-staging/main z3 4.4.0-2 (dsc) [1784 B]
Get:2 http://172.17.0.1/private/ stretch-staging/main z3 4.4.0-2 (tar) [3457 kB]
Get:3 http://172.17.0.1/private/ stretch-staging/main z3 4.4.0-2 (diff) [6620 B]
Fetched 3466 kB in 0s (3538 kB/s)
Download complete and in download only mode
Check architectures
───────────────────
Check dependencies
──────────────────
Merged Build-Depends: build-essential, fakeroot
Filtered Build-Depends: build-essential, fakeroot
dpkg-deb: building package `sbuild-build-depends-core-dummy' in `/«BUILDDIR»/resolver-HLAL7X/apt_archive/sbuild-build-depends-core-dummy.deb'.
OK
Ign file: ./ InRelease
Get:1 file: ./ Release.gpg [299 B]
Get:2 file: ./ Release [2119 B]
Ign file: ./ Translation-en
Reading package lists...
Reading package lists...
┌──────────────────────────────────────────────────────────────────────────────┐
│ Install core build dependencies (apt-based resolver) │
└──────────────────────────────────────────────────────────────────────────────┘
Installing build dependencies
Reading package lists...
Building dependency tree...
The following NEW packages will be installed:
sbuild-build-depends-core-dummy
debconf: delaying package configuration, since apt-utils is not installed
0 upgraded, 1 newly installed, 0 to remove and 90 not upgraded.
Need to get 0 B/818 B of archives.
After this operation, 0 B of additional disk space will be used.
Selecting previously unselected package sbuild-build-depends-core-dummy.
(Reading database ...
(Reading database ... 5%
(Reading database ... 10%
(Reading database ... 15%
(Reading database ... 20%
(Reading database ... 25%
(Reading database ... 30%
(Reading database ... 35%
(Reading database ... 40%
(Reading database ... 45%
(Reading database ... 50%
(Reading database ... 55%
(Reading database ... 60%
(Reading database ... 65%
(Reading database ... 70%
(Reading database ... 75%
(Reading database ... 80%
(Reading database ... 85%
(Reading database ... 90%
(Reading database ... 95%
(Reading database ... 100%
(Reading database ... 11998 files and directories currently installed.)
Preparing to unpack .../sbuild-build-depends-core-dummy.deb ...
Unpacking sbuild-build-depends-core-dummy (0.invalid.0) ...
Setting up sbuild-build-depends-core-dummy (0.invalid.0) ...
Merged Build-Depends: libc6-dev | libc-dev, gcc (>= 4:4.9.1), g++ (>= 4:4.9.1), make, dpkg-dev (>= 1.17.11), debhelper (>= 9), python
Filtered Build-Depends: libc6-dev, gcc (>= 4:4.9.1), g++ (>= 4:4.9.1), make, dpkg-dev (>= 1.17.11), debhelper (>= 9), python
dpkg-deb: building package `sbuild-build-depends-z3-dummy' in `/«BUILDDIR»/resolver-D2lj_f/apt_archive/sbuild-build-depends-z3-dummy.deb'.
OK
Ign file: ./ InRelease
Get:1 file: ./ Release.gpg [299 B]
Get:2 file: ./ Release [2119 B]
Ign file: ./ Translation-en
Reading package lists...
Reading package lists...
┌──────────────────────────────────────────────────────────────────────────────┐
│ Install z3 build dependencies (apt-based resolver) │
└──────────────────────────────────────────────────────────────────────────────┘
Installing build dependencies
Reading package lists...
Building dependency tree...
Reading state information...
The following extra packages will be installed:
bsdmainutils debhelper file gettext gettext-base groff-base intltool-debian
libasprintf0c2 libcroco3 libexpat1 libffi6 libglib2.0-0 libmagic1
libpipeline1 libpython-stdlib libpython2.7-minimal libpython2.7-stdlib
libsqlite3-0 libssl1.0.0 libunistring0 libxml2 man-db mime-support
po-debconf python python-minimal python2.7 python2.7-minimal
Suggested packages:
wamerican wordlist whois vacation dh-make gettext-doc groff less www-browser
libmail-box-perl python-doc python-tk python2.7-doc binfmt-support
Recommended packages:
curl wget lynx-cur autopoint libasprintf-dev libgettextpo-dev
libglib2.0-data shared-mime-info xdg-user-dirs xml-core
libmail-sendmail-perl
The following NEW packages will be installed:
bsdmainutils debhelper file gettext gettext-base groff-base intltool-debian
libasprintf0c2 libcroco3 libexpat1 libffi6 libglib2.0-0 libmagic1
libpipeline1 libpython-stdlib libpython2.7-minimal libpython2.7-stdlib
libsqlite3-0 libssl1.0.0 libunistring0 libxml2 man-db mime-support
po-debconf python python-minimal python2.7 python2.7-minimal
sbuild-build-depends-z3-dummy
0 upgraded, 29 newly installed, 0 to remove and 90 not upgraded.
Need to get 13.6 MB/13.6 MB of archives.
After this operation, 43.0 MB of additional disk space will be used.
Get:1 http://172.17.0.1/private/ stretch-staging/main libpipeline1 armhf 1.4.0-1 [24.0 kB]
Get:2 http://172.17.0.1/private/ stretch-staging/main groff-base armhf 1.22.3-1 [1085 kB]
Get:3 http://172.17.0.1/private/ stretch-staging/main bsdmainutils armhf 9.0.6 [177 kB]
Get:4 http://172.17.0.1/private/ stretch-staging/main man-db armhf 2.7.0.2-5 [972 kB]
Get:5 http://172.17.0.1/private/ stretch-staging/main libasprintf0c2 armhf 0.19.4-1 [31.5 kB]
Get:6 http://172.17.0.1/private/ stretch-staging/main libmagic1 armhf 1:5.22+15-2 [244 kB]
Get:7 http://172.17.0.1/private/ stretch-staging/main libxml2 armhf 2.9.1+dfsg1-5 [703 kB]
Get:8 http://172.17.0.1/private/ stretch-staging/main libpython2.7-minimal armhf 2.7.10-3 [380 kB]
Get:9 http://172.17.0.1/private/ stretch-staging/main python2.7-minimal armhf 2.7.10-3 [1163 kB]
Get:10 http://172.17.0.1/private/ stretch-staging/main python-minimal armhf 2.7.9-1 [40.1 kB]
Get:11 http://172.17.0.1/private/ stretch-staging/main mime-support all 3.58 [36.0 kB]
Get:12 http://172.17.0.1/private/ stretch-staging/main libexpat1 armhf 2.1.0-6 [60.2 kB]
Get:13 http://172.17.0.1/private/ stretch-staging/main libffi6 armhf 3.2.1-3 [18.5 kB]
Get:14 http://172.17.0.1/private/ stretch-staging/main libsqlite3-0 armhf 3.8.10.2-1 [389 kB]
Get:15 http://172.17.0.1/private/ stretch-staging/main libssl1.0.0 armhf 1.0.2d-1 [882 kB]
Get:16 http://172.17.0.1/private/ stretch-staging/main libpython2.7-stdlib armhf 2.7.10-3 [1815 kB]
Get:17 http://172.17.0.1/private/ stretch-staging/main python2.7 armhf 2.7.10-3 [259 kB]
Get:18 http://172.17.0.1/private/ stretch-staging/main libpython-stdlib armhf 2.7.9-1 [19.6 kB]
Get:19 http://172.17.0.1/private/ stretch-staging/main python armhf 2.7.9-1 [151 kB]
Get:20 http://172.17.0.1/private/ stretch-staging/main libglib2.0-0 armhf 2.44.1-1.1 [2312 kB]
Get:21 http://172.17.0.1/private/ stretch-staging/main libcroco3 armhf 0.6.8-3 [121 kB]
Get:22 http://172.17.0.1/private/ stretch-staging/main libunistring0 armhf 0.9.3-5.2 [253 kB]
Get:23 http://172.17.0.1/private/ stretch-staging/main file armhf 1:5.22+15-2 [59.9 kB]
Get:24 http://172.17.0.1/private/ stretch-staging/main gettext-base armhf 0.19.4-1 [117 kB]
Get:25 http://172.17.0.1/private/ stretch-staging/main gettext armhf 0.19.4-1 [1168 kB]
Get:26 http://172.17.0.1/private/ stretch-staging/main intltool-debian all 0.35.0+20060710.2 [25.9 kB]
Get:27 http://172.17.0.1/private/ stretch-staging/main po-debconf all 1.0.18 [248 kB]
Get:28 http://172.17.0.1/private/ stretch-staging/main debhelper all 9.20150628 [817 kB]
debconf: delaying package configuration, since apt-utils is not installed
Fetched 13.6 MB in 3s (3785 kB/s)
Selecting previously unselected package libpipeline1:armhf.
(Reading database ...
(Reading database ... 5%
(Reading database ... 10%
(Reading database ... 15%
(Reading database ... 20%
(Reading database ... 25%
(Reading database ... 30%
(Reading database ... 35%
(Reading database ... 40%
(Reading database ... 45%
(Reading database ... 50%
(Reading database ... 55%
(Reading database ... 60%
(Reading database ... 65%
(Reading database ... 70%
(Reading database ... 75%
(Reading database ... 80%
(Reading database ... 85%
(Reading database ... 90%
(Reading database ... 95%
(Reading database ... 100%
(Reading database ... 11998 files and directories currently installed.)
Preparing to unpack .../libpipeline1_1.4.0-1_armhf.deb ...
Unpacking libpipeline1:armhf (1.4.0-1) ...
Selecting previously unselected package groff-base.
Preparing to unpack .../groff-base_1.22.3-1_armhf.deb ...
Unpacking groff-base (1.22.3-1) ...
Selecting previously unselected package bsdmainutils.
Preparing to unpack .../bsdmainutils_9.0.6_armhf.deb ...
Unpacking bsdmainutils (9.0.6) ...
Selecting previously unselected package man-db.
Preparing to unpack .../man-db_2.7.0.2-5_armhf.deb ...
Unpacking man-db (2.7.0.2-5) ...
Selecting previously unselected package libasprintf0c2:armhf.
Preparing to unpack .../libasprintf0c2_0.19.4-1_armhf.deb ...
Unpacking libasprintf0c2:armhf (0.19.4-1) ...
Selecting previously unselected package libmagic1:armhf.
Preparing to unpack .../libmagic1_1%3a5.22+15-2_armhf.deb ...
Unpacking libmagic1:armhf (1:5.22+15-2) ...
Selecting previously unselected package libxml2:armhf.
Preparing to unpack .../libxml2_2.9.1+dfsg1-5_armhf.deb ...
Unpacking libxml2:armhf (2.9.1+dfsg1-5) ...
Selecting previously unselected package libpython2.7-minimal:armhf.
Preparing to unpack .../libpython2.7-minimal_2.7.10-3_armhf.deb ...
Unpacking libpython2.7-minimal:armhf (2.7.10-3) ...
Selecting previously unselected package python2.7-minimal.
Preparing to unpack .../python2.7-minimal_2.7.10-3_armhf.deb ...
Unpacking python2.7-minimal (2.7.10-3) ...
Selecting previously unselected package python-minimal.
Preparing to unpack .../python-minimal_2.7.9-1_armhf.deb ...
Unpacking python-minimal (2.7.9-1) ...
Selecting previously unselected package mime-support.
Preparing to unpack .../mime-support_3.58_all.deb ...
Unpacking mime-support (3.58) ...
Selecting previously unselected package libexpat1:armhf.
Preparing to unpack .../libexpat1_2.1.0-6_armhf.deb ...
Unpacking libexpat1:armhf (2.1.0-6) ...
Selecting previously unselected package libffi6:armhf.
Preparing to unpack .../libffi6_3.2.1-3_armhf.deb ...
Unpacking libffi6:armhf (3.2.1-3) ...
Selecting previously unselected package libsqlite3-0:armhf.
Preparing to unpack .../libsqlite3-0_3.8.10.2-1_armhf.deb ...
Unpacking libsqlite3-0:armhf (3.8.10.2-1) ...
Selecting previously unselected package libssl1.0.0:armhf.
Preparing to unpack .../libssl1.0.0_1.0.2d-1_armhf.deb ...
Unpacking libssl1.0.0:armhf (1.0.2d-1) ...
Selecting previously unselected package libpython2.7-stdlib:armhf.
Preparing to unpack .../libpython2.7-stdlib_2.7.10-3_armhf.deb ...
Unpacking libpython2.7-stdlib:armhf (2.7.10-3) ...
Selecting previously unselected package python2.7.
Preparing to unpack .../python2.7_2.7.10-3_armhf.deb ...
Unpacking python2.7 (2.7.10-3) ...
Selecting previously unselected package libpython-stdlib:armhf.
Preparing to unpack .../libpython-stdlib_2.7.9-1_armhf.deb ...
Unpacking libpython-stdlib:armhf (2.7.9-1) ...
Setting up libpython2.7-minimal:armhf (2.7.10-3) ...
Setting up python2.7-minimal (2.7.10-3) ...
Setting up python-minimal (2.7.9-1) ...
Selecting previously unselected package python.
(Reading database ...
(Reading database ... 5%
(Reading database ... 10%
(Reading database ... 15%
(Reading database ... 20%
(Reading database ... 25%
(Reading database ... 30%
(Reading database ... 35%
(Reading database ... 40%
(Reading database ... 45%
(Reading database ... 50%
(Reading database ... 55%
(Reading database ... 60%
(Reading database ... 65%
(Reading database ... 70%
(Reading database ... 75%
(Reading database ... 80%
(Reading database ... 85%
(Reading database ... 90%
(Reading database ... 95%
(Reading database ... 100%
(Reading database ... 13398 files and directories currently installed.)
Preparing to unpack .../python_2.7.9-1_armhf.deb ...
Unpacking python (2.7.9-1) ...
Selecting previously unselected package libglib2.0-0:armhf.
Preparing to unpack .../libglib2.0-0_2.44.1-1.1_armhf.deb ...
Unpacking libglib2.0-0:armhf (2.44.1-1.1) ...
Selecting previously unselected package libcroco3:armhf.
Preparing to unpack .../libcroco3_0.6.8-3_armhf.deb ...
Unpacking libcroco3:armhf (0.6.8-3) ...
Selecting previously unselected package libunistring0:armhf.
Preparing to unpack .../libunistring0_0.9.3-5.2_armhf.deb ...
Unpacking libunistring0:armhf (0.9.3-5.2) ...
Selecting previously unselected package file.
Preparing to unpack .../file_1%3a5.22+15-2_armhf.deb ...
Unpacking file (1:5.22+15-2) ...
Selecting previously unselected package gettext-base.
Preparing to unpack .../gettext-base_0.19.4-1_armhf.deb ...
Unpacking gettext-base (0.19.4-1) ...
Selecting previously unselected package gettext.
Preparing to unpack .../gettext_0.19.4-1_armhf.deb ...
Unpacking gettext (0.19.4-1) ...
Selecting previously unselected package intltool-debian.
Preparing to unpack .../intltool-debian_0.35.0+20060710.2_all.deb ...
Unpacking intltool-debian (0.35.0+20060710.2) ...
Selecting previously unselected package po-debconf.
Preparing to unpack .../po-debconf_1.0.18_all.deb ...
Unpacking po-debconf (1.0.18) ...
Selecting previously unselected package debhelper.
Preparing to unpack .../debhelper_9.20150628_all.deb ...
Unpacking debhelper (9.20150628) ...
Selecting previously unselected package sbuild-build-depends-z3-dummy.
Preparing to unpack .../sbuild-build-depends-z3-dummy.deb ...
Unpacking sbuild-build-depends-z3-dummy (0.invalid.0) ...
Setting up libpipeline1:armhf (1.4.0-1) ...
Setting up groff-base (1.22.3-1) ...
Setting up bsdmainutils (9.0.6) ...
update-alternatives: using /usr/bin/bsd-write to provide /usr/bin/write (write) in auto mode
update-alternatives: using /usr/bin/bsd-from to provide /usr/bin/from (from) in auto mode
Setting up man-db (2.7.0.2-5) ...
Not building database; man-db/auto-update is not 'true'.
Setting up libasprintf0c2:armhf (0.19.4-1) ...
Setting up libmagic1:armhf (1:5.22+15-2) ...
Setting up libxml2:armhf (2.9.1+dfsg1-5) ...
Setting up mime-support (3.58) ...
Setting up libexpat1:armhf (2.1.0-6) ...
Setting up libffi6:armhf (3.2.1-3) ...
Setting up libsqlite3-0:armhf (3.8.10.2-1) ...
Setting up libssl1.0.0:armhf (1.0.2d-1) ...
Setting up libpython2.7-stdlib:armhf (2.7.10-3) ...
Setting up python2.7 (2.7.10-3) ...
Setting up libpython-stdlib:armhf (2.7.9-1) ...
Setting up python (2.7.9-1) ...
Setting up libglib2.0-0:armhf (2.44.1-1.1) ...
No schema files found: doing nothing.
Setting up libcroco3:armhf (0.6.8-3) ...
Setting up libunistring0:armhf (0.9.3-5.2) ...
Setting up file (1:5.22+15-2) ...
Setting up gettext-base (0.19.4-1) ...
Setting up gettext (0.19.4-1) ...
Setting up intltool-debian (0.35.0+20060710.2) ...
Setting up po-debconf (1.0.18) ...
Setting up debhelper (9.20150628) ...
Setting up sbuild-build-depends-z3-dummy (0.invalid.0) ...
Processing triggers for libc-bin (2.19-18) ...
┌──────────────────────────────────────────────────────────────────────────────┐
│ Build environment │
└──────────────────────────────────────────────────────────────────────────────┘
Kernel: Linux 3.19.0-trunk-armmp armhf (armv7l)
Toolchain package versions: binutils_2.25-5 dpkg-dev_1.17.25 g++-4.9_4.9.2-10 gcc-4.9_4.9.2-10 libc6-dev_2.19-18 libstdc++-4.9-dev_4.9.2-10 libstdc++6_4.9.2-10 linux-libc-dev_3.16.7-ckt4-1+rpi1
Package versions: acl_2.2.52-2 adduser_3.113+nmu3 apt_1.0.9.8 base-files_8+rpi1 base-passwd_3.5.37 bash_4.3-11 binutils_2.25-5 bsdmainutils_9.0.6 bsdutils_1:2.25.2-6 build-essential_11.7 bzip2_1.0.6-7 coreutils_8.23-4 cpio_2.11+dfsg-4.1 cpp_4:4.9.2-2 cpp-4.9_4.9.2-10 dash_0.5.7-4 debconf_1.5.56 debconf-i18n_1.5.56 debfoster_2.7-2 debhelper_9.20150628 debianutils_4.4 diffutils_1:3.3-1 dmsetup_2:1.02.90-2.2 dpkg_1.17.25 dpkg-dev_1.17.25 e2fslibs_1.42.12-1.1 e2fsprogs_1.42.12-1.1 fakeroot_1.20.2-1 file_1:5.22+15-2 findutils_4.4.2-9 g++_4:4.9.2-2 g++-4.9_4.9.2-10 gcc_4:4.9.2-2 gcc-4.6-base_4.6.4-5+rpi1 gcc-4.7-base_4.7.3-11+rpi1 gcc-4.8-base_4.8.4-1 gcc-4.9_4.9.2-10 gcc-4.9-base_4.9.2-10 gettext_0.19.4-1 gettext-base_0.19.4-1 gnupg_1.4.18-7 gpgv_1.4.18-7 grep_2.20-4.1 groff-base_1.22.3-1 gzip_1.6-4 hostname_3.15 init_1.22 init-system-helpers_1.22 initramfs-tools_0.120 initscripts_2.88dsf-59 insserv_1.14.0-5 intltool-debian_0.35.0+20060710.2 klibc-utils_2.0.4-2+rpi1 kmod_18-3 libacl1_2.2.52-2 libapt-pkg4.12_1.0.9.8 libasan1_4.9.2-10 libasprintf0c2_0.19.4-1 libatomic1_4.9.2-10 libattr1_1:2.4.47-2 libaudit-common_1:2.4-1 libaudit1_1:2.4-1 libblkid1_2.25.2-6 libbz2-1.0_1.0.6-7 libc-bin_2.19-18 libc-dev-bin_2.19-18 libc6_2.19-18 libc6-dev_2.19-18 libcap2_1:2.24-8 libcap2-bin_1:2.24-8 libcloog-isl4_0.18.2-1 libcomerr2_1.42.12-1.1 libcroco3_0.6.8-3 libcryptsetup4_2:1.6.6-5 libdb5.3_5.3.28-9 libdbus-1-3_1.8.16-1 libdebconfclient0_0.192 libdevmapper1.02.1_2:1.02.90-2.2 libdpkg-perl_1.17.25 libdrm2_2.4.58-2 libexpat1_2.1.0-6 libfakeroot_1.20.2-1 libffi6_3.2.1-3 libgc1c2_1:7.2d-6.4 libgcc-4.9-dev_4.9.2-10 libgcc1_1:4.9.2-10 libgcrypt20_1.6.3-2 libgdbm3_1.8.3-13.1 libglib2.0-0_2.44.1-1.1 libgmp10_2:6.0.0+dfsg-6+rpi1 libgomp1_4.9.2-10 libgpg-error0_1.17-3 libisl10_0.12.2-2 libklibc_2.0.4-2+rpi1 libkmod2_18-3 liblocale-gettext-perl_1.05-8+b1 liblzma5_5.1.1alpha+20120614-2 libmagic1_1:5.22+15-2 libmount1_2.25.2-6 libmpc3_1.0.2-1 libmpfr4_3.1.2-2 libncurses5_5.9+20140913-1 libncursesw5_5.9+20140913-1 libnih-dbus1_1.0.3-4.3 libnih1_1.0.3-4.3 libpam-modules_1.1.8-3.1 libpam-modules-bin_1.1.8-3.1 libpam-runtime_1.1.8-3.1 libpam0g_1.1.8-3.1 libpcre3_2:8.35-3.3 libpipeline1_1.4.0-1 libpng12-0_1.2.50-2 libprocps3_2:3.3.9-9 libpython-stdlib_2.7.9-1 libpython2.7-minimal_2.7.10-3 libpython2.7-stdlib_2.7.10-3 libreadline6_6.3-8 libselinux1_2.3-2 libsemanage-common_2.3-1 libsemanage1_2.3-1 libsepol1_2.3-2 libslang2_2.3.0-2 libsmartcols1_2.25.2-6 libsqlite3-0_3.8.10.2-1 libss2_1.42.12-1.1 libssl1.0.0_1.0.2d-1 libstdc++-4.9-dev_4.9.2-10 libstdc++6_4.9.2-10 libsystemd0_215-17 libtext-charwidth-perl_0.04-7+b4 libtext-iconv-perl_1.7-5+b5 libtext-wrapi18n-perl_0.06-7 libtimedate-perl_2.3000-2 libtinfo5_5.9+20140913-1 libubsan0_4.9.2-10 libudev1_215-17 libunistring0_0.9.3-5.2 libusb-0.1-4_2:0.1.12-25 libustr-1.0-1_1.0.4-3 libuuid1_2.25.2-6 libxml2_2.9.1+dfsg1-5 linux-libc-dev_3.16.7-ckt4-1+rpi1 login_1:4.2-3 lsb-base_4.1+Debian13+rpi1+nmu1 make_4.0-8.1 makedev_2.3.1-93 man-db_2.7.0.2-5 mawk_1.3.3-17 mime-support_3.58 mount_2.25.2-6 mountall_2.54 multiarch-support_2.19-18 ncurses-base_5.9+20140913-1 ncurses-bin_5.9+20140913-1 passwd_1:4.2-3 patch_2.7.5-1 perl_5.20.2-3 perl-base_5.20.2-3 perl-modules_5.20.2-3 plymouth_0.9.0-9 po-debconf_1.0.18 procps_2:3.3.9-9 python_2.7.9-1 python-minimal_2.7.9-1 python2.7_2.7.10-3 python2.7-minimal_2.7.10-3 raspbian-archive-keyring_20120528.2 readline-common_6.3-8 sbuild-build-depends-core-dummy_0.invalid.0 sbuild-build-depends-z3-dummy_0.invalid.0 sed_4.2.2-4 sensible-utils_0.0.9 startpar_0.59-3 systemd_215-17 systemd-sysv_215-17 sysv-rc_2.88dsf-59 sysvinit-utils_2.88dsf-59 tar_1.27.1-2 tzdata_2015c-1 udev_215-17 util-linux_2.25.2-6 xz-utils_5.1.1alpha+20120614-2 zlib1g_1:1.2.8.dfsg-2
┌──────────────────────────────────────────────────────────────────────────────┐
│ Build │
└──────────────────────────────────────────────────────────────────────────────┘
Unpack source
─────────────
gpgv: keyblock resource `/sbuild-nonexistent/.gnupg/trustedkeys.gpg': file open error
gpgv: Signature made Tue Jul 7 08:37:18 2015 UTC using RSA key ID 36ECA931
gpgv: Can't check signature: public key not found
dpkg-source: warning: failed to verify signature on ./z3_4.4.0-2.dsc
dpkg-source: info: extracting z3 in z3-4.4.0
dpkg-source: info: unpacking z3_4.4.0.orig.tar.gz
dpkg-source: info: unpacking z3_4.4.0-2.debian.tar.xz
dpkg-source: info: applying fix_conflict
dpkg-source: info: applying disable_test
dpkg-source: info: applying disable_test2
dpkg-source: info: applying emmintrin
Check disc space
────────────────
Sufficient free space for build
User Environment
────────────────
DEB_BUILD_OPTIONS=parallel=4
HOME=/sbuild-nonexistent
LOGNAME=buildd
PATH=/usr/local/sbin:/usr/local/bin:/usr/sbin:/usr/bin:/sbin:/bin:/usr/games
SCHROOT_ALIAS_NAME=stretch-staging-armhf-sbuild
SCHROOT_CHROOT_NAME=stretch-staging-armhf-sbuild
SCHROOT_COMMAND=env
SCHROOT_GID=109
SCHROOT_GROUP=buildd
SCHROOT_SESSION_ID=stretch-staging-armhf-sbuild-9e196be8-8e33-4369-bd97-f88caee86d43
SCHROOT_UID=104
SCHROOT_USER=buildd
SHELL=/bin/sh
USER=buildd
dpkg-buildpackage
─────────────────
dpkg-buildpackage: source package z3
dpkg-buildpackage: source version 4.4.0-2
dpkg-buildpackage: source distribution unstable
dpkg-source --before-build z3-4.4.0
dpkg-buildpackage: host architecture armhf
fakeroot debian/rules clean
dh clean --parallel --with python2
dh_testdir -O--parallel
dh_auto_clean -O--parallel
debian/rules override_dh_clean
make[1]: Entering directory '/«PKGBUILDDIR»'
dh_clean
rm -f Makefile scripts/*.pyc
rm -f -r build
rm -f src/api/python/*.pyc
rm -f \
src/api/api_commands.cpp \
src/api/api_log_macros.cpp \
src/api/api_log_macros.h \
src/api/dll/gparams_register_modules.cpp \
src/api/dll/install_tactic.cpp \
src/api/dll/mem_initializer.cpp \
src/api/dotnet/Enumerations.cs \
src/api/dotnet/Native.cs \
src/api/dotnet/Properties/AssemblyInfo.cs \
src/api/python/z3consts.py \
src/api/python/z3core.py \
src/ast/fpa/fpa2bv_rewriter_params.hpp \
src/ast/normal_forms/nnf_params.hpp \
src/ast/pattern/database.h \
src/ast/pattern/pattern_inference_params_helper.hpp \
src/ast/pp_params.hpp \
src/ast/rewriter/arith_rewriter_params.hpp \
src/ast/rewriter/array_rewriter_params.hpp \
src/ast/rewriter/bool_rewriter_params.hpp \
src/ast/rewriter/bv_rewriter_params.hpp \
src/ast/rewriter/fpa_rewriter_params.hpp \
src/ast/rewriter/poly_rewriter_params.hpp \
src/ast/rewriter/rewriter_params.hpp \
src/ast/simplifier/arith_simplifier_params_helper.hpp \
src/ast/simplifier/array_simplifier_params_helper.hpp \
src/ast/simplifier/bv_simplifier_params_helper.hpp \
src/interp/interp_params.hpp \
src/math/polynomial/algebraic_params.hpp \
src/math/realclosure/rcf_params.hpp \
src/model/model_evaluator_params.hpp \
src/model/model_params.hpp \
src/muz/base/fixedpoint_params.hpp \
src/nlsat/nlsat_params.hpp \
src/parsers/util/parser_params.hpp \
src/sat/sat_asymm_branch_params.hpp \
src/sat/sat_params.hpp \
src/sat/sat_scc_params.hpp \
src/sat/sat_simplifier_params.hpp \
src/shell/gparams_register_modules.cpp \
src/shell/install_tactic.cpp \
src/shell/mem_initializer.cpp \
src/smt/params/smt_params_helper.hpp \
src/solver/combined_solver_params.hpp \
src/tactic/sls/sls_params.hpp \
src/test/gparams_register_modules.cpp \
src/test/install_tactic.cpp \
src/test/mem_initializer.cpp \
src/util/version.h \
src/opt/opt_params.hpp
make[1]: Leaving directory '/«PKGBUILDDIR»'
debian/rules build-arch
dh build-arch --parallel --with python2
dh_testdir -a -O--parallel
debian/rules override_dh_auto_configure
make[1]: Entering directory '/«PKGBUILDDIR»'
python scripts/mk_make.py --prefix=/«PKGBUILDDIR»/debian/tmp/usr
opt = --prefix, arg = /«PKGBUILDDIR»/debian/tmp/usr
New component: 'util'
New component: 'polynomial'
New component: 'sat'
New component: 'nlsat'
New component: 'hilbert'
New component: 'simplex'
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: '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: 'ddnf'
New component: 'duality_intf'
New component: 'fp'
New component: 'nlsat_smt_tactic'
New component: 'smtlogic_tactics'
New component: 'fpa_tactics'
New component: 'ufbv_tactic'
New component: 'portfolio'
New component: 'smtparser'
New component: 'opt'
New component: 'api'
New component: 'shell'
New component: 'test'
New component: 'api_dll'
New component: 'dotnet'
New component: 'java'
New component: 'ml'
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: 'ml_example'
New component: 'py_example'
Generated 'src/util/version.h'
Updated 'src/api/dotnet/Properties/AssemblyInfo'
Generated 'src/ast/pp_params.hpp'
Generated 'src/ast/fpa/fpa2bv_rewriter_params.hpp'
Generated 'src/ast/pattern/pattern_inference_params_helper.hpp'
Generated 'src/ast/normal_forms/nnf_params.hpp'
Generated 'src/ast/simplifier/arith_simplifier_params_helper.hpp'
Generated 'src/ast/simplifier/bv_simplifier_params_helper.hpp'
Generated 'src/ast/simplifier/array_simplifier_params_helper.hpp'
Generated 'src/ast/rewriter/bv_rewriter_params.hpp'
Generated 'src/ast/rewriter/fpa_rewriter_params.hpp'
Generated 'src/ast/rewriter/array_rewriter_params.hpp'
Generated 'src/ast/rewriter/poly_rewriter_params.hpp'
Generated 'src/ast/rewriter/arith_rewriter_params.hpp'
Generated 'src/ast/rewriter/rewriter_params.hpp'
Generated 'src/ast/rewriter/bool_rewriter_params.hpp'
Generated 'src/muz/base/fixedpoint_params.hpp'
Generated 'src/solver/combined_solver_params.hpp'
Generated 'src/tactic/sls/sls_params.hpp'
Generated 'src/interp/interp_params.hpp'
Generated 'src/nlsat/nlsat_params.hpp'
Generated 'src/opt/opt_params.hpp'
Generated 'src/sat/sat_scc_params.hpp'
Generated 'src/sat/sat_params.hpp'
Generated 'src/sat/sat_simplifier_params.hpp'
Generated 'src/sat/sat_asymm_branch_params.hpp'
Generated 'src/parsers/util/parser_params.hpp'
Generated 'src/math/realclosure/rcf_params.hpp'
Generated 'src/math/polynomial/algebraic_params.hpp'
Generated 'src/model/model_params.hpp'
Generated 'src/model/model_evaluator_params.hpp'
Generated 'src/smt/params/smt_params_helper.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 'z3types.py'
Copied 'z3rcf.py'
Copied 'z3poly.py'
Copied 'z3test.py'
Copied 'z3util.py'
Copied 'z3num.py'
Copied 'z3printer.py'
Copied 'z3.py'
Copied 'z3consts.py'
Copied 'z3core.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'
Testing ar...
Testing g++...
Testing gcc...
Testing floating point support...
Testing OpenMP...
Host platform: Linux
C++ Compiler: g++
C Compiler : gcc
Arithmetic: internal
OpenMP: True
Prefix: /«PKGBUILDDIR»/debian/tmp/usr
64-bit: False
FP math: ARM-VFP
Python version: 2.7
Writing build/Makefile
Copied Z3Py example 'example.py' to 'build'
Makefile was successfully generated.
python packages dir: /«PKGBUILDDIR»/debian/tmp/usr/lib/python2.7/dist-packages
compilation mode: Release
Type 'cd build; make' to build Z3
sed -i 's/^SLINK_FLAGS=.*/SLINK_FLAGS=-shared -Wl,-z,relro -Wl,-soname,libz3.so.4/' build/config.mk
sed -i 's/^CXXFLAGS=/CXXFLAGS=-fPIC /' build/config.mk
printf '%%:\n\t$(MAKE) -C build $@\n' > Makefile
printf '\nall:\n\t$(MAKE) -C build $@\n' >> Makefile
make[1]: Leaving directory '/«PKGBUILDDIR»'
dh_auto_build -a -O--parallel
make -j4
make[1]: Entering directory '/«PKGBUILDDIR»'
make -C build all
make[2]: Entering directory '/«PKGBUILDDIR»/build'
src/smt/smt_statistics.cpp
src/interp/iz3profiling.cpp
src/util/luby.cpp
src/util/scoped_ctrl_c.cpp
src/util/approx_nat.cpp
src/util/common_msgs.cpp
src/api/dll/dll.cpp
src/util/timeit.cpp
src/util/cooperate.cpp
src/util/memory_manager.cpp
src/util/approx_set.cpp
src/util/z3_exception.cpp
src/api/api_commands.cpp
src/util/util.cpp
src/util/timeout.cpp
src/util/bit_util.cpp
src/util/mpn.cpp
src/util/page.cpp
src/util/lbool.cpp
src/util/stack.cpp
src/util/timer.cpp
src/util/scoped_timer.cpp
src/shell/z3_log_frontend.cpp
src/api/api_log.cpp
src/util/fixed_bit_vector.cpp
src/util/hash.cpp
src/api/z3_replayer.cpp
src/api/api_log_macros.cpp
src/interp/iz3scopes.cpp
src/util/prime_generator.cpp
src/util/debug.cpp
src/util/smt2_util.cpp
src/util/cmd_context_types.cpp
src/util/symbol.cpp
src/util/trace.cpp
src/util/small_object_allocator.cpp
src/util/warning.cpp
src/util/region.cpp
src/util/statistics.cpp
src/util/permutation.cpp
src/util/bit_vector.cpp
src/sat/sat_clause.cpp
src/sat/sat_model_converter.cpp
src/sat/sat_clause_set.cpp
src/sat/sat_config.cpp
src/sat/sat_watched.cpp
src/sat/sat_clause_use_list.cpp
src/util/gparams.cpp
src/util/env_params.cpp
src/util/mpz.cpp
src/smt/params/dyn_ack_params.cpp
src/smt/params/theory_arith_params.cpp
src/smt/params/theory_bv_params.cpp
src/smt/params/qi_params.cpp
src/smt/params/theory_pb_params.cpp
src/ast/pattern/pattern_inference_params.cpp
src/ast/simplifier/array_simplifier_params.cpp
src/ast/simplifier/bv_simplifier_params.cpp
src/ast/simplifier/arith_simplifier_params.cpp
src/math/euclid/euclidean_solver.cpp
src/math/realclosure/mpz_matrix.cpp
src/math/interval/interval_mpq.cpp
src/util/mpq.cpp
src/util/mpff.cpp
src/util/mpfx.cpp
src/util/mpf.cpp
src/util/mpq_inf.cpp
src/util/hwf.cpp
src/shell/mem_initializer.cpp
src/smt/old_interval.cpp
src/smt/params/preprocessor_params.cpp
src/smt/params/theory_array_params.cpp
src/tactic/arith/linear_equation.cpp
src/math/subpaving/subpaving.cpp
src/math/subpaving/subpaving_mpf.cpp
src/math/subpaving/subpaving_mpfx.cpp
src/math/realclosure/realclosure.cpp
src/util/mpbq.cpp
src/util/rational.cpp
src/util/s_integer.cpp
src/util/params.cpp
src/util/inf_int_rational.cpp
src/util/sexpr.cpp
src/api/dll/mem_initializer.cpp
src/muz/rel/tbv.cpp
src/muz/base/bind_variables.cpp
src/qe/qe_util.cpp
src/smt/user_plugin/user_decl_plugin.cpp
src/smt/smt_quantifier_stat.cpp
src/smt/smt_value_sort.cpp
src/smt/proto_model/value_factory.cpp
src/smt/params/smt_params.cpp
src/ast/simplifier/simplifier_plugin.cpp
src/ast/simplifier/basic_simplifier_plugin.cpp
src/ast/simplifier/datatype_simplifier_plugin.cpp
src/cmd_context/pdecl.cpp
src/math/subpaving/tactic/expr2subpaving.cpp
src/tactic/arith/bound_propagator.cpp
src/parsers/util/simple_parser.cpp
src/parsers/util/scanner.cpp
../src/parsers/util/scanner.cpp: In member function 'scanner::token scanner::scan()':
../src/parsers/util/scanner.cpp:483:15: warning: case label value is less than minimum value for type
case -1:
^
src/ast/rewriter/expr_safe_replace.cpp
src/ast/rewriter/fpa_rewriter.cpp
src/ast/rewriter/datatype_rewriter.cpp
src/ast/ast_lt.cpp
src/ast/format.cpp
src/ast/pp.cpp
src/ast/decl_collector.cpp
src/ast/reg_decl_plugins.cpp
src/ast/num_occurs.cpp
src/ast/used_vars.cpp
src/ast/ast_smt_pp.cpp
src/ast/ast_util.cpp
src/ast/expr_abstract.cpp
src/ast/for_each_expr.cpp
src/ast/func_decl_dependencies.cpp
src/ast/expr_substitution.cpp
src/ast/expr_map.cpp
src/ast/ast_translation.cpp
src/ast/act_cache.cpp
src/ast/pb_decl_plugin.cpp
src/ast/expr_stat.cpp
src/ast/has_free_vars.cpp
src/ast/occurs.cpp
src/ast/seq_decl_plugin.cpp
src/ast/ast_ll_pp.cpp
src/ast/expr_functors.cpp
src/ast/for_each_ast.cpp
src/ast/fpa_decl_plugin.cpp
src/math/subpaving/subpaving_mpff.cpp
src/math/subpaving/subpaving_mpq.cpp
src/math/subpaving/subpaving_hwf.cpp
src/math/simplex/simplex.cpp
src/math/hilbert/hilbert_basis.cpp
src/sat/sat_probing.cpp
src/sat/sat_cleaner.cpp
src/sat/sat_solver.cpp
src/sat/sat_asymm_branch.cpp
src/sat/sat_simplifier.cpp
src/sat/sat_bceq.cpp
src/sat/sat_iff3_finder.cpp
src/sat/sat_elim_eqs.cpp
src/sat/sat_scc.cpp
src/sat/dimacs.cpp
src/sat/sat_sls.cpp
src/sat/sat_integrity_checker.cpp
src/sat/sat_mus.cpp
src/util/inf_s_integer.cpp
src/util/inf_rational.cpp
src/api/dll/gparams_register_modules.cpp
src/shell/main.cpp
src/shell/dimacs_frontend.cpp
src/shell/gparams_register_modules.cpp
src/opt/hitting_sets.cpp
src/smt/cost_evaluator.cpp
src/smt/uses_theory.cpp
src/ast/fpa/fpa2bv_converter.cpp
src/ast/simplifier/distribute_forall.cpp
src/ast/simplifier/fpa_simplifier_plugin.cpp
src/cmd_context/tactic_manager.cpp
src/parsers/util/cost_parser.cpp
src/tactic/proof_converter.cpp
src/ast/normal_forms/name_exprs.cpp
src/ast/normal_forms/nnf.cpp
src/ast/rewriter/mk_simplified_app.cpp
src/ast/rewriter/dl_rewriter.cpp
src/ast/rewriter/expr_replacer.cpp
src/ast/rewriter/bool_rewriter.cpp
src/ast/rewriter/bv_rewriter.cpp
src/ast/rewriter/rewriter.cpp
src/ast/rewriter/th_rewriter.cpp
src/ast/ast_printer.cpp
src/ast/macro_substitution.cpp
src/ast/expr2var.cpp
src/ast/shared_occs.cpp
src/ast/datatype_decl_plugin.cpp
src/nlsat/nlsat_types.cpp
src/math/polynomial/polynomial_cache.cpp
src/parsers/smt/smtparser.cpp
src/parsers/smt/smtlib.cpp
src/smt/user_plugin/user_simplifier_plugin.cpp
src/smt/arith_eq_solver.cpp
src/smt/smt_literal.cpp
src/smt/smt_farkas_util.cpp
src/smt/fingerprints.cpp
src/smt/proto_model/numeral_factory.cpp
src/ast/simplifier/bit2int.cpp
src/ast/simplifier/bv_simplifier_plugin.cpp
src/ast/simplifier/arith_simplifier_plugin.cpp
src/ast/simplifier/poly_simplifier_plugin.cpp
src/ast/simplifier/inj_axiom.cpp
src/ast/proof_checker/proof_checker.cpp
src/cmd_context/check_logic.cpp
src/interp/iz3mgr.cpp
src/tactic/aig/aig.cpp
src/tactic/arith/bv2real_rewriter.cpp
src/tactic/arith/probe_arith.cpp
src/tactic/arith/bound_manager.cpp
src/sat/tactic/atom2bool_var.cpp
src/math/grobner/grobner.cpp
src/parsers/util/pattern_validation.cpp
src/ast/substitution/substitution_tree.cpp
src/ast/substitution/substitution.cpp
src/ast/substitution/unifier.cpp
src/ast/substitution/matcher.cpp
src/tactic/replace_proof_converter.cpp
src/tactic/equiv_proof_converter.cpp
src/tactic/goal.cpp
src/tactic/goal_util.cpp
src/tactic/probe.cpp
src/tactic/goal_num_occurs.cpp
src/tactic/goal_shared_occs.cpp
src/model/func_interp.cpp
src/model/model_v2_pp.cpp
src/model/model_pp.cpp
src/model/model_smt2_pp.cpp
src/model/model_core.cpp
src/ast/normal_forms/defined_names.cpp
src/ast/normal_forms/pull_quant.cpp
src/ast/rewriter/quant_hoist.cpp
src/ast/rewriter/arith_rewriter.cpp
src/ast/rewriter/factor_rewriter.cpp
src/ast/rewriter/ast_counter.cpp
src/ast/rewriter/var_subst.cpp
src/ast/rewriter/pb_rewriter.cpp
src/ast/rewriter/array_rewriter.cpp
src/ast/rewriter/der.cpp
src/ast/static_features.cpp
src/ast/dl_decl_plugin.cpp
src/ast/ast_smt2_pp.cpp
src/ast/arith_decl_plugin.cpp
src/ast/well_sorted.cpp
src/ast/expr2polynomial.cpp
src/ast/array_decl_plugin.cpp
src/ast/ast.cpp
src/ast/bv_decl_plugin.cpp
src/nlsat/nlsat_interval_set.cpp
src/nlsat/nlsat_clause.cpp
src/math/polynomial/upolynomial.cpp
src/math/polynomial/rpolynomial.cpp
src/math/polynomial/sexpr2upolynomial.cpp
src/math/polynomial/algebraic_numbers.cpp
src/math/polynomial/polynomial_factorization.cpp
src/tactic/ufbv/ufbv_rewriter.cpp
src/smt/smt_almost_cg_table.cpp
src/smt/theory_opt.cpp
src/smt/cached_var_subst.cpp
src/smt/watch_list.cpp
src/smt/smt_cg_table.cpp
src/smt/smt_clause.cpp
src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp
src/ast/rewriter/bit_blaster/bit_blaster.cpp
src/interp/iz3pp.cpp
src/tactic/arith/bv2int_rewriter.cpp
src/model/model2expr.cpp
src/model/model_implicant.cpp
src/model/model.cpp
src/model/model_evaluator.cpp
src/math/polynomial/polynomial.cpp
src/math/polynomial/upolynomial_factorization.cpp
src/api/api_arith.cpp
src/api/api_ast_vector.cpp
src/api/api_stats.cpp
src/api/api_model.cpp
src/api/api_ast.cpp
src/api/api_bv.cpp
src/api/api_solver_old.cpp
src/opt/pb_sls.cpp
src/tactic/ufbv/ufbv_rewriter_tactic.cpp
src/tactic/fpa/fpa2bv_model_converter.cpp
src/muz/pdr/pdr_sym_mux.cpp
src/muz/rel/doc.cpp
src/muz/base/dl_boogie_proof.cpp
src/qe/qe_arith.cpp
src/qe/nlarith_util.cpp
src/qe/vsubst_tactic.cpp
src/qe/qe_bool_plugin.cpp
src/qe/qe_array_plugin.cpp
src/qe/qe_arith_plugin.cpp
src/qe/qe_bv_plugin.cpp
src/qe/qe_dl_plugin.cpp
src/qe/qe_lite.cpp
src/qe/qe_datatype_plugin.cpp
../src/qe/qe_lite.cpp: In member function 'fm::constraint* fm::fm::resolve(const fm::constraint&, const fm::constraint&, fm::var)':
../src/qe/qe_lite.cpp:2067:23: warning: case label value is less than minimum value for type
case -1:
^
src/tactic/bv/bv1_blaster_tactic.cpp
src/tactic/bv/bit_blaster_model_converter.cpp
src/tactic/bv/bit_blaster_tactic.cpp
src/tactic/bv/max_bv_sharing_tactic.cpp
src/smt/expr_context_simplifier.cpp
src/ast/simplifier/elim_bounds.cpp
src/ast/simplifier/pull_ite_tree.cpp
src/ast/simplifier/simplifier.cpp
src/ast/simplifier/push_app_ite.cpp
src/ast/simplifier/array_simplifier_plugin.cpp
src/ast/simplifier/bv_elim.cpp
src/interp/iz3proof_itp.cpp
src/solver/check_sat_result.cpp
src/tactic/aig/aig_tactic.cpp
src/tactic/arith/arith_bounds_tactic.cpp
src/tactic/arith/diff_neq_tactic.cpp
src/tactic/arith/elim01_tactic.cpp
src/tactic/arith/card2bv_tactic.cpp
src/tactic/arith/fix_dl_var_tactic.cpp
src/tactic/arith/add_bounds_tactic.cpp
src/tactic/arith/factor_tactic.cpp
src/tactic/arith/lia2card_tactic.cpp
src/tactic/core/pb_preprocess_tactic.cpp
src/tactic/core/solve_eqs_tactic.cpp
src/tactic/core/cofactor_term_ite_tactic.cpp
src/tactic/core/propagate_values_tactic.cpp
src/tactic/core/der_tactic.cpp
src/tactic/core/split_clause_tactic.cpp
src/tactic/core/distribute_forall_tactic.cpp
src/tactic/core/cofactor_elim_term_ite.cpp
src/tactic/core/symmetry_reduce_tactic.cpp
src/tactic/horn_subsume_model_converter.cpp
src/tactic/extension_model_converter.cpp
src/tactic/tactic.cpp
src/tactic/tactical.cpp
src/tactic/model_converter.cpp
src/nlsat/nlsat_explain.cpp
src/nlsat/nlsat_solver.cpp
src/nlsat/nlsat_evaluator.cpp
src/api/api_rcf.cpp
src/api/api_datatype.cpp
src/api/api_quant.cpp
src/api/api_context.cpp
src/api/api_ast_map.cpp
src/api/api_fpa.cpp
src/api/api_algebraic.cpp
src/api/api_polynomial.cpp
src/api/api_numeral.cpp
src/api/api_array.cpp
src/api/api_goal.cpp
src/api/api_params.cpp
src/api/api_pb.cpp
src/api/api_tactic.cpp
src/api/api_user_theory.cpp
src/api/api_config_params.cpp
src/opt/mus.cpp
src/opt/opt_pareto.cpp
src/opt/mss.cpp
src/opt/inc_sat_solver.cpp
src/parsers/smt/smtlib_solver.cpp
src/tactic/portfolio/smt_strategic_solver.cpp
src/tactic/portfolio/default_tactic.cpp
src/tactic/ufbv/ufbv_tactic.cpp
src/tactic/fpa/fpa2bv_converter_prec.cpp
src/tactic/fpa/fpa2bv_approx_tactic.cpp
src/tactic/fpa/fpa2bv_tactic.cpp
src/tactic/fpa/qffp_tactic.cpp
src/tactic/smtlogics/qfufnra_tactic.cpp
src/tactic/smtlogics/qfbv_tactic.cpp
src/tactic/smtlogics/qfauflia_tactic.cpp
src/tactic/smtlogics/qfuf_tactic.cpp
src/tactic/smtlogics/qfufbv_tactic.cpp
src/tactic/smtlogics/quant_tactics.cpp
src/tactic/smtlogics/qfnra_tactic.cpp
src/tactic/smtlogics/qfaufbv_tactic.cpp
src/tactic/smtlogics/qflra_tactic.cpp
src/tactic/smtlogics/qfnia_tactic.cpp
src/tactic/smtlogics/qflia_tactic.cpp
src/tactic/smtlogics/nra_tactic.cpp
src/tactic/smtlogics/qfidl_tactic.cpp
src/tactic/nlsat_smt/nl_purify_tactic.cpp
src/muz/pdr/pdr_farkas_learner.cpp
src/muz/pdr/pdr_smt_context_manager.cpp
src/muz/base/proof_utils.cpp
src/muz/base/hnf.cpp
src/duality/duality_profiling.cpp
src/duality/duality_wrapper.cpp
src/qe/qe_tactic.cpp
src/qe/qe_cmd.cpp
src/qe/qe_sat_tactic.cpp
src/smt/tactic/ctx_solver_simplify_tactic.cpp
src/smt/tactic/smt_tactic.cpp
src/tactic/bv/bv_size_reduction_tactic.cpp
src/smt/elim_term_ite.cpp
src/smt/smt_implied_equalities.cpp
src/smt/proto_model/proto_model.cpp
src/smt/proto_model/struct_factory.cpp
src/smt/proto_model/datatype_factory.cpp
src/smt/proto_model/array_factory.cpp
src/ast/pattern/pattern_inference.cpp
src/ast/macros/macro_util.cpp
src/ast/simplifier/maximise_ac_sharing.cpp
src/cmd_context/extra_cmds/dbg_cmds.cpp
src/cmd_context/extra_cmds/polynomial_cmds.cpp
src/cmd_context/extra_cmds/subpaving_cmds.cpp
src/cmd_context/cmd_util.cpp
src/cmd_context/cmd_context_to_goal.cpp
src/cmd_context/context_params.cpp
src/cmd_context/tactic_cmds.cpp
src/cmd_context/eval_cmd.cpp
src/cmd_context/echo_tactic.cpp
src/cmd_context/parametric_cmd.cpp
src/cmd_context/interpolant_cmds.cpp
src/cmd_context/simplify_cmd.cpp
src/cmd_context/basic_cmds.cpp
src/cmd_context/cmd_context.cpp
src/interp/iz3proof.cpp
src/interp/iz3base.cpp
src/interp/iz3checker.cpp
src/interp/iz3foci.cpp
src/interp/iz3translate.cpp
src/interp/iz3translate_direct.cpp
src/solver/solver.cpp
src/solver/combined_solver.cpp
src/math/subpaving/tactic/subpaving_tactic.cpp
src/nlsat/tactic/nlsat_tactic.cpp
src/nlsat/tactic/goal2nlsat.cpp
src/nlsat/tactic/qfnra_nlsat_tactic.cpp
src/tactic/arith/lia2pb_tactic.cpp
src/tactic/arith/recover_01_tactic.cpp
src/tactic/arith/normalize_bounds_tactic.cpp
src/tactic/arith/pb2bv_model_converter.cpp
src/tactic/arith/fm_tactic.cpp
src/tactic/arith/nla2bv_tactic.cpp
../src/tactic/arith/fm_tactic.cpp: In member function 'fm_tactic::constraint* fm_tactic::imp::resolve(const fm_tactic::constraint&, const fm_tactic::constraint&, fm_tactic::var)':
../src/tactic/arith/fm_tactic.cpp:1398:23: warning: case label value is less than minimum value for type
case -1:
^
src/tactic/arith/pb2bv_tactic.cpp
src/tactic/arith/degree_shift_tactic.cpp
src/tactic/arith/purify_arith_tactic.cpp
src/tactic/arith/propagate_ineqs_tactic.cpp
src/sat/tactic/sat_tactic.cpp
src/sat/tactic/goal2sat.cpp
src/tactic/core/nnf_tactic.cpp
src/tactic/core/blast_term_ite_tactic.cpp
src/tactic/core/ctx_simplify_tactic.cpp
src/tactic/core/elim_term_ite_tactic.cpp
src/tactic/core/tseitin_cnf_tactic.cpp
src/tactic/core/elim_uncnstr_tactic.cpp
src/tactic/core/simplify_tactic.cpp
src/tactic/core/occf_tactic.cpp
src/tactic/core/reduce_args_tactic.cpp
src/tactic/filter_model_converter.cpp
src/api/dll/install_tactic.cpp
src/shell/install_tactic.cpp
src/api/api_parsers.cpp
src/api/api_solver.cpp
src/api/api_interp.cpp
src/duality/duality_solver.cpp
src/duality/duality_rpfp.cpp
src/tactic/sls/sls_tactic.cpp
src/tactic/sls/sls_engine.cpp
src/smt/smt_solver.cpp
src/ast/pattern/expr_pattern_match.cpp
src/ast/macros/macro_manager.cpp
src/ast/macros/quasi_macros.cpp
src/parsers/smt2/smt2scanner.cpp
../src/parsers/smt2/smt2scanner.cpp: In member function 'smt2::scanner::token smt2::scanner::scan()':
../src/parsers/smt2/smt2scanner.cpp:335:19: warning: case label value is less than minimum value for type
case -1:
^
src/parsers/smt2/smt2parser.cpp
src/interp/iz3interp.cpp
src/solver/tactic2solver.cpp
src/solver/solver_na2as.cpp
src/shell/smtlib_frontend.cpp
src/tactic/ufbv/macro_finder_tactic.cpp
src/tactic/ufbv/quasi_macros_tactic.cpp
src/muz/pdr/pdr_util.cpp
src/muz/pdr/pdr_manager.cpp
src/muz/pdr/pdr_prop_solver.cpp
src/muz/pdr/pdr_reachable_cache.cpp
src/tactic/sls/bvsls_opt_engine.cpp
src/ast/macros/macro_finder.cpp
src/opt/optsmt.cpp
src/smt/asserted_formulas.cpp
src/opt/opt_solver.cpp
src/muz/fp/datalog_parser.cpp
src/muz/ddnf/ddnf.cpp
src/muz/bmc/dl_bmc_engine.cpp
src/muz/tab/tab_context.cpp
src/muz/clp/clp_context.cpp
src/muz/pdr/pdr_closure.cpp
src/muz/transforms/dl_mk_magic_symbolic.cpp
src/muz/transforms/dl_mk_karr_invariants.cpp
src/muz/transforms/dl_mk_coi_filter.cpp
src/muz/transforms/dl_mk_unbound_compressor.cpp
src/muz/transforms/dl_mk_separate_negated_tails.cpp
src/muz/transforms/dl_mk_loop_counter.cpp
src/muz/transforms/dl_mk_rule_inliner.cpp
src/muz/transforms/dl_mk_filter_rules.cpp
src/muz/transforms/dl_mk_quantifier_instantiation.cpp
src/muz/transforms/dl_mk_slice.cpp
src/muz/transforms/dl_mk_bit_blast.cpp
src/muz/transforms/dl_mk_magic_sets.cpp
src/muz/transforms/dl_mk_backwards.cpp
src/muz/transforms/dl_mk_scale.cpp
src/muz/transforms/dl_mk_interp_tail_simplifier.cpp
src/muz/transforms/dl_mk_array_blast.cpp
src/muz/transforms/dl_mk_quantifier_abstraction.cpp
src/muz/base/dl_rule.cpp
src/muz/base/dl_rule_subsumption_index.cpp
src/muz/base/dl_rule_set.cpp
src/muz/base/dl_util.cpp
src/muz/base/dl_rule_transformer.cpp
src/muz/base/dl_costs.cpp
src/muz/base/rule_properties.cpp
src/muz/base/dl_context.cpp
src/qe/qe.cpp
src/smt/tactic/unit_subsumption_tactic.cpp
src/smt/user_plugin/user_smt_theory.cpp
src/smt/theory_wmaxsat.cpp
src/smt/theory_bv.cpp
src/smt/theory_datatype.cpp
src/smt/smt_quick_checker.cpp
src/smt/smt_context_stat.cpp
src/smt/theory_array_full.cpp
src/smt/smt_checker.cpp
src/smt/smt_context_pp.cpp
src/smt/theory_fpa.cpp
src/smt/smt_model_checker.cpp
src/smt/smt_model_generator.cpp
src/smt/mam.cpp
src/smt/smt_context_inv.cpp
src/smt/arith_eq_adapter.cpp
src/smt/smt_kernel.cpp
src/smt/smt_justification.cpp
src/smt/theory_array_base.cpp
src/smt/theory_pb.cpp
src/smt/theory_dl.cpp
src/smt/dyn_ack.cpp
src/smt/smt_enode.cpp
src/smt/theory_dummy.cpp
src/smt/smt_theory.cpp
src/smt/smt_internalizer.cpp
src/smt/smt_case_split_queue.cpp
src/smt/smt_conflict_resolution.cpp
src/smt/qi_queue.cpp
src/smt/theory_array.cpp
src/smt/smt_relevancy.cpp
src/smt/smt_model_finder.cpp
src/smt/smt_setup.cpp
src/smt/smt_for_each_relevant_expr.cpp
src/smt/smt_context.cpp
src/smt/smt_quantifier.cpp
src/muz/fp/horn_tactic.cpp
src/muz/pdr/pdr_dl_interface.cpp
src/muz/pdr/pdr_context.cpp
src/muz/pdr/pdr_generalizers.cpp
src/muz/transforms/dl_transforms.cpp
src/muz/transforms/dl_mk_coalesce.cpp
src/muz/transforms/dl_mk_subsumption_checker.cpp
src/muz/transforms/dl_mk_unfold.cpp
src/smt/theory_diff_logic.cpp
src/smt/theory_dense_diff_logic.cpp
src/smt/theory_utvpi.cpp
src/api/api_opt.cpp
src/opt/wmax.cpp
src/opt/opt_cmds.cpp
src/opt/maxhs.cpp
src/opt/opt_context.cpp
src/opt/bcd2.cpp
src/opt/maxsmt.cpp
src/opt/fu_malik.cpp
src/opt/maxsls.cpp
src/opt/maxres.cpp
src/muz/fp/dl_register_engine.cpp
src/muz/duality/duality_dl_interface.cpp
src/muz/rel/dl_mk_similarity_compressor.cpp
src/muz/rel/dl_table_relation.cpp
src/muz/rel/check_relation.cpp
src/muz/rel/udoc_relation.cpp
src/muz/rel/dl_table.cpp
src/muz/rel/dl_lazy_table.cpp
src/muz/rel/dl_mk_simple_joins.cpp
src/muz/rel/dl_mk_partial_equiv.cpp
src/muz/rel/dl_sparse_table.cpp
src/muz/rel/dl_base.cpp
src/muz/rel/dl_sieve_relation.cpp
src/muz/rel/dl_instruction.cpp
src/muz/rel/dl_external_relation.cpp
src/muz/rel/dl_product_relation.cpp
src/muz/rel/dl_interval_relation.cpp
src/smt/theory_arith.cpp
src/shell/opt_frontend.cpp
src/api/api_datalog.cpp
src/muz/fp/dl_cmds.cpp
src/muz/rel/dl_mk_explanations.cpp
src/muz/rel/dl_check_table.cpp
src/muz/rel/aig_exporter.cpp
src/muz/rel/dl_finite_product_relation.cpp
src/muz/rel/dl_relation_manager.cpp
src/muz/rel/dl_compiler.cpp
src/muz/rel/karr_relation.cpp
src/muz/rel/rel_context.cpp
src/shell/datalog_frontend.cpp
src/muz/rel/dl_bound_relation.cpp
g++ -o z3 shell/opt_frontend.o shell/main.o shell/dimacs_frontend.o shell/z3_log_frontend.o shell/smtlib_frontend.o shell/datalog_frontend.o shell/install_tactic.o shell/mem_initializer.o shell/gparams_register_modules.o api/api.a opt/opt.a parsers/smt/smtparser.a tactic/portfolio/portfolio.a tactic/ufbv/ufbv_tactic.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a tactic/nlsat_smt/nlsat_smt_tactic.a muz/fp/fp.a muz/duality/duality_intf.a muz/ddnf/ddnf.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/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/simplex/simplex.a math/hilbert/hilbert.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a -lpthread -Wl,-z,relro -fopenmp -lrt
g++ -o libz3.so -shared -Wl,-z,relro -Wl,-soname,libz3.so.4 api/dll/dll.o api/dll/install_tactic.o api/dll/mem_initializer.o api/dll/gparams_register_modules.o api/api_rcf.o api/api_datatype.o api/api_parsers.o api/api_quant.o api/api_context.o api/api_ast_map.o api/api_fpa.o api/api_algebraic.o api/api_polynomial.o api/api_opt.o api/api_numeral.o api/api_array.o api/api_goal.o api/api_params.o api/api_pb.o api/api_datalog.o api/api_arith.o api/api_ast_vector.o api/api_solver.o api/api_tactic.o api/api_stats.o api/api_model.o api/api_log.o api/z3_replayer.o api/api_ast.o api/api_interp.o api/api_bv.o api/api_solver_old.o api/api_user_theory.o api/api_config_params.o api/api_log_macros.o api/api_commands.o opt/opt.a parsers/smt/smtparser.a tactic/portfolio/portfolio.a tactic/ufbv/ufbv_tactic.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a tactic/nlsat_smt/nlsat_smt_tactic.a muz/fp/fp.a muz/duality/duality_intf.a muz/ddnf/ddnf.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/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/simplex/simplex.a math/hilbert/hilbert.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a -fopenmp -lrt
Z3 was successfully built.
Z3Py scripts can already be executed in the 'build' directory.
Z3Py scripts stored in arbitrary directories can be also executed if 'build' directory is added to the PYTHONPATH environment variable.
Use the following command to install Z3 at prefix /«PKGBUILDDIR»/debian/tmp/usr.
sudo make install
make[2]: Leaving directory '/«PKGBUILDDIR»/build'
make[1]: Leaving directory '/«PKGBUILDDIR»'
debian/rules override_dh_auto_test
make[1]: Entering directory '/«PKGBUILDDIR»'
/usr/bin/make test-z3
make[2]: Entering directory '/«PKGBUILDDIR»'
/usr/bin/make -C build test-z3
make[3]: Entering directory '/«PKGBUILDDIR»/build'
src/test/list.cpp
src/test/parray.cpp
src/test/old_interval.cpp
src/test/horn_subsume_model_converter.cpp
src/test/model2expr.cpp
src/test/qe_arith.cpp
src/test/get_implied_equalities.cpp
src/test/nlarith_util.cpp
src/test/datalog_parser.cpp
src/test/polynomial.cpp
src/test/quant_solve.cpp
src/test/random.cpp
src/test/upolynomial.cpp
src/test/string_buffer.cpp
src/test/quant_elim.cpp
src/test/expr_rand.cpp
src/test/simplex.cpp
src/test/main.cpp
src/test/prime_generator.cpp
src/test/ext_numeral.cpp
src/test/interval.cpp
src/test/timeout.cpp
src/test/sat_user_scope.cpp
src/test/doc.cpp
src/test/smt2print_parse.cpp
src/test/arith_rewriter.cpp
src/test/bit_blaster.cpp
src/test/f2n.cpp
src/test/mpq.cpp
src/test/model_retrieval.cpp
src/test/symbol.cpp
src/test/hwf.cpp
src/test/for_each_file.cpp
src/test/ex.cpp
src/test/inf_rational.cpp
src/test/heap_trie.cpp
src/test/trigo.cpp
src/test/small_object_allocator.cpp
src/test/bv_simplifier_plugin.cpp
src/test/api.cpp
src/test/nlsat.cpp
src/test/udoc_relation.cpp
src/test/uint_set.cpp
src/test/mpbq.cpp
src/test/dl_table.cpp
src/test/arith_simplifier_plugin.cpp
src/test/escaped.cpp
src/test/dl_util.cpp
src/test/mpff.cpp
src/test/substitution.cpp
src/test/chashtable.cpp
src/test/tbv.cpp
src/test/ddnf.cpp
src/test/mpfx.cpp
src/test/hilbert_basis.cpp
src/test/factor_rewriter.cpp
src/test/theory_pb.cpp
src/test/vector.cpp
src/test/algebraic.cpp
src/test/check_assumptions.cpp
src/test/buffer.cpp
src/test/polynorm.cpp
src/test/hashtable.cpp
src/test/rational.cpp
src/test/theory_dl.cpp
src/test/memory.cpp
src/test/proof_checker.cpp
src/test/expr_substitution.cpp
src/test/symbol_table.cpp
src/test/simplifier.cpp
src/test/optional.cpp
src/test/map.cpp
src/test/region.cpp
src/test/var_subst.cpp
src/test/mpf.cpp
src/test/diff_logic.cpp
src/test/no_overflow.cpp
src/test/object_allocator.cpp
src/test/rcf.cpp
src/test/stack.cpp
src/test/bits.cpp
src/test/dl_relation.cpp
src/test/fixed_bit_vector.cpp
src/test/permutation.cpp
src/test/sorting_network.cpp
src/test/simple_parser.cpp
src/test/mpz.cpp
src/test/matcher.cpp
src/test/total_order.cpp
src/test/api_bug.cpp
src/test/karr.cpp
src/test/smt_context.cpp
src/test/ast.cpp
src/test/heap.cpp
src/test/polynomial_factorization.cpp
src/test/dl_product_relation.cpp
src/test/bit_vector.cpp
src/test/pdr.cpp
src/test/dl_context.cpp
src/test/dl_query.cpp
src/test/install_tactic.cpp
src/test/mem_initializer.cpp
src/test/gparams_register_modules.cpp
src/api/api_solver.cpp
src/api/api_interp.cpp
src/test/fuzzing/expr_delta.cpp
src/test/fuzzing/expr_rand.cpp
src/smt/smt_implied_equalities.cpp
g++ -o test-z3 test/list.o test/parray.o test/old_interval.o test/horn_subsume_model_converter.o test/model2expr.o test/qe_arith.o test/get_implied_equalities.o test/nlarith_util.o test/datalog_parser.o test/polynomial.o test/quant_solve.o test/random.o test/upolynomial.o test/string_buffer.o test/quant_elim.o test/expr_rand.o test/simplex.o test/main.o test/prime_generator.o test/ext_numeral.o test/interval.o test/timeout.o test/sat_user_scope.o test/doc.o test/smt2print_parse.o test/arith_rewriter.o test/bit_blaster.o test/f2n.o test/mpq.o test/model_retrieval.o test/symbol.o test/hwf.o test/for_each_file.o test/ex.o test/inf_rational.o test/heap_trie.o test/trigo.o test/small_object_allocator.o test/bv_simplifier_plugin.o test/api.o test/nlsat.o test/udoc_relation.o test/uint_set.o test/mpbq.o test/dl_table.o test/arith_simplifier_plugin.o test/escaped.o test/dl_util.o test/mpff.o test/substitution.o test/chashtable.o test/tbv.o test/ddnf.o test/mpfx.o test/hilbert_basis.o test/factor_rewriter.o test/theory_pb.o test/vector.o test/algebraic.o test/check_assumptions.o test/buffer.o test/polynorm.o test/hashtable.o test/rational.o test/theory_dl.o test/memory.o test/proof_checker.o test/expr_substitution.o test/symbol_table.o test/simplifier.o test/optional.o test/map.o test/region.o test/var_subst.o test/mpf.o test/diff_logic.o test/no_overflow.o test/object_allocator.o test/rcf.o test/stack.o test/bits.o test/dl_relation.o test/fixed_bit_vector.o test/permutation.o test/sorting_network.o test/simple_parser.o test/mpz.o test/matcher.o test/total_order.o test/api_bug.o test/karr.o test/smt_context.o test/ast.o test/heap.o test/polynomial_factorization.o test/dl_product_relation.o test/bit_vector.o test/pdr.o test/dl_context.o test/dl_query.o test/install_tactic.o test/mem_initializer.o test/gparams_register_modules.o api/api.a opt/opt.a parsers/smt/smtparser.a tactic/portfolio/portfolio.a tactic/ufbv/ufbv_tactic.a tactic/fpa/fpa_tactics.a tactic/smtlogics/smtlogic_tactics.a tactic/nlsat_smt/nlsat_smt_tactic.a muz/fp/fp.a muz/duality/duality_intf.a muz/ddnf/ddnf.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 test/fuzzing/fuzzing.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/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/simplex/simplex.a math/hilbert/hilbert.a nlsat/nlsat.a sat/sat.a math/polynomial/polynomial.a util/util.a -lpthread -Wl,-z,relro -fopenmp -lrt
make[3]: Leaving directory '/«PKGBUILDDIR»/build'
make[2]: Leaving directory '/«PKGBUILDDIR»'
build/test-z3 -a
PASS
(test random :time 0.00 :before-memory 0.02 :after-memory 0.02)
PASS
(test random :time 0.00 :before-memory 0.02 :after-memory 0.02)
resize 1000000000
out of memory
PASS
(test vector :time 0.04 :before-memory 0.02 :after-memory 876.88)
resize 1000000000
out of memory
PASS
(test vector :time 0.02 :before-memory 876.88 :after-memory 1461.46)
PASS
(test symbol_table :time 0.00 :before-memory 1461.46 :after-memory 1461.46)
PASS
(test symbol_table :time 0.00 :before-memory 1461.46 :after-memory 1461.46)
PASS
(test region :time 0.00 :before-memory 1461.46 :after-memory 1461.46)
PASS
(test region :time 0.00 :before-memory 1461.46 :after-memory 1461.46)
foo boo foo
PASS
(test symbol :time 0.00 :before-memory 1461.46 :after-memory 1461.46)
foo boo foo
PASS
(test symbol :time 0.00 :before-memory 1461.46 :after-memory 1461.46)
i: 0
i: 1000
i: 2000
i: 3000
i: 4000
i: 5000
i: 6000
i: 7000
i: 8000
i: 9000
i: 10000
i: 11000
i: 12000
i: 13000
i: 14000
i: 15000
i: 16000
i: 17000
i: 18000
i: 19000
i: 20000
i: 21000
i: 22000
i: 23000
i: 24000
i: 25000
i: 26000
i: 27000
i: 28000
i: 29000
i: 30000
i: 31000
i: 32000
i: 33000
i: 34000
i: 35000
i: 36000
i: 37000
i: 38000
i: 39000
i: 40000
i: 41000
i: 42000
i: 43000
i: 44000
i: 45000
i: 46000
i: 47000
i: 48000
i: 49000
i: 50000
i: 51000
i: 52000
i: 53000
i: 54000
i: 55000
i: 56000
i: 57000
i: 58000
i: 59000
i: 60000
i: 61000
i: 62000
i: 63000
i: 64000
i: 65000
i: 66000
i: 67000
i: 68000
i: 69000
i: 70000
i: 71000
i: 72000
i: 73000
i: 74000
i: 75000
i: 76000
i: 77000
i: 78000
i: 79000
i: 80000
i: 81000
i: 82000
i: 83000
i: 84000
i: 85000
i: 86000
i: 87000
i: 88000
i: 89000
i: 90000
i: 91000
i: 92000
i: 93000
i: 94000
i: 95000
i: 96000
i: 97000
i: 98000
i: 99000
PASS
(test heap :time 0.06 :before-memory 1461.46 :after-memory 1461.46)
i: 0
i: 1000
i: 2000
i: 3000
i: 4000
i: 5000
i: 6000
i: 7000
i: 8000
i: 9000
i: 10000
i: 11000
i: 12000
i: 13000
i: 14000
i: 15000
i: 16000
i: 17000
i: 18000
i: 19000
i: 20000
i: 21000
i: 22000
i: 23000
i: 24000
i: 25000
i: 26000
i: 27000
i: 28000
i: 29000
i: 30000
i: 31000
i: 32000
i: 33000
i: 34000
i: 35000
i: 36000
i: 37000
i: 38000
i: 39000
i: 40000
i: 41000
i: 42000
i: 43000
i: 44000
i: 45000
i: 46000
i: 47000
i: 48000
i: 49000
i: 50000
i: 51000
i: 52000
i: 53000
i: 54000
i: 55000
i: 56000
i: 57000
i: 58000
i: 59000
i: 60000
i: 61000
i: 62000
i: 63000
i: 64000
i: 65000
i: 66000
i: 67000
i: 68000
i: 69000
i: 70000
i: 71000
i: 72000
i: 73000
i: 74000
i: 75000
i: 76000
i: 77000
i: 78000
i: 79000
i: 80000
i: 81000
i: 82000
i: 83000
i: 84000
i: 85000
i: 86000
i: 87000
i: 88000
i: 89000
i: 90000
i: 91000
i: 92000
i: 93000
i: 94000
i: 95000
i: 96000
i: 97000
i: 98000
i: 99000
PASS
(test heap :time 0.06 :before-memory 1461.46 :after-memory 1461.46)
PASS
(test hashtable :time 0.00 :before-memory 1461.46 :after-memory 1461.46)
PASS
(test hashtable :time 0.00 :before-memory 1461.46 :after-memory 1461.46)
sizeof(rational): 16
int64_max: 9223372036854775807, INT64_MAX: 9223372036854775807, int64_max.get_int64(): 9223372036854775807, int64_max.get_uint64(): 9223372036854775807
running tst6
running tst7
running tst8
running tst9
41000000000000 -7000000000000 -5 6000000000000
41000000000000 == 41000000000000
-41000000000000 -7000000000000 6 1000000000000
-41000000000000 == -41000000000000
-41000000000000 7000000000000 -6 1000000000000
-41000000000000 == -41000000000000
41000000000000 7000000000000 5 6000000000000
41000000000000 == 41000000000000
41 -7 -5 6
41 == 41
-41 -7 6 1
-41 == -41
-41 7 -6 1
-41 == -41
41 7 5 6
41 == 41
running rational_tester::tst1
(multiplication with big rationals :time 26.83 :before-memory 1461.69 :after-memory 1511.13)
(multiplication with floats: :time 0.00 :before-memory 1511.13 :after-memory 1511.13)
Testing multiplication performace using small ints
(multiplication with rationals :time 0.08 :before-memory 1500.81 :after-memory 1500.81)
(multiplication with floats: :time 0.02 :before-memory 1500.81 :after-memory 1500.81)
Testing multiplication performace using small rationals
(multiplication with rationals :time 1.19 :before-memory 1500.81 :after-memory 1500.81)
(multiplication with floats: :time 0.02 :before-memory 1500.81 :after-memory 1500.81)
PASS
(test rational :time 31.95 :before-memory 1461.46 :after-memory 1464.77)
sizeof(rational): 16
int64_max: 9223372036854775807, INT64_MAX: 9223372036854775807, int64_max.get_int64(): 9223372036854775807, int64_max.get_uint64(): 9223372036854775807
running tst6
running tst7
running tst8
running tst9
41000000000000 -7000000000000 -5 6000000000000
41000000000000 == 41000000000000
-41000000000000 -7000000000000 6 1000000000000
-41000000000000 == -41000000000000
-41000000000000 7000000000000 -6 1000000000000
-41000000000000 == -41000000000000
41000000000000 7000000000000 5 6000000000000
41000000000000 == 41000000000000
41 -7 -5 6
41 == 41
-41 -7 6 1
-41 == -41
-41 7 -6 1
-41 == -41
41 7 5 6
41 == 41
running rational_tester::tst1
(multiplication with big rationals :time 25.20 :before-memory 1465.00 :after-memory 1511.21)
(multiplication with floats: :time 0.00 :before-memory 1511.21 :after-memory 1511.21)
Testing multiplication performace using small ints
(multiplication with rationals :time 0.08 :before-memory 1500.85 :after-memory 1500.85)
(multiplication with floats: :time 0.02 :before-memory 1500.85 :after-memory 1500.85)
Testing multiplication performace using small rationals
(multiplication with rationals :time 1.19 :before-memory 1500.85 :after-memory 1500.85)
(multiplication with floats: :time 0.02 :before-memory 1500.85 :after-memory 1500.85)
PASS
(test rational :time 30.32 :before-memory 1464.77 :after-memory 1464.80)
PASS
(test inf_rational :time 0.00 :before-memory 1464.80 :after-memory 1464.80)
PASS
(test inf_rational :time 0.00 :before-memory 1464.80 :after-memory 1464.80)
PASS
(test ast :time 0.00 :before-memory 1464.80 :after-memory 1464.80)
PASS
(test ast :time 0.00 :before-memory 1464.80 :after-memory 1464.80)
PASS
(test optional :time 0.00 :before-memory 1464.80 :after-memory 1464.80)
PASS
(test optional :time 0.00 :before-memory 1464.80 :after-memory 1464.80)
b: 000001000001100000001000000000100001000000000000000000000000000000000000000001111000000000000000000010000000000
b: 0000010000011000000010000000001000010000000000000000000000000000000000000000011110000000000000000000100000000000000000000000000
b: 00000100000110000000100000000010000100000000000000000000000000000000000000000111100000000000000000001000000000000000000000000000
b: 0000010000011000000010000000001000010000000000000000000000000000000000000000011110000000000000000000100000000000000000000000000000000000000000000000000000000000
b: 0000010000011000000010000000001000010000000000000000000000000000000000000000011110000000000000000000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
b: 00000100000110000000100000000010000100000000000000000000000000000000000000000111100000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
b: 00000100000110000000100000000010000100000000000000000000000000000000000000000111100000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
10000
0100001110
0100011110
-----
10001
b1(size32): 00000000000000000000000100100011
------
b1: 10100
------
b1: 00100
PASS
(test bit_vector :time 0.00 :before-memory 1464.80 :after-memory 1464.80)
b: 000001000001100000001000000000100001000000000000000000000000000000000000000001111000000000000000000010000000000
b: 0000010000011000000010000000001000010000000000000000000000000000000000000000011110000000000000000000100000000000000000000000000
b: 00000100000110000000100000000010000100000000000000000000000000000000000000000111100000000000000000001000000000000000000000000000
b: 0000010000011000000010000000001000010000000000000000000000000000000000000000011110000000000000000000100000000000000000000000000000000000000000000000000000000000
b: 0000010000011000000010000000001000010000000000000000000000000000000000000000011110000000000000000000100000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
b: 00000100000110000000100000000010000100000000000000000000000000000000000000000111100000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
b: 00000100000110000000100000000010000100000000000000000000000000000000000000000111100000000000000000001000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000000
10000
0100001110
0100011110
-----
10001
b1(size32): 00000000000000000000000100100011
------
b1: 10100
------
b1: 00100
PASS
(test bit_vector :time 0.00 :before-memory 1464.80 :after-memory 1464.80)
0000010000
0100001110
0100011110
PASS
(test fixed_bit_vector :time 0.00 :before-memory 1464.80 :after-memory 1464.80)
0000010000
0100001110
0100011110
PASS
(test fixed_bit_vector :time 0.00 :before-memory 1464.80 :after-memory 1464.80)
[]
[]
[]
0000000000000000000000000000000
1111111111111111111111111111111
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
0000000000000000000000000011111
11111111111111111111111111x1011 -> 11111111111111111111111111x01
00000000000
11111111111
xxxxxxxxxxx
00000011111
111111x1011 -> 111111x01
000000000000000
111111111111111
xxxxxxxxxxxxxxx
000000000011111
1111111111x1011 -> 1111111111x01
0000000000000000
1111111111111111
xxxxxxxxxxxxxxxx
0000000000011111
11111111111x1011 -> 11111111111x01
00000000000000000
11111111111111111
xxxxxxxxxxxxxxxxx
00000000000011111
111111111111x1011 -> 111111111111x01
PASS
(test tbv :time 0.00 :before-memory 1464.80 :after-memory 1464.80)
[]
[]
[]
0000000000000000000000000000000
1111111111111111111111111111111
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
0000000000000000000000000011111
11111111111111111111111111x1011 -> 11111111111111111111111111x01
00000000000
11111111111
xxxxxxxxxxx
00000011111
111111x1011 -> 111111x01
000000000000000
111111111111111
xxxxxxxxxxxxxxx
000000000011111
1111111111x1011 -> 1111111111x01
0000000000000000
1111111111111111
xxxxxxxxxxxxxxxx
0000000000011111
11111111111x1011 -> 11111111111x01
00000000000000000
11111111111111111
xxxxxxxxxxxxxxxxx
00000000000011111
111111111111x1011 -> 111111111111x01
PASS
(test tbv :time 0.00 :before-memory 1464.80 :after-memory 1464.80)
xxxx \ {xxx0}
xxx
(or (and true (not (not true))) (and true (not (not false)))) true
{xx10}
{xxxx \ {x0x1, x1x0}}
{x110}
11111
00000
xxxxx
01010
10100
00000
xxxxx
11111 \ {00000} -> 11111
11111 -> 111
x1x11 -> xx1
x1x11 \ {11111} -> xx1 \ {111}
1111111111
0000000000
xxxxxxxxxx
0000001010
0000010100
0000000000
xxxxxxxxxx
1111111111 \ {
0000000000} -> 1111111111
1111111111 -> 11111111
11111x1x11 -> 11111xx1
11111x1x11 \ {
1111111111} -> 11111xx1 \ {11111111}
1111111111111111111111111111111111111111111111111111111111111111111111
0000000000000000000000000000000000000000000000000000000000000000000000
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
0000000000000000000000000000000000000000000000000000000000000000001010
0000000000000000000000000000000000000000000000000000000000000000010100
0000000000000000000000000000000000000000000000000000000000000000000000
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
1111111111111111111111111111111111111111111111111111111111111111111111 \ {
0000000000000000000000000000000000000000000000000000000000000000000000} -> 1111111111111111111111111111111111111111111111111111111111111111111111
1111111111111111111111111111111111111111111111111111111111111111111111 -> 11111111111111111111111111111111111111111111111111111111111111111111
11111111111111111111111111111111111111111111111111111111111111111x1x11 -> 11111111111111111111111111111111111111111111111111111111111111111xx1
11111111111111111111111111111111111111111111111111111111111111111x1x11 \ {
1111111111111111111111111111111111111111111111111111111111111111111111} -> 11111111111111111111111111111111111111111111111111111111111111111xx1 \ {
11111111111111111111111111111111111111111111111111111111111111111111}
PASS
(test doc :time 212.09 :before-memory 1464.80 :after-memory 1559.72)
xxxx \ {xxx0}
xxx
(or (and true (not (not true))) (and true (not (not false)))) true
{xx10}
{xxxx \ {x0x1, x1x0}}
{x110}
11111
00000
xxxxx
01010
10100
00000
xxxxx
11111 \ {00000} -> 11111
11111 -> 111
x1x11 -> xx1
x1x11 \ {11111} -> xx1 \ {111}
1111111111
0000000000
xxxxxxxxxx
0000001010
0000010100
0000000000
xxxxxxxxxx
1111111111 \ {
0000000000} -> 1111111111
1111111111 -> 11111111
11111x1x11 -> 11111xx1
11111x1x11 \ {
1111111111} -> 11111xx1 \ {11111111}
1111111111111111111111111111111111111111111111111111111111111111111111
0000000000000000000000000000000000000000000000000000000000000000000000
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
0000000000000000000000000000000000000000000000000000000000000000001010
0000000000000000000000000000000000000000000000000000000000000000010100
0000000000000000000000000000000000000000000000000000000000000000000000
xxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxxx
1111111111111111111111111111111111111111111111111111111111111111111111 \ {
0000000000000000000000000000000000000000000000000000000000000000000000} -> 1111111111111111111111111111111111111111111111111111111111111111111111
1111111111111111111111111111111111111111111111111111111111111111111111 -> 11111111111111111111111111111111111111111111111111111111111111111111
11111111111111111111111111111111111111111111111111111111111111111x1x11 -> 11111111111111111111111111111111111111111111111111111111111111111xx1
11111111111111111111111111111111111111111111111111111111111111111x1x11 \ {
1111111111111111111111111111111111111111111111111111111111111111111111} -> 11111111111111111111111111111111111111111111111111111111111111111xx1 \ {
11111111111111111111111111111111111111111111111111111111111111111111}
PASS
(test doc :time 209.99 :before-memory 1559.72 :after-memory 1654.59)
terminate called after throwing an instance of 'int'
true
(and true (not (and (= (:var 0) #b1) (= (:var 2) #b0))))
(and (= (:var 0) #b1) (= (:var 2) #b0))
(let ((a!1 (not (exists ((x!1 (_ BitVec 1))
(x!2 (_ BitVec 1))
(x!3 (_ BitVec 1)))
(and (= x!3 #b1)
(= x!1 #b0)
(= k!0 x!3)
(= k!1 x!2)
(= k!2 x!1))))))
(and true a!1))
(and true (not (and (= k!0 #b1) (= k!2 #b0))))
make[1]: *** [override_dh_auto_test] Aborted
debian/rules:79: recipe for target 'override_dh_auto_test' failed
make[1]: Leaving directory '/«PKGBUILDDIR»'
make: *** [build-arch] Error 2
debian/rules:13: recipe for target 'build-arch' failed
dpkg-buildpackage: error: debian/rules build-arch gave error exit status 2
────────────────────────────────────────────────────────────────────────────────
Build finished at 20150725-0829
Finished
────────
E: Build failure (dpkg-buildpackage died)
┌──────────────────────────────────────────────────────────────────────────────┐
│ Cleanup │
└──────────────────────────────────────────────────────────────────────────────┘
Purging /«BUILDDIR»
Not cleaning session: cloned chroot in use
┌──────────────────────────────────────────────────────────────────────────────┐
│ Summary │
└──────────────────────────────────────────────────────────────────────────────┘
Build Architecture: armhf
Build-Space: 1592956
Build-Time: 5937
Distribution: stretch-staging
Fail-Stage: build
Host Architecture: armhf
Install-Time: 206
Job: z3_4.4.0-2
Machine Architecture: armhf
Package: z3
Package-Time: 6209
Source-Version: 4.4.0-2
Space: 1592956
Status: attempted
Version: 4.4.0-2
────────────────────────────────────────────────────────────────────────────────
Finished at 20150725-0829
Build needed 01:43:29, 1592956k disc space