z3 →
4.4.0-2 →
armhf → 2016-02-24 15:42:42
sbuild (Debian sbuild) 0.66.0 (04 Oct 2015) on testbuildd.raspbian.org
+==============================================================================+
| z3 4.4.0-2 (armhf) 24 Feb 2016 14:04 |
+==============================================================================+
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-xu19Fy/z3-4.4.0' with '<<PKGBUILDDIR>>'
I: NOTICE: Log filtering will replace 'build/z3-xu19Fy' with '<<BUILDDIR>>'
I: NOTICE: Log filtering will replace 'var/lib/schroot/mount/stretch-staging-armhf-sbuild-b5faec98-69df-4440-b368-ff2a84ec5c9b' with '<<CHROOT>>'
+------------------------------------------------------------------------------+
| Update chroot |
+------------------------------------------------------------------------------+
Get:1 http://172.17.0.1/private stretch-staging InRelease [11.3 kB]
Get:2 http://172.17.0.1/private stretch-staging/main Sources [8753 kB]
Get:3 http://172.17.0.1/private stretch-staging/main armhf Packages [10.8 MB]
Fetched 19.6 MB in 24s (815 kB/s)
Reading package lists...
W: No sandbox user '_apt' on the system, can not drop privileges
+------------------------------------------------------------------------------+
| Fetch source files |
+------------------------------------------------------------------------------+
Check APT
---------
Checking available source versions...
Download source files with APT
------------------------------
Reading package lists...
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 1s (2383 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-AZA6V9/apt_archive/sbuild-build-depends-core-dummy.deb'.
OK
Get:1 file:/<<BUILDDIR>>/resolver-AZA6V9/apt_archive ./ InRelease
Ign:1 file:/<<BUILDDIR>>/resolver-AZA6V9/apt_archive ./ InRelease
Get:2 file:/<<BUILDDIR>>/resolver-AZA6V9/apt_archive ./ Release [2119 B]
Get:2 file:/<<BUILDDIR>>/resolver-AZA6V9/apt_archive ./ Release [2119 B]
Get:3 file:/<<BUILDDIR>>/resolver-AZA6V9/apt_archive ./ Release.gpg [299 B]
Get:3 file:/<<BUILDDIR>>/resolver-AZA6V9/apt_archive ./ Release.gpg [299 B]
Get:4 file:/<<BUILDDIR>>/resolver-AZA6V9/apt_archive ./ Sources [214 B]
Get:5 file:/<<BUILDDIR>>/resolver-AZA6V9/apt_archive ./ Packages [528 B]
Reading package lists...
W: No sandbox user '_apt' on the system, can not drop privileges
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
0 upgraded, 1 newly installed, 0 to remove and 27 not upgraded.
Need to get 0 B/764 B of archives.
After this operation, 0 B of additional disk space will be used.
Get:1 file:/<<BUILDDIR>>/resolver-AZA6V9/apt_archive ./ sbuild-build-depends-core-dummy 0.invalid.0 [764 B]
debconf: delaying package configuration, since apt-utils is not installed
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 ... 12695 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) ...
W: No sandbox user '_apt' on the system, can not drop privileges
Merged Build-Depends: debhelper (>= 9), python
Filtered Build-Depends: debhelper (>= 9), python
dpkg-deb: building package 'sbuild-build-depends-z3-dummy' in '/<<BUILDDIR>>/resolver-d3Qf7D/apt_archive/sbuild-build-depends-z3-dummy.deb'.
OK
Get:1 file:/<<BUILDDIR>>/resolver-d3Qf7D/apt_archive ./ InRelease
Ign:1 file:/<<BUILDDIR>>/resolver-d3Qf7D/apt_archive ./ InRelease
Get:2 file:/<<BUILDDIR>>/resolver-d3Qf7D/apt_archive ./ Release [2119 B]
Get:2 file:/<<BUILDDIR>>/resolver-d3Qf7D/apt_archive ./ Release [2119 B]
Get:3 file:/<<BUILDDIR>>/resolver-d3Qf7D/apt_archive ./ Release.gpg [299 B]
Get:3 file:/<<BUILDDIR>>/resolver-d3Qf7D/apt_archive ./ Release.gpg [299 B]
Get:4 file:/<<BUILDDIR>>/resolver-d3Qf7D/apt_archive ./ Sources [213 B]
Get:5 file:/<<BUILDDIR>>/resolver-d3Qf7D/apt_archive ./ Packages [528 B]
Reading package lists...
W: No sandbox user '_apt' on the system, can not drop privileges
Reading package lists...
+------------------------------------------------------------------------------+
| Install z3 build dependencies (apt-based resolver) |
+------------------------------------------------------------------------------+
Installing build dependencies
Reading package lists...
Building dependency tree...
Reading state information...
The following additional packages will be installed:
autotools-dev 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:
autotools-dev 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, 34 newly installed, 0 to remove and 27 not upgraded.
Need to get 21.6 MB/21.6 MB of archives.
After this operation, 77.1 MB of additional disk space will be used.
Get:1 file:/<<BUILDDIR>>/resolver-d3Qf7D/apt_archive ./ sbuild-build-depends-z3-dummy 0.invalid.0 [768 B]
Get:2 http://172.17.0.1/private stretch-staging/main armhf groff-base armhf 1.22.3-7 [1083 kB]
Get:3 http://172.17.0.1/private stretch-staging/main armhf bsdmainutils armhf 9.0.6 [177 kB]
Get:4 http://172.17.0.1/private stretch-staging/main armhf libpipeline1 armhf 1.4.1-2 [23.7 kB]
Get:5 http://172.17.0.1/private stretch-staging/main armhf man-db armhf 2.7.5-1 [975 kB]
Get:6 http://172.17.0.1/private stretch-staging/main armhf libpython2.7-minimal armhf 2.7.11-3 [380 kB]
Get:7 http://172.17.0.1/private stretch-staging/main armhf python2.7-minimal armhf 2.7.11-3 [1093 kB]
Get:8 http://172.17.0.1/private stretch-staging/main armhf python-minimal armhf 2.7.11-1 [40.0 kB]
Get:9 http://172.17.0.1/private stretch-staging/main armhf mime-support all 3.59 [36.4 kB]
Get:10 http://172.17.0.1/private stretch-staging/main armhf libexpat1 armhf 2.1.0-7 [59.8 kB]
Get:11 http://172.17.0.1/private stretch-staging/main armhf libffi6 armhf 3.2.1-4 [18.5 kB]
Get:12 http://172.17.0.1/private stretch-staging/main armhf libsqlite3-0 armhf 3.10.2-1 [408 kB]
Get:13 http://172.17.0.1/private stretch-staging/main armhf libssl1.0.2 armhf 1.0.2f-2 [883 kB]
Get:14 http://172.17.0.1/private stretch-staging/main armhf libpython2.7-stdlib armhf 2.7.11-3 [1836 kB]
Get:15 http://172.17.0.1/private stretch-staging/main armhf python2.7 armhf 2.7.11-3 [266 kB]
Get:16 http://172.17.0.1/private stretch-staging/main armhf libpython-stdlib armhf 2.7.11-1 [19.5 kB]
Get:17 http://172.17.0.1/private stretch-staging/main armhf python armhf 2.7.11-1 [150 kB]
Get:18 http://172.17.0.1/private stretch-staging/main armhf libunistring0 armhf 0.9.3-5.2 [253 kB]
Get:19 http://172.17.0.1/private stretch-staging/main armhf libmagic1 armhf 1:5.25-2 [250 kB]
Get:20 http://172.17.0.1/private stretch-staging/main armhf file armhf 1:5.25-2 [61.2 kB]
Get:21 http://172.17.0.1/private stretch-staging/main armhf gettext-base armhf 0.19.7-2 [111 kB]
Get:22 http://172.17.0.1/private stretch-staging/main armhf libicu55 armhf 55.1-7 [7380 kB]
Get:23 http://172.17.0.1/private stretch-staging/main armhf libxml2 armhf 2.9.3+dfsg1-1 [800 kB]
Get:24 http://172.17.0.1/private stretch-staging/main armhf autotools-dev all 20150820.1 [71.7 kB]
Get:25 http://172.17.0.1/private stretch-staging/main armhf libglib2.0-0 armhf 2.46.2-3 [2482 kB]
Get:26 http://172.17.0.1/private stretch-staging/main armhf libcroco3 armhf 0.6.11-1 [131 kB]
Get:27 http://172.17.0.1/private stretch-staging/main armhf gettext armhf 0.19.7-2 [1400 kB]
Get:28 http://172.17.0.1/private stretch-staging/main armhf intltool-debian all 0.35.0+20060710.4 [26.3 kB]
Get:29 http://172.17.0.1/private stretch-staging/main armhf po-debconf all 1.0.19 [249 kB]
Get:30 http://172.17.0.1/private stretch-staging/main armhf libarchive-zip-perl all 1.56-2 [94.9 kB]
Get:31 http://172.17.0.1/private stretch-staging/main armhf libfile-stripnondeterminism-perl all 0.015-1 [11.0 kB]
Get:32 http://172.17.0.1/private stretch-staging/main armhf libtimedate-perl all 2.3000-2 [42.2 kB]
Get:33 http://172.17.0.1/private stretch-staging/main armhf dh-strip-nondeterminism all 0.015-1 [6810 B]
Get:34 http://172.17.0.1/private stretch-staging/main armhf debhelper all 9.20160115 [827 kB]
debconf: delaying package configuration, since apt-utils is not installed
Fetched 21.6 MB in 7s (2737 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 ... 12695 files and directories currently installed.)
Preparing to unpack .../groff-base_1.22.3-7_armhf.deb ...
Unpacking groff-base (1.22.3-7) ...
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-2_armhf.deb ...
Unpacking libpipeline1:armhf (1.4.1-2) ...
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.11-3_armhf.deb ...
Unpacking libpython2.7-minimal:armhf (2.7.11-3) ...
Selecting previously unselected package python2.7-minimal.
Preparing to unpack .../python2.7-minimal_2.7.11-3_armhf.deb ...
Unpacking python2.7-minimal (2.7.11-3) ...
Selecting previously unselected package python-minimal.
Preparing to unpack .../python-minimal_2.7.11-1_armhf.deb ...
Unpacking python-minimal (2.7.11-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-4_armhf.deb ...
Unpacking libffi6:armhf (3.2.1-4) ...
Selecting previously unselected package libsqlite3-0:armhf.
Preparing to unpack .../libsqlite3-0_3.10.2-1_armhf.deb ...
Unpacking libsqlite3-0:armhf (3.10.2-1) ...
Selecting previously unselected package libssl1.0.2:armhf.
Preparing to unpack .../libssl1.0.2_1.0.2f-2_armhf.deb ...
Unpacking libssl1.0.2:armhf (1.0.2f-2) ...
Selecting previously unselected package libpython2.7-stdlib:armhf.
Preparing to unpack .../libpython2.7-stdlib_2.7.11-3_armhf.deb ...
Unpacking libpython2.7-stdlib:armhf (2.7.11-3) ...
Selecting previously unselected package python2.7.
Preparing to unpack .../python2.7_2.7.11-3_armhf.deb ...
Unpacking python2.7 (2.7.11-3) ...
Selecting previously unselected package libpython-stdlib:armhf.
Preparing to unpack .../libpython-stdlib_2.7.11-1_armhf.deb ...
Unpacking libpython-stdlib:armhf (2.7.11-1) ...
Processing triggers for libc-bin (2.21-7) ...
Setting up libpython2.7-minimal:armhf (2.7.11-3) ...
Setting up python2.7-minimal (2.7.11-3) ...
Setting up python-minimal (2.7.11-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 ... 14058 files and directories currently installed.)
Preparing to unpack .../python_2.7.11-1_armhf.deb ...
Unpacking python (2.7.11-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.7-2_armhf.deb ...
Unpacking gettext-base (0.19.7-2) ...
Selecting previously unselected package libicu55:armhf.
Preparing to unpack .../libicu55_55.1-7_armhf.deb ...
Unpacking libicu55:armhf (55.1-7) ...
Selecting previously unselected package libxml2:armhf.
Preparing to unpack .../libxml2_2.9.3+dfsg1-1_armhf.deb ...
Unpacking libxml2:armhf (2.9.3+dfsg1-1) ...
Selecting previously unselected package autotools-dev.
Preparing to unpack .../autotools-dev_20150820.1_all.deb ...
Unpacking autotools-dev (20150820.1) ...
Selecting previously unselected package libglib2.0-0:armhf.
Preparing to unpack .../libglib2.0-0_2.46.2-3_armhf.deb ...
Unpacking libglib2.0-0:armhf (2.46.2-3) ...
Selecting previously unselected package libcroco3:armhf.
Preparing to unpack .../libcroco3_0.6.11-1_armhf.deb ...
Unpacking libcroco3:armhf (0.6.11-1) ...
Selecting previously unselected package gettext.
Preparing to unpack .../gettext_0.19.7-2_armhf.deb ...
Unpacking gettext (0.19.7-2) ...
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.19_all.deb ...
Unpacking po-debconf (1.0.19) ...
Selecting previously unselected package libarchive-zip-perl.
Preparing to unpack .../libarchive-zip-perl_1.56-2_all.deb ...
Unpacking libarchive-zip-perl (1.56-2) ...
Selecting previously unselected package libfile-stripnondeterminism-perl.
Preparing to unpack .../libfile-stripnondeterminism-perl_0.015-1_all.deb ...
Unpacking libfile-stripnondeterminism-perl (0.015-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.015-1_all.deb ...
Unpacking dh-strip-nondeterminism (0.015-1) ...
Selecting previously unselected package debhelper.
Preparing to unpack .../debhelper_9.20160115_all.deb ...
Unpacking debhelper (9.20160115) ...
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.21-7) ...
Setting up groff-base (1.22.3-7) ...
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-2) ...
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-4) ...
Setting up libsqlite3-0:armhf (3.10.2-1) ...
Setting up libssl1.0.2:armhf (1.0.2f-2) ...
Setting up libpython2.7-stdlib:armhf (2.7.11-3) ...
Setting up python2.7 (2.7.11-3) ...
Setting up libpython-stdlib:armhf (2.7.11-1) ...
Setting up python (2.7.11-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.7-2) ...
Setting up libicu55:armhf (55.1-7) ...
Setting up libxml2:armhf (2.9.3+dfsg1-1) ...
Setting up autotools-dev (20150820.1) ...
Setting up libglib2.0-0:armhf (2.46.2-3) ...
No schema files found: doing nothing.
Setting up libcroco3:armhf (0.6.11-1) ...
Setting up gettext (0.19.7-2) ...
Setting up intltool-debian (0.35.0+20060710.4) ...
Setting up po-debconf (1.0.19) ...
Setting up libarchive-zip-perl (1.56-2) ...
Setting up libfile-stripnondeterminism-perl (0.015-1) ...
Setting up libtimedate-perl (2.3000-2) ...
Setting up dh-strip-nondeterminism (0.015-1) ...
Setting up debhelper (9.20160115) ...
Setting up sbuild-build-depends-z3-dummy (0.invalid.0) ...
Processing triggers for libc-bin (2.21-7) ...
W: No sandbox user '_apt' on the system, can not drop privileges
+------------------------------------------------------------------------------+
| Build environment |
+------------------------------------------------------------------------------+
Kernel: Linux 3.19.0-trunk-armmp armhf (armv7l)
Toolchain package versions: binutils_2.26-3 dpkg-dev_1.18.4 g++-5_5.3.1-8+rpi1 gcc-5_5.3.1-8+rpi1 libc6-dev_2.21-7 libstdc++-5-dev_5.3.1-8+rpi1 libstdc++6_5.3.1-8+rpi1 linux-libc-dev_3.18.5-1~exp1+rpi19+stretch
Package versions: adduser_3.113+nmu3 apt_1.2.3 autotools-dev_20150820.1 base-files_9.5+rpi1 base-passwd_3.5.39 bash_4.3-14 binutils_2.26-3 bsdmainutils_9.0.6 bsdutils_1:2.27.1-3 build-essential_11.7 bzip2_1.0.6-8 coreutils_8.24-1 cpio_2.11+dfsg-4.1 cpp_4:5.3.1-1+rpi1 cpp-5_5.3.1-8+rpi1 dash_0.5.8-2.1 debconf_1.5.58 debfoster_2.7-2 debhelper_9.20160115 debianutils_4.7 dh-strip-nondeterminism_0.015-1 diffutils_1:3.3-3 dmsetup_2:1.02.115-2 dpkg_1.18.4 dpkg-dev_1.18.4 e2fslibs_1.42.13-1 e2fsprogs_1.42.13-1 fakeroot_1.20.2-1 file_1:5.25-2 findutils_4.6.0+git+20160126-2 g++_4:5.3.1-1+rpi1 g++-5_5.3.1-8+rpi1 gcc_4:5.3.1-1+rpi1 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-4 gcc-4.9-base_4.9.3-10 gcc-5_5.3.1-8+rpi1 gcc-5-base_5.3.1-8+rpi1 gettext_0.19.7-2 gettext-base_0.19.7-2 gnupg_1.4.20-1 gpgv_1.4.20-1 grep_2.22-1 groff-base_1.22.3-7 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.2 intltool-debian_0.35.0+20060710.4 klibc-utils_2.0.4-7+rpi1 kmod_22-1 libacl1_2.2.52-3 libapparmor1_2.10-3 libapt-pkg5.0_1.2.3 libarchive-zip-perl_1.56-2 libasan2_5.3.1-8+rpi1 libatomic1_5.3.1-8+rpi1 libattr1_1:2.4.47-2 libaudit-common_1:2.4.5-1 libaudit1_1:2.4.5-1 libblkid1_2.27.1-3 libbz2-1.0_1.0.6-8 libc-bin_2.21-7 libc-dev-bin_2.21-7 libc6_2.21-7 libc6-dev_2.21-7 libcap2_1:2.24-12 libcap2-bin_1:2.24-12 libcc1-0_5.3.1-8+rpi1 libcomerr2_1.42.13-1 libcroco3_0.6.11-1 libcryptsetup4_2:1.7.0-2 libdb5.3_5.3.28-11 libdbus-1-3_1.10.6-1 libdebconfclient0_0.204 libdevmapper1.02.1_2:1.02.115-2 libdpkg-perl_1.18.4 libdrm2_2.4.66-2 libexpat1_2.1.0-7 libfakeroot_1.20.2-1 libfdisk1_2.27.1-3 libffi6_3.2.1-4 libfile-stripnondeterminism-perl_0.015-1 libgc1c2_1:7.4.2-7.3 libgcc-5-dev_5.3.1-8+rpi1 libgcc1_1:5.3.1-8+rpi1 libgcrypt20_1.6.4-5 libgdbm3_1.8.3-13.1 libglib2.0-0_2.46.2-3 libgmp10_2:6.1.0+dfsg-2 libgomp1_5.3.1-8+rpi1 libgpg-error0_1.21-1 libicu55_55.1-7 libisl15_0.16.1-1 libklibc_2.0.4-7+rpi1 libkmod2_22-1 liblz4-1_0.0~r131-1 liblzma5_5.1.1alpha+20120614-2.1 libmagic1_1:5.25-2 libmount1_2.27.1-3 libmpc3_1.0.3-1 libmpfr4_3.1.3-2 libncurses5_6.0+20151024-2 libncursesw5_6.0+20151024-2 libpam-modules_1.1.8-3.2 libpam-modules-bin_1.1.8-3.2 libpam-runtime_1.1.8-3.2 libpam0g_1.1.8-3.2 libpcre3_2:8.38-1 libperl5.22_5.22.1-5 libpipeline1_1.4.1-2 libpng12-0_1.2.54-1 libprocps5_2:3.3.11-3 libpython-stdlib_2.7.11-1 libpython2.7-minimal_2.7.11-3 libpython2.7-stdlib_2.7.11-3 libreadline6_6.3-8+b3 libseccomp2_2.2.3-2 libselinux1_2.4-3 libsemanage-common_2.4-3 libsemanage1_2.4-3 libsepol1_2.4-2 libsmartcols1_2.27.1-3 libsqlite3-0_3.10.2-1 libss2_1.42.13-1 libssl1.0.2_1.0.2f-2 libstdc++-5-dev_5.3.1-8+rpi1 libstdc++6_5.3.1-8+rpi1 libsystemd0_228-6 libtext-charwidth-perl_0.04-7+b6 libtext-iconv-perl_1.7-5+b7 libtext-wrapi18n-perl_0.06-7.1 libtimedate-perl_2.3000-2 libtinfo5_6.0+20151024-2 libubsan0_5.3.1-8+rpi1 libudev1_228-6 libunistring0_0.9.3-5.2 libusb-0.1-4_2:0.1.12-28 libustr-1.0-1_1.0.4-5 libuuid1_2.27.1-3 libxml2_2.9.3+dfsg1-1 linux-libc-dev_3.18.5-1~exp1+rpi19+stretch login_1:4.2-3.1 lsb-base_9.20160110+rpi1 make_4.1-5 makedev_2.3.1-93 man-db_2.7.5-1 manpages_4.04-1 mawk_1.3.3-17 mime-support_3.59 mount_2.27.1-3 multiarch-support_2.21-7 nano_2.5.1-1 ncurses-base_6.0+20151024-2 ncurses-bin_6.0+20151024-2 passwd_1:4.2-3.1 patch_2.7.5-1 perl_5.22.1-5 perl-base_5.22.1-5 perl-modules-5.22_5.22.1-7 po-debconf_1.0.19 procps_2:3.3.11-3 python_2.7.11-1 python-minimal_2.7.11-1 python2.7_2.7.11-3 python2.7-minimal_2.7.11-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-6.1 sensible-utils_0.0.9 startpar_0.59-3 systemd_228-6 systemd-sysv_228-6 sysv-rc_2.88dsf-59.2 sysvinit-utils_2.88dsf-59.2 tar_1.28-2.1 tzdata_2016a-1 udev_228-6 util-linux_2.27.1-3 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=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=111
SCHROOT_GROUP=buildd
SCHROOT_SESSION_ID=stretch-staging-armhf-sbuild-b5faec98-69df-4440-b368-ff2a84ec5c9b
SCHROOT_UID=106
SCHROOT_USER=buildd
SHELL=/bin/sh
TERM=linux
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
dh_update_autotools_config -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:9: 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/tactic/bv/bv1_blaster_tactic.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/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:17: 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: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.18 :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.08 :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.14 :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 30.23 :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.23 :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.08 :before-memory 1793.13 :after-memory 1793.13)
(multiplication with floats: :time 0.02 :before-memory 1793.13 :after-memory 1793.13)
Testing multiplication performace using small rationals
(multiplication with rationals :time 1.12 :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.27 :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 214.96 :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 216.64 :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))))
debian/rules:79: recipe for target 'override_dh_auto_test' failed
make[1]: *** [override_dh_auto_test] Aborted
make[1]: Leaving directory '/<<PKGBUILDDIR>>'
debian/rules:13: recipe for target 'build-arch' failed
make: *** [build-arch] Error 2
dpkg-buildpackage: error: debian/rules build-arch gave error exit status 2
--------------------------------------------------------------------------------
Build finished at 20160224-1541
Finished
--------
E: Build failure (dpkg-buildpackage died)
+------------------------------------------------------------------------------+
| Cleanup |
+------------------------------------------------------------------------------+
Purging /<<BUILDDIR>>
Not cleaning session: cloned chroot in use
+------------------------------------------------------------------------------+
| Summary |
+------------------------------------------------------------------------------+
Build Architecture: armhf
Build-Space: 1559516
Build-Time: 5546
Distribution: stretch-staging
Fail-Stage: build
Host Architecture: armhf
Install-Time: 249
Job: z3_4.4.0-2
Machine Architecture: armhf
Package: z3
Package-Time: 5846
Source-Version: 4.4.0-2
Space: 1559516
Status: attempted
Version: 4.4.0-2
--------------------------------------------------------------------------------
Finished at 20160224-1541
Build needed 01:37:26, 1559516k disc space