Raspbian Package Auto-Building

Build log for z3 (4.4.0-2) on armhf

z3 → 4.4.0-2 → armhf → 2016-05-27 09:58:54 

sbuild (Debian sbuild) 0.66.0 (04 Oct 2015) on bm-wb-04

+==============================================================================+
| z3 4.4.0-2 (armhf)                                         27 May 2016 08:15 |
+==============================================================================+

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-yk2KT3/z3-4.4.0' with '<<PKGBUILDDIR>>'
I: NOTICE: Log filtering will replace 'build/z3-yk2KT3' with '<<BUILDDIR>>'
I: NOTICE: Log filtering will replace 'var/lib/schroot/mount/stretch-staging-armhf-sbuild-b2108ec5-6a4a-4783-a849-c006bfa26aa2' 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 [8995 kB]
Get:3 http://172.17.0.1/private stretch-staging/main armhf Packages [11.0 MB]
Fetched 20.0 MB in 21s (910 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 0s (6651 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-LPX8mS/apt_archive/sbuild-build-depends-core-dummy.deb'.
OK
Get:1 file:/<<BUILDDIR>>/resolver-LPX8mS/apt_archive ./ InRelease
Ign:1 file:/<<BUILDDIR>>/resolver-LPX8mS/apt_archive ./ InRelease
Get:2 file:/<<BUILDDIR>>/resolver-LPX8mS/apt_archive ./ Release [2119 B]
Get:2 file:/<<BUILDDIR>>/resolver-LPX8mS/apt_archive ./ Release [2119 B]
Get:3 file:/<<BUILDDIR>>/resolver-LPX8mS/apt_archive ./ Release.gpg [299 B]
Get:3 file:/<<BUILDDIR>>/resolver-LPX8mS/apt_archive ./ Release.gpg [299 B]
Get:4 file:/<<BUILDDIR>>/resolver-LPX8mS/apt_archive ./ Sources [214 B]
Get:5 file:/<<BUILDDIR>>/resolver-LPX8mS/apt_archive ./ Packages [526 B]
Reading package lists...
W: No sandbox user '_apt' on the system, can not drop privileges
W: file:///<<BUILDDIR>>/resolver-LPX8mS/apt_archive/./Release.gpg: Signature by key 3493EC2B8E6DC280C121C60435506D9A48F77B2E uses weak digest algorithm (SHA1)
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 17 not upgraded.
Need to get 0 B/762 B of archives.
After this operation, 0 B of additional disk space will be used.
Get:1 file:/<<BUILDDIR>>/resolver-LPX8mS/apt_archive ./ sbuild-build-depends-core-dummy 0.invalid.0 [762 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 ... 13638 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-T6T46X/apt_archive/sbuild-build-depends-z3-dummy.deb'.
OK
Get:1 file:/<<BUILDDIR>>/resolver-T6T46X/apt_archive ./ InRelease
Ign:1 file:/<<BUILDDIR>>/resolver-T6T46X/apt_archive ./ InRelease
Get:2 file:/<<BUILDDIR>>/resolver-T6T46X/apt_archive ./ Release [2119 B]
Get:2 file:/<<BUILDDIR>>/resolver-T6T46X/apt_archive ./ Release [2119 B]
Get:3 file:/<<BUILDDIR>>/resolver-T6T46X/apt_archive ./ Release.gpg [299 B]
Get:3 file:/<<BUILDDIR>>/resolver-T6T46X/apt_archive ./ Release.gpg [299 B]
Get:4 file:/<<BUILDDIR>>/resolver-T6T46X/apt_archive ./ Sources [213 B]
Get:5 file:/<<BUILDDIR>>/resolver-T6T46X/apt_archive ./ Packages [528 B]
Reading package lists...
W: No sandbox user '_apt' on the system, can not drop privileges
W: file:///<<BUILDDIR>>/resolver-T6T46X/apt_archive/./Release.gpg: Signature by key 3493EC2B8E6DC280C121C60435506D9A48F77B2E uses weak digest algorithm (SHA1)
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:
  autoconf automake autopoint autotools-dev bsdmainutils debhelper
  dh-autoreconf dh-strip-nondeterminism file gettext gettext-base groff-base
  intltool-debian libarchive-zip-perl libbsd0 libcroco3 libexpat1 libffi6
  libfile-stripnondeterminism-perl libglib2.0-0 libicu55 libmagic1
  libpipeline1 libpython-stdlib libpython2.7-minimal libpython2.7-stdlib
  libsigsegv2 libsqlite3-0 libssl1.0.2 libtool libunistring0 libxml2 m4 man-db
  mime-support po-debconf python python-minimal python2.7 python2.7-minimal
Suggested packages:
  autoconf-archive gnu-standards autoconf-doc wamerican | wordlist whois
  vacation dh-make gettext-doc libasprintf-dev libgettextpo-dev groff
  libtool-doc gfortran | fortran95-compiler gcj-jdk 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
  libltdl-dev xml-core libmail-sendmail-perl
The following NEW packages will be installed:
  autoconf automake autopoint autotools-dev bsdmainutils debhelper
  dh-autoreconf dh-strip-nondeterminism file gettext gettext-base groff-base
  intltool-debian libarchive-zip-perl libbsd0 libcroco3 libexpat1 libffi6
  libfile-stripnondeterminism-perl libglib2.0-0 libicu55 libmagic1
  libpipeline1 libpython-stdlib libpython2.7-minimal libpython2.7-stdlib
  libsigsegv2 libsqlite3-0 libssl1.0.2 libtool libunistring0 libxml2 m4 man-db
  mime-support po-debconf python python-minimal python2.7 python2.7-minimal
  sbuild-build-depends-z3-dummy
0 upgraded, 41 newly installed, 0 to remove and 17 not upgraded.
Need to get 23.8 MB/23.8 MB of archives.
After this operation, 82.9 MB of additional disk space will be used.
Get:1 file:/<<BUILDDIR>>/resolver-T6T46X/apt_archive ./ sbuild-build-depends-z3-dummy 0.invalid.0 [764 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 libbsd0 armhf 0.8.3-1 [89.0 kB]
Get:4 http://172.17.0.1/private stretch-staging/main armhf bsdmainutils armhf 9.0.10 [177 kB]
Get:5 http://172.17.0.1/private stretch-staging/main armhf libpipeline1 armhf 1.4.1-2 [23.7 kB]
Get:6 http://172.17.0.1/private stretch-staging/main armhf man-db armhf 2.7.5-1 [975 kB]
Get:7 http://172.17.0.1/private stretch-staging/main armhf libpython2.7-minimal armhf 2.7.11-9 [382 kB]
Get:8 http://172.17.0.1/private stretch-staging/main armhf python2.7-minimal armhf 2.7.11-9 [1163 kB]
Get:9 http://172.17.0.1/private stretch-staging/main armhf python-minimal armhf 2.7.11-1 [40.0 kB]
Get:10 http://172.17.0.1/private stretch-staging/main armhf mime-support all 3.60 [36.7 kB]
Get:11 http://172.17.0.1/private stretch-staging/main armhf libexpat1 armhf 2.1.1-2 [60.2 kB]
Get:12 http://172.17.0.1/private stretch-staging/main armhf libffi6 armhf 3.2.1-4 [18.5 kB]
Get:13 http://172.17.0.1/private stretch-staging/main armhf libsqlite3-0 armhf 3.12.2-1 [464 kB]
Get:14 http://172.17.0.1/private stretch-staging/main armhf libssl1.0.2 armhf 1.0.2h-1 [889 kB]
Get:15 http://172.17.0.1/private stretch-staging/main armhf libpython2.7-stdlib armhf 2.7.11-9 [1817 kB]
Get:16 http://172.17.0.1/private stretch-staging/main armhf python2.7 armhf 2.7.11-9 [271 kB]
Get:17 http://172.17.0.1/private stretch-staging/main armhf libpython-stdlib armhf 2.7.11-1 [19.5 kB]
Get:18 http://172.17.0.1/private stretch-staging/main armhf python armhf 2.7.11-1 [150 kB]
Get:19 http://172.17.0.1/private stretch-staging/main armhf libunistring0 armhf 0.9.3-5.2 [253 kB]
Get:20 http://172.17.0.1/private stretch-staging/main armhf libmagic1 armhf 1:5.25-2 [250 kB]
Get:21 http://172.17.0.1/private stretch-staging/main armhf file armhf 1:5.25-2 [61.2 kB]
Get:22 http://172.17.0.1/private stretch-staging/main armhf gettext-base armhf 0.19.7-2 [111 kB]
Get:23 http://172.17.0.1/private stretch-staging/main armhf libicu55 armhf 55.1-7 [7380 kB]
Get:24 http://172.17.0.1/private stretch-staging/main armhf libxml2 armhf 2.9.3+dfsg1-1 [800 kB]
Get:25 http://172.17.0.1/private stretch-staging/main armhf libsigsegv2 armhf 2.10-5 [28.4 kB]
Get:26 http://172.17.0.1/private stretch-staging/main armhf m4 armhf 1.4.17-5 [239 kB]
Get:27 http://172.17.0.1/private stretch-staging/main armhf autoconf all 2.69-10 [338 kB]
Get:28 http://172.17.0.1/private stretch-staging/main armhf autotools-dev all 20160430.1 [72.6 kB]
Get:29 http://172.17.0.1/private stretch-staging/main armhf automake all 1:1.15-4 [735 kB]
Get:30 http://172.17.0.1/private stretch-staging/main armhf autopoint all 0.19.7-2 [424 kB]
Get:31 http://172.17.0.1/private stretch-staging/main armhf libglib2.0-0 armhf 2.48.1-1 [2548 kB]
Get:32 http://172.17.0.1/private stretch-staging/main armhf libcroco3 armhf 0.6.11-1 [131 kB]
Get:33 http://172.17.0.1/private stretch-staging/main armhf gettext armhf 0.19.7-2 [1400 kB]
Get:34 http://172.17.0.1/private stretch-staging/main armhf intltool-debian all 0.35.0+20060710.4 [26.3 kB]
Get:35 http://172.17.0.1/private stretch-staging/main armhf po-debconf all 1.0.19 [249 kB]
Get:36 http://172.17.0.1/private stretch-staging/main armhf libarchive-zip-perl all 1.57-1 [95.1 kB]
Get:37 http://172.17.0.1/private stretch-staging/main armhf libfile-stripnondeterminism-perl all 0.016-1 [11.9 kB]
Get:38 http://172.17.0.1/private stretch-staging/main armhf dh-strip-nondeterminism all 0.016-1 [6998 B]
Get:39 http://172.17.0.1/private stretch-staging/main armhf libtool all 2.4.6-0.1 [200 kB]
Get:40 http://172.17.0.1/private stretch-staging/main armhf dh-autoreconf all 12 [15.8 kB]
Get:41 http://172.17.0.1/private stretch-staging/main armhf debhelper all 9.20160403 [800 kB]
debconf: delaying package configuration, since apt-utils is not installed
Fetched 23.8 MB in 3s (7219 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 ... 13638 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 libbsd0:armhf.
Preparing to unpack .../libbsd0_0.8.3-1_armhf.deb ...
Unpacking libbsd0:armhf (0.8.3-1) ...
Selecting previously unselected package bsdmainutils.
Preparing to unpack .../bsdmainutils_9.0.10_armhf.deb ...
Unpacking bsdmainutils (9.0.10) ...
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-9_armhf.deb ...
Unpacking libpython2.7-minimal:armhf (2.7.11-9) ...
Selecting previously unselected package python2.7-minimal.
Preparing to unpack .../python2.7-minimal_2.7.11-9_armhf.deb ...
Unpacking python2.7-minimal (2.7.11-9) ...
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.60_all.deb ...
Unpacking mime-support (3.60) ...
Selecting previously unselected package libexpat1:armhf.
Preparing to unpack .../libexpat1_2.1.1-2_armhf.deb ...
Unpacking libexpat1:armhf (2.1.1-2) ...
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.12.2-1_armhf.deb ...
Unpacking libsqlite3-0:armhf (3.12.2-1) ...
Selecting previously unselected package libssl1.0.2:armhf.
Preparing to unpack .../libssl1.0.2_1.0.2h-1_armhf.deb ...
Unpacking libssl1.0.2:armhf (1.0.2h-1) ...
Selecting previously unselected package libpython2.7-stdlib:armhf.
Preparing to unpack .../libpython2.7-stdlib_2.7.11-9_armhf.deb ...
Unpacking libpython2.7-stdlib:armhf (2.7.11-9) ...
Selecting previously unselected package python2.7.
Preparing to unpack .../python2.7_2.7.11-9_armhf.deb ...
Unpacking python2.7 (2.7.11-9) ...
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.22-7) ...
Setting up libpython2.7-minimal:armhf (2.7.11-9) ...
Setting up python2.7-minimal (2.7.11-9) ...
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 ... 15007 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 libsigsegv2:armhf.
Preparing to unpack .../libsigsegv2_2.10-5_armhf.deb ...
Unpacking libsigsegv2:armhf (2.10-5) ...
Selecting previously unselected package m4.
Preparing to unpack .../archives/m4_1.4.17-5_armhf.deb ...
Unpacking m4 (1.4.17-5) ...
Selecting previously unselected package autoconf.
Preparing to unpack .../autoconf_2.69-10_all.deb ...
Unpacking autoconf (2.69-10) ...
Selecting previously unselected package autotools-dev.
Preparing to unpack .../autotools-dev_20160430.1_all.deb ...
Unpacking autotools-dev (20160430.1) ...
Selecting previously unselected package automake.
Preparing to unpack .../automake_1%3a1.15-4_all.deb ...
Unpacking automake (1:1.15-4) ...
Selecting previously unselected package autopoint.
Preparing to unpack .../autopoint_0.19.7-2_all.deb ...
Unpacking autopoint (0.19.7-2) ...
Selecting previously unselected package libglib2.0-0:armhf.
Preparing to unpack .../libglib2.0-0_2.48.1-1_armhf.deb ...
Unpacking libglib2.0-0:armhf (2.48.1-1) ...
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.57-1_all.deb ...
Unpacking libarchive-zip-perl (1.57-1) ...
Selecting previously unselected package libfile-stripnondeterminism-perl.
Preparing to unpack .../libfile-stripnondeterminism-perl_0.016-1_all.deb ...
Unpacking libfile-stripnondeterminism-perl (0.016-1) ...
Selecting previously unselected package dh-strip-nondeterminism.
Preparing to unpack .../dh-strip-nondeterminism_0.016-1_all.deb ...
Unpacking dh-strip-nondeterminism (0.016-1) ...
Selecting previously unselected package libtool.
Preparing to unpack .../libtool_2.4.6-0.1_all.deb ...
Unpacking libtool (2.4.6-0.1) ...
Selecting previously unselected package dh-autoreconf.
Preparing to unpack .../dh-autoreconf_12_all.deb ...
Unpacking dh-autoreconf (12) ...
Selecting previously unselected package debhelper.
Preparing to unpack .../debhelper_9.20160403_all.deb ...
Unpacking debhelper (9.20160403) ...
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.22-7) ...
Setting up groff-base (1.22.3-7) ...
Setting up libbsd0:armhf (0.8.3-1) ...
Setting up bsdmainutils (9.0.10) ...
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.60) ...
Setting up libexpat1:armhf (2.1.1-2) ...
Setting up libffi6:armhf (3.2.1-4) ...
Setting up libsqlite3-0:armhf (3.12.2-1) ...
Setting up libssl1.0.2:armhf (1.0.2h-1) ...
Setting up libpython2.7-stdlib:armhf (2.7.11-9) ...
Setting up python2.7 (2.7.11-9) ...
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 libsigsegv2:armhf (2.10-5) ...
Setting up m4 (1.4.17-5) ...
Setting up autoconf (2.69-10) ...
Setting up autotools-dev (20160430.1) ...
Setting up automake (1:1.15-4) ...
update-alternatives: using /usr/bin/automake-1.15 to provide /usr/bin/automake (automake) in auto mode
Setting up autopoint (0.19.7-2) ...
Setting up libglib2.0-0:armhf (2.48.1-1) ...
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.57-1) ...
Setting up libfile-stripnondeterminism-perl (0.016-1) ...
Setting up libtool (2.4.6-0.1) ...
Setting up dh-strip-nondeterminism (0.016-1) ...
Setting up debhelper (9.20160403) ...
Setting up dh-autoreconf (12) ...
Setting up sbuild-build-depends-z3-dummy (0.invalid.0) ...
Processing triggers for libc-bin (2.22-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-8 dpkg-dev_1.18.7 g++-5_5.3.1-19 gcc-5_5.3.1-19 libc6-dev_2.22-7 libstdc++-4.9-dev_4.9.3-14 libstdc++-5-dev_5.3.1-19 libstdc++6_6.1.1-1+rpi1 linux-libc-dev_3.18.5-1~exp1+rpi19+stretch
Package versions: acl_2.2.52-3 adduser_3.114 apt_1.2.12 autoconf_2.69-10 automake_1:1.15-4 autopoint_0.19.7-2 autotools-dev_20160430.1 base-files_9.6+rpi1 base-passwd_3.5.39 bash_4.3-14 binutils_2.26-8 bsdmainutils_9.0.10 bsdutils_1:2.28-5 build-essential_11.7 bzip2_1.0.6-8 coreutils_8.25-2 cpio_2.11+dfsg-5 cpp_4:5.3.1-1+rpi1 cpp-5_5.3.1-19 dash_0.5.8-2.2 debconf_1.5.59 debfoster_2.7-2 debhelper_9.20160403 debianutils_4.7 dh-autoreconf_12 dh-strip-nondeterminism_0.016-1 diffutils_1:3.3-3 dmsetup_2:1.02.124-1 dpkg_1.18.7 dpkg-dev_1.18.7 e2fslibs_1.43~WIP.2016.03.15-2 e2fsprogs_1.43~WIP.2016.03.15-2 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-19 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-14 gcc-5_5.3.1-19 gcc-5-base_5.3.1-19 gcc-6-base_6.1.1-1+rpi1 gettext_0.19.7-2 gettext-base_0.19.7-2 gnupg_1.4.20-6 gpgv_1.4.20-6 grep_2.25-1 groff-base_1.22.3-7 gzip_1.6-5 hostname_3.17 init_1.33 init-system-helpers_1.33 initscripts_2.88dsf-59.4 insserv_1.14.0-5.3 intltool-debian_0.35.0+20060710.4 klibc-utils_2.0.4-8+rpi1 kmod_22-1.1 libacl1_2.2.52-3 libapparmor1_2.10-4 libapt-pkg4.12_1.0.9.10 libapt-pkg5.0_1.2.12 libarchive-zip-perl_1.57-1 libasan1_4.9.3-14 libasan2_5.3.1-19 libatomic1_6.1.1-1+rpi1 libattr1_1:2.4.47-2 libaudit-common_1:2.5.2-1+rpi1 libaudit1_1:2.5.2-1+rpi1 libblkid1_2.28-5 libbsd0_0.8.3-1 libbz2-1.0_1.0.6-8 libc-bin_2.22-7 libc-dev-bin_2.22-7 libc6_2.22-7 libc6-dev_2.22-7 libcap2_1:2.24-12 libcap2-bin_1:2.24-12 libcc1-0_6.1.1-1+rpi1 libcomerr2_1.43~WIP.2016.03.15-2 libcroco3_0.6.11-1 libcryptsetup4_2:1.7.0-2 libdb5.3_5.3.28-11 libdbus-1-3_1.10.8-1 libdebconfclient0_0.210 libdevmapper1.02.1_2:1.02.124-1 libdpkg-perl_1.18.7 libdrm2_2.4.68-1 libexpat1_2.1.1-2 libfakeroot_1.20.2-1 libfdisk1_2.28-5 libffi6_3.2.1-4 libfile-stripnondeterminism-perl_0.016-1 libgc1c2_1:7.4.2-7.4 libgcc-4.9-dev_4.9.3-14 libgcc-5-dev_5.3.1-19 libgcc1_1:6.1.1-1+rpi1 libgcrypt20_1.7.0-2 libgdbm3_1.8.3-13.1 libglib2.0-0_2.48.1-1 libgmp10_2:6.1.0+dfsg-2 libgomp1_6.1.1-1+rpi1 libgpg-error0_1.22-2 libicu55_55.1-7 libisl15_0.16.1-1 libklibc_2.0.4-8+rpi1 libkmod2_22-1.1 liblz4-1_0.0~r131-2 liblzma5_5.1.1alpha+20120614-2.1 libmagic1_1:5.25-2 libmount1_2.28-5 libmpc3_1.0.3-1 libmpfr4_3.1.4-1 libncurses5_6.0+20160319-1 libncursesw5_6.0+20160319-1 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-3.1 libperl5.22_5.22.2-1 libpipeline1_1.4.1-2 libpng12-0_1.2.54-6 libprocps3_2:3.3.9-9 libprocps5_2:3.3.11-3 libpython-stdlib_2.7.11-1 libpython2.7-minimal_2.7.11-9 libpython2.7-stdlib_2.7.11-9 libreadline6_6.3-8+b3 libseccomp2_2.3.0-1 libselinux1_2.5-2 libsemanage-common_2.5-1 libsemanage1_2.5-1 libsepol1_2.5-1 libsigsegv2_2.10-5 libslang2_2.3.0-2.3 libsmartcols1_2.28-5 libsqlite3-0_3.12.2-1 libss2_1.43~WIP.2016.03.15-2 libssl1.0.2_1.0.2h-1 libstdc++-4.9-dev_4.9.3-14 libstdc++-5-dev_5.3.1-19 libstdc++6_6.1.1-1+rpi1 libsystemd0_229-5 libtimedate-perl_2.3000-2 libtinfo5_6.0+20160319-1 libtool_2.4.6-0.1 libubsan0_6.1.1-1+rpi1 libudev1_229-5 libunistring0_0.9.3-5.2 libusb-0.1-4_2:0.1.12-30 libustr-1.0-1_1.0.4-5 libuuid1_2.28-5 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 m4_1.4.17-5 make_4.1-9 makedev_2.3.1-93 man-db_2.7.5-1 manpages_4.06-1 mawk_1.3.3-17 mime-support_3.60 mount_2.28-5 multiarch-support_2.22-7 nano_2.5.3-3 ncurses-base_6.0+20160319-1 ncurses-bin_6.0+20160319-1 passwd_1:4.2-3.1 patch_2.7.5-1 perl_5.22.2-1 perl-base_5.22.2-1 perl-modules-5.22_5.22.2-1 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-9 python2.7-minimal_2.7.11-9 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-7.1 sensible-utils_0.0.9 startpar_0.59-3 systemd_229-5 systemd-sysv_229-5 sysv-rc_2.88dsf-59.4 sysvinit-utils_2.88dsf-59.4 tar_1.28-2.2+rpi1 tzdata_2016d-2 udev_229-5 util-linux_2.28-5 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=109
SCHROOT_GROUP=buildd
SCHROOT_SESSION_ID=stretch-staging-armhf-sbuild-b2108ec5-6a4a-4783-a849-c006bfa26aa2
SCHROOT_UID=104
SCHROOT_USER=buildd
SHELL=/bin/sh
USER=buildd

dpkg-buildpackage
-----------------

dpkg-buildpackage: info: source package z3
dpkg-buildpackage: info: source version 4.4.0-2
dpkg-buildpackage: info: source distribution unstable
 dpkg-source --before-build z3-4.4.0
dpkg-buildpackage: info: 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/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/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/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/smt2parser.cpp
src/interp/iz3interp.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/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.05 :before-memory 0.02 :after-memory 876.88)
resize 1000000000
out of memory
PASS
(test vector :time 0.05 :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.07 :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.07 :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 26.67 :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.09 :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.27 :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 32.33 :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.93 :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.02 :before-memory 1793.13 :after-memory 1793.13)

Testing multiplication performace using small rationals
(multiplication with rationals :time 1.09 :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.75 :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 201.79 :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 204.11 :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 20160527-0958

Finished
--------

E: Build failure (dpkg-buildpackage died)

+------------------------------------------------------------------------------+
| Cleanup                                                                      |
+------------------------------------------------------------------------------+

Purging /<<BUILDDIR>>
Not cleaning session: cloned chroot in use

+------------------------------------------------------------------------------+
| Summary                                                                      |
+------------------------------------------------------------------------------+

Build Architecture: armhf
Build-Space: 1559164
Build-Time: 5820
Distribution: stretch-staging
Fail-Stage: build
Host Architecture: armhf
Install-Time: 294
Job: z3_4.4.0-2
Machine Architecture: armhf
Package: z3
Package-Time: 6163
Source-Version: 4.4.0-2
Space: 1559164
Status: attempted
Version: 4.4.0-2
--------------------------------------------------------------------------------
Finished at 20160527-0958
Build needed 01:42:43, 1559164k disc space