z3 →
4.4.0-2 →
armhf → 2015-11-19 10:26:50
sbuild (Debian sbuild) 0.65.2 (24 Mar 2015) on bm-wb-01
╔══════════════════════════════════════════════════════════════════════════════╗
║ z3 4.4.0-2 (armhf) 19 Nov 2015 08: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-7psYSq/z3-4.4.0' with '«PKGBUILDDIR»'
I: NOTICE: Log filtering will replace 'build/z3-7psYSq' with '«BUILDDIR»'
I: NOTICE: Log filtering will replace 'var/lib/schroot/mount/stretch-staging-armhf-sbuild-2309c0f2-9918-4056-a27e-71654d9c4441' 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 [8471 kB]
Get:3 http://172.17.0.1 stretch-staging/main armhf Packages [10.4 MB]
Ign http://172.17.0.1 stretch-staging/main Translation-en
Fetched 18.9 MB in 35s (526 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...
Reading state information...
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 (4089 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-SPUzAc/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...
Reading state information...
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 2 not upgraded.
Need to get 0 B/768 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 ... 12031 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-4MUNuP/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 dh-strip-nondeterminism file gettext gettext-base
groff-base intltool-debian libarchive-zip-perl libcroco3 libexpat1 libffi6
libfile-stripnondeterminism-perl libglib2.0-0 libicu55 libmagic1
libpipeline1 libpython-stdlib libpython2.7-minimal libpython2.7-stdlib
libsqlite3-0 libssl1.0.2 libtimedate-perl 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 autopoint
libasprintf-dev libgettextpo-dev groff less www-browser libmail-box-perl
python-doc python-tk python2.7-doc binfmt-support
Recommended packages:
curl wget lynx-cur libglib2.0-data shared-mime-info xdg-user-dirs xml-core
libmail-sendmail-perl
The following NEW packages will be installed:
bsdmainutils debhelper dh-strip-nondeterminism file gettext gettext-base
groff-base intltool-debian libarchive-zip-perl libcroco3 libexpat1 libffi6
libfile-stripnondeterminism-perl libglib2.0-0 libicu55 libmagic1
libpipeline1 libpython-stdlib libpython2.7-minimal libpython2.7-stdlib
libsqlite3-0 libssl1.0.2 libtimedate-perl libunistring0 libxml2 man-db
mime-support po-debconf python python-minimal python2.7 python2.7-minimal
sbuild-build-depends-z3-dummy
0 upgraded, 33 newly installed, 0 to remove and 2 not upgraded.
Need to get 21.5 MB/21.5 MB of archives.
After this operation, 76.6 MB of additional disk space will be used.
Get:1 http://172.17.0.1/private/ stretch-staging/main groff-base armhf 1.22.3-3 [1084 kB]
Get:2 http://172.17.0.1/private/ stretch-staging/main bsdmainutils armhf 9.0.6 [177 kB]
Get:3 http://172.17.0.1/private/ stretch-staging/main libpipeline1 armhf 1.4.1-1 [23.9 kB]
Get:4 http://172.17.0.1/private/ stretch-staging/main man-db armhf 2.7.5-1 [975 kB]
Get:5 http://172.17.0.1/private/ stretch-staging/main libpython2.7-minimal armhf 2.7.10-5+b1 [380 kB]
Get:6 http://172.17.0.1/private/ stretch-staging/main python2.7-minimal armhf 2.7.10-5+b1 [1092 kB]
Get:7 http://172.17.0.1/private/ stretch-staging/main python-minimal armhf 2.7.9-1 [40.1 kB]
Get:8 http://172.17.0.1/private/ stretch-staging/main mime-support all 3.59 [36.4 kB]
Get:9 http://172.17.0.1/private/ stretch-staging/main libexpat1 armhf 2.1.0-7 [59.8 kB]
Get:10 http://172.17.0.1/private/ stretch-staging/main libffi6 armhf 3.2.1-3 [18.5 kB]
Get:11 http://172.17.0.1/private/ stretch-staging/main libsqlite3-0 armhf 3.9.2-1 [404 kB]
Get:12 http://172.17.0.1/private/ stretch-staging/main libssl1.0.2 armhf 1.0.2d-3 [881 kB]
Get:13 http://172.17.0.1/private/ stretch-staging/main libpython2.7-stdlib armhf 2.7.10-5+b1 [1811 kB]
Get:14 http://172.17.0.1/private/ stretch-staging/main python2.7 armhf 2.7.10-5+b1 [265 kB]
Get:15 http://172.17.0.1/private/ stretch-staging/main libpython-stdlib armhf 2.7.9-1 [19.6 kB]
Get:16 http://172.17.0.1/private/ stretch-staging/main python armhf 2.7.9-1 [151 kB]
Get:17 http://172.17.0.1/private/ stretch-staging/main libunistring0 armhf 0.9.3-5.2 [253 kB]
Get:18 http://172.17.0.1/private/ stretch-staging/main libmagic1 armhf 1:5.25-2 [250 kB]
Get:19 http://172.17.0.1/private/ stretch-staging/main file armhf 1:5.25-2 [61.2 kB]
Get:20 http://172.17.0.1/private/ stretch-staging/main gettext-base armhf 0.19.6-1 [119 kB]
Get:21 http://172.17.0.1/private/ stretch-staging/main libicu55 armhf 55.1-6 [7379 kB]
Get:22 http://172.17.0.1/private/ stretch-staging/main libxml2 armhf 2.9.2+zdfsg1-4 [797 kB]
Get:23 http://172.17.0.1/private/ stretch-staging/main libglib2.0-0 armhf 2.46.2-1 [2482 kB]
Get:24 http://172.17.0.1/private/ stretch-staging/main libcroco3 armhf 0.6.9-1 [129 kB]
Get:25 http://172.17.0.1/private/ stretch-staging/main gettext armhf 0.19.6-1 [1393 kB]
Get:26 http://172.17.0.1/private/ stretch-staging/main intltool-debian all 0.35.0+20060710.4 [26.3 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 libarchive-zip-perl all 1.53-1 [97.3 kB]
Get:29 http://172.17.0.1/private/ stretch-staging/main libfile-stripnondeterminism-perl all 0.014-1 [10.6 kB]
Get:30 http://172.17.0.1/private/ stretch-staging/main libtimedate-perl all 2.3000-2 [42.2 kB]
Get:31 http://172.17.0.1/private/ stretch-staging/main dh-strip-nondeterminism all 0.014-1 [7472 B]
Get:32 http://172.17.0.1/private/ stretch-staging/main debhelper all 9.20151005 [817 kB]
debconf: delaying package configuration, since apt-utils is not installed
Fetched 21.5 MB in 5s (3991 kB/s)
Selecting previously unselected package groff-base.
(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 ... 12031 files and directories currently installed.)
Preparing to unpack .../groff-base_1.22.3-3_armhf.deb ...
Unpacking groff-base (1.22.3-3) ...
Selecting previously unselected package bsdmainutils.
Preparing to unpack .../bsdmainutils_9.0.6_armhf.deb ...
Unpacking bsdmainutils (9.0.6) ...
Selecting previously unselected package libpipeline1:armhf.
Preparing to unpack .../libpipeline1_1.4.1-1_armhf.deb ...
Unpacking libpipeline1:armhf (1.4.1-1) ...
Selecting previously unselected package man-db.
Preparing to unpack .../man-db_2.7.5-1_armhf.deb ...
Unpacking man-db (2.7.5-1) ...
Selecting previously unselected package libpython2.7-minimal:armhf.
Preparing to unpack .../libpython2.7-minimal_2.7.10-5+b1_armhf.deb ...
Unpacking libpython2.7-minimal:armhf (2.7.10-5+b1) ...
Selecting previously unselected package python2.7-minimal.
Preparing to unpack .../python2.7-minimal_2.7.10-5+b1_armhf.deb ...
Unpacking python2.7-minimal (2.7.10-5+b1) ...
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.59_all.deb ...
Unpacking mime-support (3.59) ...
Selecting previously unselected package libexpat1:armhf.
Preparing to unpack .../libexpat1_2.1.0-7_armhf.deb ...
Unpacking libexpat1:armhf (2.1.0-7) ...
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.9.2-1_armhf.deb ...
Unpacking libsqlite3-0:armhf (3.9.2-1) ...
Selecting previously unselected package libssl1.0.2:armhf.
Preparing to unpack .../libssl1.0.2_1.0.2d-3_armhf.deb ...
Unpacking libssl1.0.2:armhf (1.0.2d-3) ...
Selecting previously unselected package libpython2.7-stdlib:armhf.
Preparing to unpack .../libpython2.7-stdlib_2.7.10-5+b1_armhf.deb ...
Unpacking libpython2.7-stdlib:armhf (2.7.10-5+b1) ...
Selecting previously unselected package python2.7.
Preparing to unpack .../python2.7_2.7.10-5+b1_armhf.deb ...
Unpacking python2.7 (2.7.10-5+b1) ...
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) ...
Processing triggers for libc-bin (2.19-22) ...
Setting up libpython2.7-minimal:armhf (2.7.10-5+b1) ...
Setting up python2.7-minimal (2.7.10-5+b1) ...
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 ... 13399 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 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 libmagic1:armhf.
Preparing to unpack .../libmagic1_1%3a5.25-2_armhf.deb ...
Unpacking libmagic1:armhf (1:5.25-2) ...
Selecting previously unselected package file.
Preparing to unpack .../file_1%3a5.25-2_armhf.deb ...
Unpacking file (1:5.25-2) ...
Selecting previously unselected package gettext-base.
Preparing to unpack .../gettext-base_0.19.6-1_armhf.deb ...
Unpacking gettext-base (0.19.6-1) ...
Selecting previously unselected package libicu55:armhf.
Preparing to unpack .../libicu55_55.1-6_armhf.deb ...
Unpacking libicu55:armhf (55.1-6) ...
Selecting previously unselected package libxml2:armhf.
Preparing to unpack .../libxml2_2.9.2+zdfsg1-4_armhf.deb ...
Unpacking libxml2:armhf (2.9.2+zdfsg1-4) ...
Selecting previously unselected package libglib2.0-0:armhf.
Preparing to unpack .../libglib2.0-0_2.46.2-1_armhf.deb ...
Unpacking libglib2.0-0:armhf (2.46.2-1) ...
Selecting previously unselected package libcroco3:armhf.
Preparing to unpack .../libcroco3_0.6.9-1_armhf.deb ...
Unpacking libcroco3:armhf (0.6.9-1) ...
Selecting previously unselected package gettext.
Preparing to unpack .../gettext_0.19.6-1_armhf.deb ...
Unpacking gettext (0.19.6-1) ...
Selecting previously unselected package intltool-debian.
Preparing to unpack .../intltool-debian_0.35.0+20060710.4_all.deb ...
Unpacking intltool-debian (0.35.0+20060710.4) ...
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 libarchive-zip-perl.
Preparing to unpack .../libarchive-zip-perl_1.53-1_all.deb ...
Unpacking libarchive-zip-perl (1.53-1) ...
Selecting previously unselected package libfile-stripnondeterminism-perl.
Preparing to unpack .../libfile-stripnondeterminism-perl_0.014-1_all.deb ...
Unpacking libfile-stripnondeterminism-perl (0.014-1) ...
Selecting previously unselected package libtimedate-perl.
Preparing to unpack .../libtimedate-perl_2.3000-2_all.deb ...
Unpacking libtimedate-perl (2.3000-2) ...
Selecting previously unselected package dh-strip-nondeterminism.
Preparing to unpack .../dh-strip-nondeterminism_0.014-1_all.deb ...
Unpacking dh-strip-nondeterminism (0.014-1) ...
Selecting previously unselected package debhelper.
Preparing to unpack .../debhelper_9.20151005_all.deb ...
Unpacking debhelper (9.20151005) ...
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) ...
Processing triggers for libc-bin (2.19-22) ...
Setting up groff-base (1.22.3-3) ...
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 libpipeline1:armhf (1.4.1-1) ...
Setting up man-db (2.7.5-1) ...
Not building database; man-db/auto-update is not 'true'.
Setting up mime-support (3.59) ...
Setting up libexpat1:armhf (2.1.0-7) ...
Setting up libffi6:armhf (3.2.1-3) ...
Setting up libsqlite3-0:armhf (3.9.2-1) ...
Setting up libssl1.0.2:armhf (1.0.2d-3) ...
Setting up libpython2.7-stdlib:armhf (2.7.10-5+b1) ...
Setting up python2.7 (2.7.10-5+b1) ...
Setting up libpython-stdlib:armhf (2.7.9-1) ...
Setting up python (2.7.9-1) ...
Setting up libunistring0:armhf (0.9.3-5.2) ...
Setting up libmagic1:armhf (1:5.25-2) ...
Setting up file (1:5.25-2) ...
Setting up gettext-base (0.19.6-1) ...
Setting up libicu55:armhf (55.1-6) ...
Setting up libxml2:armhf (2.9.2+zdfsg1-4) ...
Setting up libglib2.0-0:armhf (2.46.2-1) ...
No schema files found: doing nothing.
Setting up libcroco3:armhf (0.6.9-1) ...
Setting up gettext (0.19.6-1) ...
Setting up intltool-debian (0.35.0+20060710.4) ...
Setting up po-debconf (1.0.18) ...
Setting up libarchive-zip-perl (1.53-1) ...
Setting up libfile-stripnondeterminism-perl (0.014-1) ...
Setting up libtimedate-perl (2.3000-2) ...
Setting up dh-strip-nondeterminism (0.014-1) ...
Setting up debhelper (9.20151005) ...
Setting up sbuild-build-depends-z3-dummy (0.invalid.0) ...
Processing triggers for libc-bin (2.19-22) ...
┌──────────────────────────────────────────────────────────────────────────────┐
│ Build environment │
└──────────────────────────────────────────────────────────────────────────────┘
Kernel: Linux 3.19.0-trunk-armmp armhf (armv7l)
Toolchain package versions: binutils_2.25.1-7 dpkg-dev_1.18.3 g++-5_5.2.1-23+rpi1 gcc-5_5.2.1-23+rpi1 libc6-dev_2.19-22 libstdc++-5-dev_5.2.1-23+rpi1 libstdc++6_5.2.1-23+rpi1 linux-libc-dev_3.18.5-1~exp1+rpi19+stretch
Package versions: adduser_3.113+nmu3 apt_1.0.10.2 base-files_9.4+rpi1 base-passwd_3.5.38 bash_4.3-14 binutils_2.25.1-7 bsdmainutils_9.0.6 bsdutils_1:2.27.1-1 build-essential_11.7 bzip2_1.0.6-8 coreutils_8.23-4 cpio_2.11+dfsg-4.1 cpp_4:5.2.1-4+rpi2 cpp-5_5.2.1-23+rpi1 dash_0.5.7-4 debconf_1.5.58 debconf-i18n_1.5.58 debfoster_2.7-2 debhelper_9.20151005 debianutils_4.5.1 dh-strip-nondeterminism_0.014-1 diffutils_1:3.3-2 dmsetup_2:1.02.110-1+rpi1 dpkg_1.18.3 dpkg-dev_1.18.3 e2fslibs_1.42.13-1 e2fsprogs_1.42.13-1 fakeroot_1.20.2-1 file_1:5.25-2 findutils_4.4.2-10 g++_4:5.2.1-4+rpi2 g++-5_5.2.1-23+rpi1 gcc_4:5.2.1-4+rpi2 gcc-4.6-base_4.6.4-5+rpi1 gcc-4.7-base_4.7.3-11+rpi1 gcc-4.8-base_4.8.5-1 gcc-4.9-base_4.9.3-5 gcc-5_5.2.1-23+rpi1 gcc-5-base_5.2.1-23+rpi1 gettext_0.19.6-1 gettext-base_0.19.6-1 gnupg_1.4.19-6 gpgv_1.4.19-6 grep_2.21-2 groff-base_1.22.3-3 gzip_1.6-4 hostname_3.16 init_1.24 init-system-helpers_1.24 initramfs-tools_0.120 initscripts_2.88dsf-59.2 insserv_1.14.0-5 intltool-debian_0.35.0+20060710.4 klibc-utils_2.0.4-2+rpi1 kmod_21-1 libacl1_2.2.52-2 libapparmor1_2.10-2+b2 libapt-pkg4.16_1.0.10.2 libarchive-zip-perl_1.53-1 libasan2_5.2.1-23+rpi1 libatomic1_5.2.1-23+rpi1 libattr1_1:2.4.47-2 libaudit-common_1:2.4.4-4 libaudit1_1:2.4.4-4 libblkid1_2.27.1-1 libbz2-1.0_1.0.6-8 libc-bin_2.19-22 libc-dev-bin_2.19-22 libc6_2.19-22 libc6-dev_2.19-22 libcap2_1:2.24-12 libcap2-bin_1:2.24-12 libcc1-0_5.2.1-23+rpi1 libcomerr2_1.42.13-1 libcroco3_0.6.9-1 libcryptsetup4_2:1.6.6-5 libdb5.3_5.3.28-11 libdbus-1-3_1.10.2-1 libdebconfclient0_0.195 libdevmapper1.02.1_2:1.02.110-1+rpi1 libdpkg-perl_1.18.3 libdrm2_2.4.65-3 libexpat1_2.1.0-7 libfakeroot_1.20.2-1 libfdisk1_2.27.1-1 libffi6_3.2.1-3 libfile-stripnondeterminism-perl_0.014-1 libgc1c2_1:7.4.2-7 libgcc-5-dev_5.2.1-23+rpi1 libgcc1_1:5.2.1-23+rpi1 libgcrypt20_1.6.4-3 libgdbm3_1.8.3-13.1 libglib2.0-0_2.46.2-1 libgmp10_2:6.0.0+dfsg-7+rpi1 libgomp1_5.2.1-23+rpi1 libgpg-error0_1.20-1 libicu55_55.1-6 libisl13_0.14-2 libklibc_2.0.4-2+rpi1 libkmod2_21-1 liblocale-gettext-perl_1.07-1 liblzma5_5.1.1alpha+20120614-2.1 libmagic1_1:5.25-2 libmount1_2.27.1-1 libmpc3_1.0.3-1 libmpfr4_3.1.3-1 libncurses5_6.0+20151024-2 libncursesw5_6.0+20151024-2 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-7.4 libpipeline1_1.4.1-1 libpng12-0_1.2.50-2+b2 libprocps4_2:3.3.10-2 libpython-stdlib_2.7.9-1 libpython2.7-minimal_2.7.10-5+b1 libpython2.7-stdlib_2.7.10-5+b1 libreadline6_6.3-8+b3 libseccomp2_2.2.3-2 libselinux1_2.3-2 libsemanage-common_2.3-1 libsemanage1_2.3-1 libsepol1_2.3-2 libsmartcols1_2.27.1-1 libsqlite3-0_3.9.2-1 libss2_1.42.13-1 libssl1.0.2_1.0.2d-3 libstdc++-5-dev_5.2.1-23+rpi1 libstdc++6_5.2.1-23+rpi1 libsystemd0_227-2 libtext-charwidth-perl_0.04-7+b4 libtext-iconv-perl_1.7-5+b5 libtext-wrapi18n-perl_0.06-7.1 libtimedate-perl_2.3000-2 libtinfo5_6.0+20151024-2 libubsan0_5.2.1-23+rpi1 libudev1_227-2 libunistring0_0.9.3-5.2 libusb-0.1-4_2:0.1.12-27 libustr-1.0-1_1.0.4-5 libuuid1_2.27.1-1 libxml2_2.9.2+zdfsg1-4 linux-libc-dev_3.18.5-1~exp1+rpi19+stretch login_1:4.2-3 lsb-base_4.1+Debian13+rpi1+nmu1 make_4.0-8.2 makedev_2.3.1-93 man-db_2.7.5-1 mawk_1.3.3-17 mime-support_3.59 mount_2.27.1-1 multiarch-support_2.19-22 nano_2.4.2-1 ncurses-base_6.0+20151024-2 ncurses-bin_6.0+20151024-2 passwd_1:4.2-3 patch_2.7.5-1 perl_5.20.2-6 perl-base_5.20.2-6 perl-modules_5.20.2-6 po-debconf_1.0.18 procps_2:3.3.10-2 python_2.7.9-1 python-minimal_2.7.9-1 python2.7_2.7.10-5+b1 python2.7-minimal_2.7.10-5+b1 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-6.1 sensible-utils_0.0.9 startpar_0.59-3 systemd_227-2 systemd-sysv_227-2 sysv-rc_2.88dsf-59.2 sysvinit-utils_2.88dsf-59.2 tar_1.28-2.1 tzdata_2015g-1 udev_227-2 util-linux_2.27.1-1 xz-utils_5.1.1alpha+20120614-2.1 zlib1g_1:1.2.8.dfsg-2+b1
┌──────────────────────────────────────────────────────────────────────────────┐
│ 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=root
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-2309c0f2-9918-4056-a27e-71654d9c4441
SCHROOT_UID=104
SCHROOT_USER=buildd
SHELL=/bin/sh
TERM=xterm
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/page.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/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/ast/rewriter/expr_safe_replace.cpp
../src/parsers/util/scanner.cpp: In member function 'scanner::token scanner::scan()':
../src/parsers/util/scanner.cpp:483:9: warning: case label value is less than minimum value for type
case -1:
^
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:17: 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/pb2bv_tactic.cpp
src/tactic/arith/degree_shift_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:17: warning: case label value is less than minimum value for type
case -1:
^
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:13: 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.04 :before-memory 876.88 :after-memory 1753.75)
PASS
(test symbol_table :time 0.00 :before-memory 1753.75 :after-memory 1753.75)
PASS
(test symbol_table :time 0.00 :before-memory 1753.75 :after-memory 1753.75)
PASS
(test region :time 0.00 :before-memory 1753.75 :after-memory 1753.75)
PASS
(test region :time 0.00 :before-memory 1753.75 :after-memory 1753.75)
foo boo foo
PASS
(test symbol :time 0.00 :before-memory 1753.75 :after-memory 1753.75)
foo boo foo
PASS
(test symbol :time 0.00 :before-memory 1753.75 :after-memory 1753.75)
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 1753.75 :after-memory 1753.75)
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 1753.75 :after-memory 1753.75)
PASS
(test hashtable :time 0.00 :before-memory 1753.75 :after-memory 1753.75)
PASS
(test hashtable :time 0.00 :before-memory 1753.75 :after-memory 1753.75)
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.16 :before-memory 1753.98 :after-memory 1803.41)
(multiplication with floats: :time 0.00 :before-memory 1803.41 :after-memory 1803.41)
Testing multiplication performace using small ints
(multiplication with rationals :time 0.07 :before-memory 1793.10 :after-memory 1793.10)
(multiplication with floats: :time 0.02 :before-memory 1793.10 :after-memory 1793.10)
Testing multiplication performace using small rationals
(multiplication with rationals :time 1.10 :before-memory 1793.10 :after-memory 1793.10)
(multiplication with floats: :time 0.02 :before-memory 1793.10 :after-memory 1793.10)
PASS
(test rational :time 29.89 :before-memory 1753.75 :after-memory 1757.06)
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 1757.29 :after-memory 1803.50)
(multiplication with floats: :time 0.00 :before-memory 1803.50 :after-memory 1803.50)
Testing multiplication performace using small ints
(multiplication with rationals :time 0.07 :before-memory 1793.13 :after-memory 1793.13)
(multiplication with floats: :time 0.04 :before-memory 1793.13 :after-memory 1793.13)
Testing multiplication performace using small rationals
(multiplication with rationals :time 1.20 :before-memory 1793.13 :after-memory 1793.13)
(multiplication with floats: :time 0.02 :before-memory 1793.13 :after-memory 1793.13)
PASS
(test rational :time 30.23 :before-memory 1757.06 :after-memory 1757.09)
PASS
(test inf_rational :time 0.00 :before-memory 1757.09 :after-memory 1757.09)
PASS
(test inf_rational :time 0.00 :before-memory 1757.09 :after-memory 1757.09)
PASS
(test ast :time 0.00 :before-memory 1757.09 :after-memory 1757.09)
PASS
(test ast :time 0.00 :before-memory 1757.09 :after-memory 1757.09)
PASS
(test optional :time 0.00 :before-memory 1757.09 :after-memory 1757.09)
PASS
(test optional :time 0.00 :before-memory 1757.09 :after-memory 1757.09)
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 1757.09 :after-memory 1757.09)
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 1757.09 :after-memory 1757.09)
0000010000
0100001110
0100011110
PASS
(test fixed_bit_vector :time 0.00 :before-memory 1757.09 :after-memory 1757.09)
0000010000
0100001110
0100011110
PASS
(test fixed_bit_vector :time 0.00 :before-memory 1757.09 :after-memory 1757.09)
[]
[]
[]
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 1757.09 :after-memory 1757.09)
[]
[]
[]
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 1757.09 :after-memory 1757.09)
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 215.20 :before-memory 1757.09 :after-memory 1852.01)
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 211.66 :before-memory 1852.01 :after-memory 1946.88)
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 20151119-1024
Finished
────────
E: Build failure (dpkg-buildpackage died)
┌──────────────────────────────────────────────────────────────────────────────┐
│ Cleanup │
└──────────────────────────────────────────────────────────────────────────────┘
Purging /«BUILDDIR»
Not cleaning session: cloned chroot in use
┌──────────────────────────────────────────────────────────────────────────────┐
│ Summary │
└──────────────────────────────────────────────────────────────────────────────┘
Build Architecture: armhf
Build-Space: 1559096
Build-Time: 5627
Distribution: stretch-staging
Fail-Stage: build
Host Architecture: armhf
Install-Time: 221
Job: z3_4.4.0-2
Machine Architecture: armhf
Package: z3
Package-Time: 5910
Source-Version: 4.4.0-2
Space: 1559096
Status: attempted
Version: 4.4.0-2
────────────────────────────────────────────────────────────────────────────────
Finished at 20151119-1024
Build needed 01:38:30, 1559096k disc space