Diff of the two buildlogs: -- --- b1/build.log 2020-08-13 02:11:05.492520693 +0000 +++ b2/build.log 2020-08-13 04:52:00.373374233 +0000 @@ -1,6 +1,6 @@ I: pbuilder: network access will be disabled during build -I: Current time: Wed Aug 12 12:37:01 -12 2020 -I: pbuilder-time-stamp: 1597279021 +I: Current time: Thu Aug 13 16:15:54 +14 2020 +I: pbuilder-time-stamp: 1597284954 I: Building the build Environment I: extracting base tarball [/var/cache/pbuilder/buster-reproducible-base.tgz] I: copying local configuration @@ -17,7 +17,7 @@ I: Extracting source gpgv: unknown type of key resource 'trustedkeys.kbx' gpgv: keyblock resource '/root/.gnupg/trustedkeys.kbx': General error -gpgv: Signature made Fri Aug 23 22:41:08 2019 -12 +gpgv: Signature made Sun Aug 25 00:41:08 2019 +14 gpgv: using RSA key EBF30A30A8D9C63BDA44C6945FB33F9359E9ED08 gpgv: issuer "anbe@debian.org" gpgv: Can't check signature: No public key @@ -39,136 +39,170 @@ dpkg-source: info: applying fix-build.patch I: using fakeroot in build. I: Installing the build-deps -I: user script /srv/workspace/pbuilder/13915/tmp/hooks/D02_print_environment starting +I: user script /srv/workspace/pbuilder/15030/tmp/hooks/D01_modify_environment starting +debug: Running on jtk1a. +I: Changing host+domainname to test build reproducibility +I: Adding a custom variable just for the fun of it... +I: Changing /bin/sh to bash +Removing 'diversion of /bin/sh to /bin/sh.distrib by dash' +Adding 'diversion of /bin/sh to /bin/sh.distrib by bash' +Removing 'diversion of /usr/share/man/man1/sh.1.gz to /usr/share/man/man1/sh.distrib.1.gz by dash' +Adding 'diversion of /usr/share/man/man1/sh.1.gz to /usr/share/man/man1/sh.distrib.1.gz by bash' +I: Setting pbuilder2's login shell to /bin/bash +I: Setting pbuilder2's GECOS to second user,second room,second work-phone,second home-phone,second other +I: user script /srv/workspace/pbuilder/15030/tmp/hooks/D01_modify_environment finished +I: user script /srv/workspace/pbuilder/15030/tmp/hooks/D02_print_environment starting I: set - BUILDDIR='/build' - BUILDUSERGECOS='first user,first room,first work-phone,first home-phone,first other' - BUILDUSERNAME='pbuilder1' - BUILD_ARCH='armhf' - DEBIAN_FRONTEND='noninteractive' - DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=3' - DISTRIBUTION='' - HOME='/root' - HOST_ARCH='armhf' + BASH=/bin/sh + BASHOPTS=checkwinsize:cmdhist:complete_fullquote:extquote:force_fignore:globasciiranges:hostcomplete:interactive_comments:progcomp:promptvars:sourcepath + BASH_ALIASES=() + BASH_ARGC=() + BASH_ARGV=() + BASH_CMDS=() + BASH_LINENO=([0]="12" [1]="0") + BASH_SOURCE=([0]="/tmp/hooks/D02_print_environment" [1]="/tmp/hooks/D02_print_environment") + BASH_VERSINFO=([0]="5" [1]="0" [2]="3" [3]="1" [4]="release" [5]="arm-unknown-linux-gnueabihf") + BASH_VERSION='5.0.3(1)-release' + BUILDDIR=/build + BUILDUSERGECOS='second user,second room,second work-phone,second home-phone,second other' + BUILDUSERNAME=pbuilder2 + BUILD_ARCH=armhf + DEBIAN_FRONTEND=noninteractive + DEB_BUILD_OPTIONS='buildinfo=+all reproducible=+all parallel=4' + DIRSTACK=() + DISTRIBUTION= + EUID=0 + FUNCNAME=([0]="Echo" [1]="main") + GROUPS=() + HOME=/root + HOSTNAME=i-capture-the-hostname + HOSTTYPE=arm + HOST_ARCH=armhf IFS=' ' - INVOCATION_ID='ee628f46c6f743b39e15e7d6928cdd94' - LANG='C' - LANGUAGE='en_US:en' - LC_ALL='C' - MAIL='/var/mail/root' - OPTIND='1' - PATH='/usr/sbin:/usr/bin:/sbin:/bin:/usr/games' - PBCURRENTCOMMANDLINEOPERATION='build' - PBUILDER_OPERATION='build' - PBUILDER_PKGDATADIR='/usr/share/pbuilder' - PBUILDER_PKGLIBDIR='/usr/lib/pbuilder' - PBUILDER_SYSCONFDIR='/etc' - PPID='13915' - PS1='# ' - PS2='> ' + INVOCATION_ID=4e6b9d89540d4b8fa1e2d738e9ccfe8f + LANG=C + LANGUAGE=it_CH:it + LC_ALL=C + MACHTYPE=arm-unknown-linux-gnueabihf + MAIL=/var/mail/root + OPTERR=1 + OPTIND=1 + OSTYPE=linux-gnueabihf + PATH=/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path + PBCURRENTCOMMANDLINEOPERATION=build + PBUILDER_OPERATION=build + PBUILDER_PKGDATADIR=/usr/share/pbuilder + PBUILDER_PKGLIBDIR=/usr/lib/pbuilder + PBUILDER_SYSCONFDIR=/etc + PIPESTATUS=([0]="0") + POSIXLY_CORRECT=y + PPID=15030 PS4='+ ' - PWD='/' - SHELL='/bin/bash' - SHLVL='2' - SUDO_COMMAND='/usr/bin/timeout -k 18.1h 18h /usr/bin/ionice -c 3 /usr/bin/nice /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/tmp.ROoL5UBnxH/pbuilderrc_9whQ --hookdir /etc/pbuilder/first-build-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/buster-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/tmp.ROoL5UBnxH/b1 --logfile b1/build.log z3_4.4.1-1~deb10u1.dsc' - SUDO_GID='111' - SUDO_UID='107' - SUDO_USER='jenkins' - TERM='unknown' - TZ='/usr/share/zoneinfo/Etc/GMT+12' - USER='root' - _='/usr/bin/systemd-run' - http_proxy='http://10.0.0.15:8000/' + PWD=/ + SHELL=/bin/bash + SHELLOPTS=braceexpand:errexit:hashall:interactive-comments:posix + SHLVL=3 + SUDO_COMMAND='/usr/bin/timeout -k 24.1h 24h /usr/bin/ionice -c 3 /usr/bin/nice -n 11 /usr/bin/unshare --uts -- /usr/sbin/pbuilder --build --configfile /srv/reproducible-results/rbuild-debian/tmp.ROoL5UBnxH/pbuilderrc_99rq --hookdir /etc/pbuilder/rebuild-hooks --debbuildopts -b --basetgz /var/cache/pbuilder/buster-reproducible-base.tgz --buildresult /srv/reproducible-results/rbuild-debian/tmp.ROoL5UBnxH/b2 --logfile b2/build.log z3_4.4.1-1~deb10u1.dsc' + SUDO_GID=113 + SUDO_UID=107 + SUDO_USER=jenkins + TERM=unknown + TZ=/usr/share/zoneinfo/Etc/GMT-14 + UID=0 + USER=root + _='I: set' + http_proxy=http://10.0.0.15:8000/ I: uname -a - Linux jtx1c 4.19.0-10-arm64 #1 SMP Debian 4.19.132-1 (2020-07-24) aarch64 GNU/Linux + Linux i-capture-the-hostname 4.19.0-10-armmp-lpae #1 SMP Debian 4.19.132-1 (2020-07-24) armv7l GNU/Linux I: ls -l /bin total 3328 - -rwxr-xr-x 1 root root 767656 Apr 17 2019 bash - -rwxr-xr-x 3 root root 26052 Jul 10 2019 bunzip2 - -rwxr-xr-x 3 root root 26052 Jul 10 2019 bzcat - lrwxrwxrwx 1 root root 6 Jul 10 2019 bzcmp -> bzdiff - -rwxr-xr-x 1 root root 2227 Jul 10 2019 bzdiff - lrwxrwxrwx 1 root root 6 Jul 10 2019 bzegrep -> bzgrep - -rwxr-xr-x 1 root root 4877 Jun 24 2019 bzexe - lrwxrwxrwx 1 root root 6 Jul 10 2019 bzfgrep -> bzgrep - -rwxr-xr-x 1 root root 3641 Jul 10 2019 bzgrep - -rwxr-xr-x 3 root root 26052 Jul 10 2019 bzip2 - -rwxr-xr-x 1 root root 9636 Jul 10 2019 bzip2recover - lrwxrwxrwx 1 root root 6 Jul 10 2019 bzless -> bzmore - -rwxr-xr-x 1 root root 1297 Jul 10 2019 bzmore - -rwxr-xr-x 1 root root 22432 Feb 28 2019 cat - -rwxr-xr-x 1 root root 38868 Feb 28 2019 chgrp - -rwxr-xr-x 1 root root 38836 Feb 28 2019 chmod - -rwxr-xr-x 1 root root 42972 Feb 28 2019 chown - -rwxr-xr-x 1 root root 88376 Feb 28 2019 cp - -rwxr-xr-x 1 root root 75516 Jan 17 2019 dash - -rwxr-xr-x 1 root root 71648 Feb 28 2019 date - -rwxr-xr-x 1 root root 51212 Feb 28 2019 dd - -rwxr-xr-x 1 root root 55672 Feb 28 2019 df - -rwxr-xr-x 1 root root 88444 Feb 28 2019 dir - -rwxr-xr-x 1 root root 54872 Jan 9 2019 dmesg - lrwxrwxrwx 1 root root 8 Sep 26 2018 dnsdomainname -> hostname - lrwxrwxrwx 1 root root 8 Sep 26 2018 domainname -> hostname - -rwxr-xr-x 1 root root 22364 Feb 28 2019 echo - -rwxr-xr-x 1 root root 28 Jan 7 2019 egrep - -rwxr-xr-x 1 root root 18260 Feb 28 2019 false - -rwxr-xr-x 1 root root 28 Jan 7 2019 fgrep - -rwxr-xr-x 1 root root 47356 Jan 9 2019 findmnt - -rwsr-xr-x 1 root root 21980 Apr 22 07:38 fusermount - -rwxr-xr-x 1 root root 124508 Jan 7 2019 grep - -rwxr-xr-x 2 root root 2345 Jan 5 2019 gunzip - -rwxr-xr-x 1 root root 6375 Jan 5 2019 gzexe - -rwxr-xr-x 1 root root 64232 Jan 5 2019 gzip - -rwxr-xr-x 1 root root 13784 Sep 26 2018 hostname - -rwxr-xr-x 1 root root 43044 Feb 28 2019 ln - -rwxr-xr-x 1 root root 34932 Jul 26 2018 login - -rwxr-xr-x 1 root root 88444 Feb 28 2019 ls - -rwxr-xr-x 1 root root 67036 Jan 9 2019 lsblk - -rwxr-xr-x 1 root root 47168 Feb 28 2019 mkdir - -rwxr-xr-x 1 root root 43040 Feb 28 2019 mknod - -rwxr-xr-x 1 root root 26552 Feb 28 2019 mktemp - -rwxr-xr-x 1 root root 26024 Jan 9 2019 more - -rwsr-xr-x 1 root root 34268 Jan 9 2019 mount - -rwxr-xr-x 1 root root 9688 Jan 9 2019 mountpoint - -rwxr-xr-x 1 root root 84284 Feb 28 2019 mv - lrwxrwxrwx 1 root root 8 Sep 26 2018 nisdomainname -> hostname - lrwxrwxrwx 1 root root 14 Feb 14 2019 pidof -> /sbin/killall5 - -rwxr-xr-x 1 root root 22416 Feb 28 2019 pwd - lrwxrwxrwx 1 root root 4 Apr 17 2019 rbash -> bash - -rwxr-xr-x 1 root root 26504 Feb 28 2019 readlink - -rwxr-xr-x 1 root root 42968 Feb 28 2019 rm - -rwxr-xr-x 1 root root 26496 Feb 28 2019 rmdir - -rwxr-xr-x 1 root root 14136 Jan 21 2019 run-parts - -rwxr-xr-x 1 root root 76012 Dec 22 2018 sed - lrwxrwxrwx 1 root root 4 Aug 10 20:25 sh -> dash - -rwxr-xr-x 1 root root 22384 Feb 28 2019 sleep - -rwxr-xr-x 1 root root 51124 Feb 28 2019 stty - -rwsr-xr-x 1 root root 42472 Jan 9 2019 su - -rwxr-xr-x 1 root root 22392 Feb 28 2019 sync - -rwxr-xr-x 1 root root 283324 Apr 23 2019 tar - -rwxr-xr-x 1 root root 9808 Jan 21 2019 tempfile - -rwxr-xr-x 1 root root 63464 Feb 28 2019 touch - -rwxr-xr-x 1 root root 18260 Feb 28 2019 true - -rwxr-xr-x 1 root root 9636 Apr 22 07:38 ulockmgr_server - -rwsr-xr-x 1 root root 21976 Jan 9 2019 umount - -rwxr-xr-x 1 root root 22380 Feb 28 2019 uname - -rwxr-xr-x 2 root root 2345 Jan 5 2019 uncompress - -rwxr-xr-x 1 root root 88444 Feb 28 2019 vdir - -rwxr-xr-x 1 root root 21980 Jan 9 2019 wdctl - -rwxr-xr-x 1 root root 946 Jan 21 2019 which - lrwxrwxrwx 1 root root 8 Sep 26 2018 ypdomainname -> hostname - -rwxr-xr-x 1 root root 1983 Jan 5 2019 zcat - -rwxr-xr-x 1 root root 1677 Jan 5 2019 zcmp - -rwxr-xr-x 1 root root 5879 Jan 5 2019 zdiff - -rwxr-xr-x 1 root root 29 Jan 5 2019 zegrep - -rwxr-xr-x 1 root root 29 Jan 5 2019 zfgrep - -rwxr-xr-x 1 root root 2080 Jan 5 2019 zforce - -rwxr-xr-x 1 root root 7584 Jan 5 2019 zgrep - -rwxr-xr-x 1 root root 2205 Jan 5 2019 zless - -rwxr-xr-x 1 root root 1841 Jan 5 2019 zmore - -rwxr-xr-x 1 root root 4552 Jan 5 2019 znew -I: user script /srv/workspace/pbuilder/13915/tmp/hooks/D02_print_environment finished + -rwxr-xr-x 1 root root 767656 Apr 18 2019 bash + -rwxr-xr-x 3 root root 26052 Jul 11 2019 bunzip2 + -rwxr-xr-x 3 root root 26052 Jul 11 2019 bzcat + lrwxrwxrwx 1 root root 6 Jul 11 2019 bzcmp -> bzdiff + -rwxr-xr-x 1 root root 2227 Jul 11 2019 bzdiff + lrwxrwxrwx 1 root root 6 Jul 11 2019 bzegrep -> bzgrep + -rwxr-xr-x 1 root root 4877 Jun 25 2019 bzexe + lrwxrwxrwx 1 root root 6 Jul 11 2019 bzfgrep -> bzgrep + -rwxr-xr-x 1 root root 3641 Jul 11 2019 bzgrep + -rwxr-xr-x 3 root root 26052 Jul 11 2019 bzip2 + -rwxr-xr-x 1 root root 9636 Jul 11 2019 bzip2recover + lrwxrwxrwx 1 root root 6 Jul 11 2019 bzless -> bzmore + -rwxr-xr-x 1 root root 1297 Jul 11 2019 bzmore + -rwxr-xr-x 1 root root 22432 Mar 1 2019 cat + -rwxr-xr-x 1 root root 38868 Mar 1 2019 chgrp + -rwxr-xr-x 1 root root 38836 Mar 1 2019 chmod + -rwxr-xr-x 1 root root 42972 Mar 1 2019 chown + -rwxr-xr-x 1 root root 88376 Mar 1 2019 cp + -rwxr-xr-x 1 root root 75516 Jan 18 2019 dash + -rwxr-xr-x 1 root root 71648 Mar 1 2019 date + -rwxr-xr-x 1 root root 51212 Mar 1 2019 dd + -rwxr-xr-x 1 root root 55672 Mar 1 2019 df + -rwxr-xr-x 1 root root 88444 Mar 1 2019 dir + -rwxr-xr-x 1 root root 54872 Jan 10 2019 dmesg + lrwxrwxrwx 1 root root 8 Sep 27 2018 dnsdomainname -> hostname + lrwxrwxrwx 1 root root 8 Sep 27 2018 domainname -> hostname + -rwxr-xr-x 1 root root 22364 Mar 1 2019 echo + -rwxr-xr-x 1 root root 28 Jan 8 2019 egrep + -rwxr-xr-x 1 root root 18260 Mar 1 2019 false + -rwxr-xr-x 1 root root 28 Jan 8 2019 fgrep + -rwxr-xr-x 1 root root 47356 Jan 10 2019 findmnt + -rwsr-xr-x 1 root root 21980 Apr 23 09:38 fusermount + -rwxr-xr-x 1 root root 124508 Jan 8 2019 grep + -rwxr-xr-x 2 root root 2345 Jan 6 2019 gunzip + -rwxr-xr-x 1 root root 6375 Jan 6 2019 gzexe + -rwxr-xr-x 1 root root 64232 Jan 6 2019 gzip + -rwxr-xr-x 1 root root 13784 Sep 27 2018 hostname + -rwxr-xr-x 1 root root 43044 Mar 1 2019 ln + -rwxr-xr-x 1 root root 34932 Jul 27 2018 login + -rwxr-xr-x 1 root root 88444 Mar 1 2019 ls + -rwxr-xr-x 1 root root 67036 Jan 10 2019 lsblk + -rwxr-xr-x 1 root root 47168 Mar 1 2019 mkdir + -rwxr-xr-x 1 root root 43040 Mar 1 2019 mknod + -rwxr-xr-x 1 root root 26552 Mar 1 2019 mktemp + -rwxr-xr-x 1 root root 26024 Jan 10 2019 more + -rwsr-xr-x 1 root root 34268 Jan 10 2019 mount + -rwxr-xr-x 1 root root 9688 Jan 10 2019 mountpoint + -rwxr-xr-x 1 root root 84284 Mar 1 2019 mv + lrwxrwxrwx 1 root root 8 Sep 27 2018 nisdomainname -> hostname + lrwxrwxrwx 1 root root 14 Feb 15 2019 pidof -> /sbin/killall5 + -rwxr-xr-x 1 root root 22416 Mar 1 2019 pwd + lrwxrwxrwx 1 root root 4 Apr 18 2019 rbash -> bash + -rwxr-xr-x 1 root root 26504 Mar 1 2019 readlink + -rwxr-xr-x 1 root root 42968 Mar 1 2019 rm + -rwxr-xr-x 1 root root 26496 Mar 1 2019 rmdir + -rwxr-xr-x 1 root root 14136 Jan 22 2019 run-parts + -rwxr-xr-x 1 root root 76012 Dec 23 2018 sed + lrwxrwxrwx 1 root root 4 Aug 13 16:17 sh -> bash + lrwxrwxrwx 1 root root 4 Aug 12 22:27 sh.distrib -> dash + -rwxr-xr-x 1 root root 22384 Mar 1 2019 sleep + -rwxr-xr-x 1 root root 51124 Mar 1 2019 stty + -rwsr-xr-x 1 root root 42472 Jan 10 2019 su + -rwxr-xr-x 1 root root 22392 Mar 1 2019 sync + -rwxr-xr-x 1 root root 283324 Apr 24 2019 tar + -rwxr-xr-x 1 root root 9808 Jan 22 2019 tempfile + -rwxr-xr-x 1 root root 63464 Mar 1 2019 touch + -rwxr-xr-x 1 root root 18260 Mar 1 2019 true + -rwxr-xr-x 1 root root 9636 Apr 23 09:38 ulockmgr_server + -rwsr-xr-x 1 root root 21976 Jan 10 2019 umount + -rwxr-xr-x 1 root root 22380 Mar 1 2019 uname + -rwxr-xr-x 2 root root 2345 Jan 6 2019 uncompress + -rwxr-xr-x 1 root root 88444 Mar 1 2019 vdir + -rwxr-xr-x 1 root root 21980 Jan 10 2019 wdctl + -rwxr-xr-x 1 root root 946 Jan 22 2019 which + lrwxrwxrwx 1 root root 8 Sep 27 2018 ypdomainname -> hostname + -rwxr-xr-x 1 root root 1983 Jan 6 2019 zcat + -rwxr-xr-x 1 root root 1677 Jan 6 2019 zcmp + -rwxr-xr-x 1 root root 5879 Jan 6 2019 zdiff + -rwxr-xr-x 1 root root 29 Jan 6 2019 zegrep + -rwxr-xr-x 1 root root 29 Jan 6 2019 zfgrep + -rwxr-xr-x 1 root root 2080 Jan 6 2019 zforce + -rwxr-xr-x 1 root root 7584 Jan 6 2019 zgrep + -rwxr-xr-x 1 root root 2205 Jan 6 2019 zless + -rwxr-xr-x 1 root root 1841 Jan 6 2019 zmore + -rwxr-xr-x 1 root root 4552 Jan 6 2019 znew +I: user script /srv/workspace/pbuilder/15030/tmp/hooks/D02_print_environment finished -> Attempting to satisfy build-dependencies -> Creating pbuilder-satisfydepends-dummy package Package: pbuilder-satisfydepends-dummy @@ -597,7 +631,7 @@ Get: 373 http://deb.debian.org/debian buster/main armhf ocaml-interp armhf 4.05.0-11 [3581 kB] Get: 374 http://deb.debian.org/debian buster/main armhf ocaml-nox armhf 4.05.0-11 [26.1 MB] Get: 375 http://deb.debian.org/debian buster/main armhf ocaml-compiler-libs armhf 4.05.0-11 [19.2 MB] -Fetched 386 MB in 41s (9381 kB/s) +Fetched 386 MB in 1min 18s (4969 kB/s) debconf: delaying package configuration, since apt-utils is not installed Selecting previously unselected package libbsd0:armhf. (Reading database ... (Reading database ... 5% (Reading database ... 10% (Reading database ... 15% (Reading database ... 20% (Reading database ... 25% (Reading database ... 30% (Reading database ... 35% (Reading database ... 40% (Reading database ... 45% (Reading database ... 50% (Reading database ... 55% (Reading database ... 60% (Reading database ... 65% (Reading database ... 70% (Reading database ... 75% (Reading database ... 80% (Reading database ... 85% (Reading database ... 90% (Reading database ... 95% (Reading database ... 100% (Reading database ... 18932 files and directories currently installed.) @@ -1992,134 +2026,134 @@ update-alternatives: using /usr/lib/jvm/java-11-openjdk-armhf/bin/jconsole to provide /usr/bin/jconsole (jconsole) in auto mode Setting up ca-certificates-java (20190405) ... head: cannot open '/etc/ssl/certs/java/cacerts' for reading: No such file or directory +Adding debian:Buypass_Class_2_Root_CA.pem +Adding debian:GlobalSign_Root_CA_-_R6.pem +Adding debian:SwissSign_Silver_CA_-_G2.pem +Adding debian:TWCA_Global_Root_CA.pem +Adding debian:VeriSign_Universal_Root_Certification_Authority.pem +Adding debian:VeriSign_Class_3_Public_Primary_Certification_Authority_-_G5.pem +Adding debian:GeoTrust_Universal_CA.pem +Adding debian:Staat_der_Nederlanden_Root_CA_-_G3.pem +Adding debian:DigiCert_Assured_ID_Root_G2.pem +Adding debian:TrustCor_RootCert_CA-1.pem +Adding debian:NetLock_Arany_=Class_Gold=_FÅ‘tanúsítvány.pem +Adding debian:Network_Solutions_Certificate_Authority.pem +Adding debian:ePKI_Root_Certification_Authority.pem +Adding debian:Baltimore_CyberTrust_Root.pem +Adding debian:Go_Daddy_Class_2_CA.pem +Adding debian:SSL.com_Root_Certification_Authority_RSA.pem +Adding debian:Actalis_Authentication_Root_CA.pem +Adding debian:Microsec_e-Szigno_Root_CA_2009.pem +Adding debian:AffirmTrust_Networking.pem Adding debian:Deutsche_Telekom_Root_CA_2.pem -Adding debian:QuoVadis_Root_CA_2_G3.pem +Adding debian:T-TeleSec_GlobalRoot_Class_3.pem +Adding debian:CFCA_EV_ROOT.pem +Adding debian:D-TRUST_Root_Class_3_CA_2_EV_2009.pem +Adding debian:GeoTrust_Primary_Certification_Authority_-_G2.pem +Adding debian:Comodo_AAA_Services_root.pem +Adding debian:AffirmTrust_Commercial.pem +Adding debian:Hellenic_Academic_and_Research_Institutions_RootCA_2015.pem +Adding debian:Starfield_Services_Root_Certificate_Authority_-_G2.pem +Adding debian:Security_Communication_RootCA2.pem +Adding debian:USERTrust_ECC_Certification_Authority.pem +Adding debian:certSIGN_ROOT_CA.pem +Adding debian:DigiCert_Assured_ID_Root_G3.pem +Adding debian:GlobalSign_Root_CA_-_R2.pem Adding debian:QuoVadis_Root_CA_3.pem Adding debian:ACCVRAIZ1.pem -Adding debian:Baltimore_CyberTrust_Root.pem -Adding debian:GlobalSign_ECC_Root_CA_-_R4.pem -Adding debian:Entrust_Root_Certification_Authority.pem -Adding debian:Security_Communication_RootCA2.pem +Adding debian:TWCA_Root_Certification_Authority.pem +Adding debian:AC_RAIZ_FNMT-RCM.pem +Adding debian:TrustCor_ECA-1.pem +Adding debian:AffirmTrust_Premium_ECC.pem +Adding debian:GDCA_TrustAUTH_R5_ROOT.pem +Adding debian:CA_Disig_Root_R2.pem Adding debian:TUBITAK_Kamu_SM_SSL_Kok_Sertifikasi_-_Surum_1.pem -Adding debian:COMODO_ECC_Certification_Authority.pem -Adding debian:COMODO_Certification_Authority.pem -Adding debian:Amazon_Root_CA_2.pem -Adding debian:SSL.com_EV_Root_Certification_Authority_RSA_R2.pem -Adding debian:Sonera_Class_2_Root_CA.pem -Adding debian:Certplus_Class_2_Primary_CA.pem -Adding debian:IdenTrust_Public_Sector_Root_CA_1.pem +Adding debian:ISRG_Root_X1.pem +Adding debian:Trustis_FPS_Root_CA.pem +Adding debian:GeoTrust_Primary_Certification_Authority.pem Adding debian:SSL.com_Root_Certification_Authority_ECC.pem -Adding debian:VeriSign_Universal_Root_Certification_Authority.pem -Adding debian:Staat_der_Nederlanden_Root_CA_-_G2.pem -Adding debian:NetLock_Arany_=Class_Gold=_FÅ‘tanúsítvány.pem -Adding debian:QuoVadis_Root_CA_2.pem -Adding debian:Hellenic_Academic_and_Research_Institutions_ECC_RootCA_2015.pem -Adding debian:T-TeleSec_GlobalRoot_Class_2.pem -Adding debian:DigiCert_Assured_ID_Root_CA.pem -Adding debian:Hongkong_Post_Root_CA_1.pem -Adding debian:USERTrust_ECC_Certification_Authority.pem -Adding debian:AC_RAIZ_FNMT-RCM.pem +Adding debian:Certinomis_-_Root_CA.pem +Adding debian:SSL.com_EV_Root_Certification_Authority_ECC.pem +Adding debian:OISTE_WISeKey_Global_Root_GB_CA.pem +Adding debian:QuoVadis_Root_CA_3_G3.pem +Adding debian:TeliaSonera_Root_CA_v1.pem +Adding debian:Hellenic_Academic_and_Research_Institutions_RootCA_2011.pem +Adding debian:Starfield_Root_Certificate_Authority_-_G2.pem +Adding debian:Autoridad_de_Certificacion_Firmaprofesional_CIF_A62634068.pem +Adding debian:Security_Communication_Root_CA.pem +Adding debian:DST_Root_CA_X3.pem Adding debian:QuoVadis_Root_CA_1_G3.pem -Adding debian:AffirmTrust_Premium.pem -Adding debian:Secure_Global_CA.pem -Adding debian:IdenTrust_Commercial_Root_CA_1.pem -Adding debian:DigiCert_Global_Root_G2.pem -Adding debian:OISTE_WISeKey_Global_Root_GA_CA.pem -Adding debian:GeoTrust_Universal_CA_2.pem +Adding debian:Go_Daddy_Root_Certificate_Authority_-_G2.pem +Adding debian:QuoVadis_Root_CA_2_G3.pem +Adding debian:GeoTrust_Primary_Certification_Authority_-_G3.pem +Adding debian:Amazon_Root_CA_2.pem Adding debian:Verisign_Class_3_Public_Primary_Certification_Authority_-_G3.pem -Adding debian:DigiCert_Global_Root_CA.pem -Adding debian:DigiCert_High_Assurance_EV_Root_CA.pem -Adding debian:OISTE_WISeKey_Global_Root_GB_CA.pem -Adding debian:LuxTrust_Global_Root_2.pem -Adding debian:GlobalSign_Root_CA_-_R6.pem -Adding debian:thawte_Primary_Root_CA_-_G2.pem -Adding debian:Certum_Trusted_Network_CA_2.pem -Adding debian:GlobalSign_Root_CA.pem -Adding debian:E-Tugra_Certification_Authority.pem -Adding debian:Entrust_Root_Certification_Authority_-_EC1.pem +Adding debian:SecureSign_RootCA11.pem Adding debian:Atos_TrustedRoot_2011.pem -Adding debian:QuoVadis_Root_CA.pem -Adding debian:SSL.com_EV_Root_Certification_Authority_ECC.pem -Adding debian:D-TRUST_Root_Class_3_CA_2_EV_2009.pem -Adding debian:DigiCert_Assured_ID_Root_G3.pem -Adding debian:Izenpe.com.pem -Adding debian:TeliaSonera_Root_CA_v1.pem -Adding debian:Amazon_Root_CA_4.pem -Adding debian:AffirmTrust_Commercial.pem -Adding debian:AffirmTrust_Networking.pem -Adding debian:Microsec_e-Szigno_Root_CA_2009.pem Adding debian:XRamp_Global_CA_Root.pem -Adding debian:SSL.com_Root_Certification_Authority_RSA.pem -Adding debian:GDCA_TrustAUTH_R5_ROOT.pem -Adding debian:GeoTrust_Primary_Certification_Authority_-_G2.pem -Adding debian:TWCA_Global_Root_CA.pem -Adding debian:Hellenic_Academic_and_Research_Institutions_RootCA_2015.pem -Adding debian:Cybertrust_Global_Root.pem -Adding debian:COMODO_RSA_Certification_Authority.pem -Adding debian:EC-ACC.pem -Adding debian:CFCA_EV_ROOT.pem -Adding debian:Certinomis_-_Root_CA.pem -Adding debian:DigiCert_Global_Root_G3.pem -Adding debian:VeriSign_Class_3_Public_Primary_Certification_Authority_-_G4.pem +Adding debian:Global_Chambersign_Root_-_2008.pem Adding debian:Buypass_Class_3_Root_CA.pem -Adding debian:TrustCor_ECA-1.pem +Adding debian:D-TRUST_Root_Class_3_CA_2_2009.pem +Adding debian:TrustCor_RootCert_CA-2.pem +Adding debian:DigiCert_Assured_ID_Root_CA.pem +Adding debian:EE_Certification_Centre_Root_CA.pem +Adding debian:LuxTrust_Global_Root_2.pem +Adding debian:SSL.com_EV_Root_Certification_Authority_RSA_R2.pem Adding debian:SwissSign_Gold_CA_-_G2.pem -Adding debian:SwissSign_Silver_CA_-_G2.pem -Adding debian:Global_Chambersign_Root_-_2008.pem +Adding debian:Staat_der_Nederlanden_Root_CA_-_G2.pem +Adding debian:Amazon_Root_CA_1.pem +Adding debian:thawte_Primary_Root_CA_-_G2.pem +Adding debian:GlobalSign_ECC_Root_CA_-_R5.pem +Adding debian:DigiCert_Global_Root_G3.pem +Adding debian:EC-ACC.pem +Adding debian:Cybertrust_Global_Root.pem +Adding debian:Hongkong_Post_Root_CA_1.pem +Adding debian:IdenTrust_Public_Sector_Root_CA_1.pem +Adding debian:QuoVadis_Root_CA.pem +Adding debian:GeoTrust_Global_CA.pem Adding debian:Amazon_Root_CA_3.pem -Adding debian:ePKI_Root_Certification_Authority.pem -Adding debian:GeoTrust_Primary_Certification_Authority.pem -Adding debian:T-TeleSec_GlobalRoot_Class_3.pem -Adding debian:Staat_der_Nederlanden_EV_Root_CA.pem -Adding debian:DST_Root_CA_X3.pem +Adding debian:GlobalSign_Root_CA_-_R3.pem +Adding debian:Certum_Trusted_Network_CA.pem +Adding debian:SZAFIR_ROOT_CA2.pem +Adding debian:Certum_Trusted_Network_CA_2.pem +Adding debian:DigiCert_Trusted_Root_G4.pem +Adding debian:Sonera_Class_2_Root_CA.pem Adding debian:thawte_Primary_Root_CA.pem +Adding debian:AffirmTrust_Premium.pem +Adding debian:thawte_Primary_Root_CA_-_G3.pem +Adding debian:IdenTrust_Commercial_Root_CA_1.pem +Adding debian:GeoTrust_Universal_CA_2.pem +Adding debian:Certplus_Class_2_Primary_CA.pem +Adding debian:Staat_der_Nederlanden_EV_Root_CA.pem +Adding debian:QuoVadis_Root_CA_2.pem +Adding debian:Secure_Global_CA.pem Adding debian:Entrust_Root_Certification_Authority_-_G2.pem -Adding debian:GeoTrust_Universal_CA.pem -Adding debian:Certigna.pem -Adding debian:Starfield_Root_Certificate_Authority_-_G2.pem +Adding debian:Entrust_Root_Certification_Authority_-_EC1.pem +Adding debian:USERTrust_RSA_Certification_Authority.pem +Adding debian:Entrust_Root_Certification_Authority.pem +Adding debian:DigiCert_Global_Root_G2.pem +Adding debian:COMODO_ECC_Certification_Authority.pem +Adding debian:AddTrust_External_Root.pem +Adding debian:GlobalSign_ECC_Root_CA_-_R4.pem Adding debian:OISTE_WISeKey_Global_Root_GC_CA.pem -Adding debian:CA_Disig_Root_R2.pem +Adding debian:E-Tugra_Certification_Authority.pem +Adding debian:DigiCert_High_Assurance_EV_Root_CA.pem +Adding debian:Chambers_of_Commerce_Root_-_2008.pem +Adding debian:GlobalSign_Root_CA.pem +Adding debian:COMODO_RSA_Certification_Authority.pem Adding debian:Taiwan_GRCA.pem -Adding debian:Starfield_Class_2_CA.pem -Adding debian:GeoTrust_Global_CA.pem -Adding debian:Go_Daddy_Root_Certificate_Authority_-_G2.pem -Adding debian:Buypass_Class_2_Root_CA.pem -Adding debian:GeoTrust_Primary_Certification_Authority_-_G3.pem -Adding debian:SecureTrust_CA.pem -Adding debian:Trustis_FPS_Root_CA.pem -Adding debian:Hellenic_Academic_and_Research_Institutions_RootCA_2011.pem -Adding debian:certSIGN_ROOT_CA.pem -Adding debian:DigiCert_Trusted_Root_G4.pem -Adding debian:Network_Solutions_Certificate_Authority.pem -Adding debian:Staat_der_Nederlanden_Root_CA_-_G3.pem -Adding debian:D-TRUST_Root_Class_3_CA_2_2009.pem +Adding debian:Amazon_Root_CA_4.pem +Adding debian:VeriSign_Class_3_Public_Primary_Certification_Authority_-_G4.pem +Adding debian:OISTE_WISeKey_Global_Root_GA_CA.pem +Adding debian:T-TeleSec_GlobalRoot_Class_2.pem Adding debian:Entrust.net_Premium_2048_Secure_Server_CA.pem -Adding debian:DigiCert_Assured_ID_Root_G2.pem -Adding debian:VeriSign_Class_3_Public_Primary_Certification_Authority_-_G5.pem -Adding debian:GlobalSign_ECC_Root_CA_-_R5.pem -Adding debian:Starfield_Services_Root_Certificate_Authority_-_G2.pem -Adding debian:Actalis_Authentication_Root_CA.pem -Adding debian:Security_Communication_Root_CA.pem -Adding debian:QuoVadis_Root_CA_3_G3.pem -Adding debian:Amazon_Root_CA_1.pem -Adding debian:EE_Certification_Centre_Root_CA.pem -Adding debian:Chambers_of_Commerce_Root_-_2008.pem -Adding debian:thawte_Primary_Root_CA_-_G3.pem -Adding debian:Comodo_AAA_Services_root.pem -Adding debian:AddTrust_External_Root.pem -Adding debian:TrustCor_RootCert_CA-2.pem -Adding debian:Autoridad_de_Certificacion_Firmaprofesional_CIF_A62634068.pem -Adding debian:USERTrust_RSA_Certification_Authority.pem -Adding debian:GlobalSign_Root_CA_-_R2.pem -Adding debian:TrustCor_RootCert_CA-1.pem -Adding debian:Certum_Trusted_Network_CA.pem -Adding debian:ISRG_Root_X1.pem -Adding debian:GlobalSign_Root_CA_-_R3.pem -Adding debian:AffirmTrust_Premium_ECC.pem -Adding debian:SZAFIR_ROOT_CA2.pem -Adding debian:TWCA_Root_Certification_Authority.pem -Adding debian:SecureSign_RootCA11.pem -Adding debian:Go_Daddy_Class_2_CA.pem +Adding debian:SecureTrust_CA.pem +Adding debian:Certigna.pem +Adding debian:Starfield_Class_2_CA.pem +Adding debian:Hellenic_Academic_and_Research_Institutions_ECC_RootCA_2015.pem +Adding debian:Izenpe.com.pem +Adding debian:COMODO_Certification_Authority.pem +Adding debian:DigiCert_Global_Root_CA.pem done. Setting up libxml-parser-perl (2.44-4) ... Setting up libmono-system4.0-cil (5.18.0.240+dfsg-3) ... @@ -2313,7 +2347,7 @@ fakeroot is already the newest version (1.23-1). 0 upgraded, 0 newly installed, 0 to remove and 0 not upgraded. I: Building the package -I: Running cd /build/z3-4.4.1/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games" HOME="/nonexistent/first-build" dpkg-buildpackage -us -uc -b +I: Running cd /build/z3-4.4.1/ && env PATH="/usr/sbin:/usr/bin:/sbin:/bin:/usr/games:/i/capture/the/path" HOME="/nonexistent/second-build" dpkg-buildpackage -us -uc -b dpkg-buildpackage: info: source package z3 dpkg-buildpackage: info: source version 4.4.1-1~deb10u1 dpkg-buildpackage: info: source distribution buster @@ -2518,36 +2552,36 @@ New component: 'py_example' Generated 'src/util/version.h' Updated 'src/api/dotnet/Properties/AssemblyInfo' -Generated 'src/math/polynomial/algebraic_params.hpp' -Generated 'src/math/realclosure/rcf_params.hpp' -Generated 'src/tactic/sls/sls_params.hpp' -Generated 'src/solver/combined_solver_params.hpp' -Generated 'src/model/model_params.hpp' -Generated 'src/model/model_evaluator_params.hpp' Generated 'src/nlsat/nlsat_params.hpp' +Generated 'src/muz/base/fixedpoint_params.hpp' +Generated 'src/interp/interp_params.hpp' +Generated 'src/opt/opt_params.hpp' +Generated 'src/tactic/sls/sls_params.hpp' Generated 'src/ast/pp_params.hpp' -Generated 'src/ast/rewriter/poly_rewriter_params.hpp' -Generated 'src/ast/rewriter/array_rewriter_params.hpp' -Generated 'src/ast/rewriter/bool_rewriter_params.hpp' -Generated 'src/ast/rewriter/rewriter_params.hpp' +Generated 'src/ast/fpa/fpa2bv_rewriter_params.hpp' +Generated 'src/ast/pattern/pattern_inference_params_helper.hpp' Generated 'src/ast/rewriter/fpa_rewriter_params.hpp' -Generated 'src/ast/rewriter/bv_rewriter_params.hpp' +Generated 'src/ast/rewriter/poly_rewriter_params.hpp' Generated 'src/ast/rewriter/arith_rewriter_params.hpp' -Generated 'src/ast/pattern/pattern_inference_params_helper.hpp' -Generated 'src/ast/fpa/fpa2bv_rewriter_params.hpp' -Generated 'src/ast/normal_forms/nnf_params.hpp' +Generated 'src/ast/rewriter/bv_rewriter_params.hpp' +Generated 'src/ast/rewriter/rewriter_params.hpp' +Generated 'src/ast/rewriter/bool_rewriter_params.hpp' +Generated 'src/ast/rewriter/array_rewriter_params.hpp' +Generated 'src/ast/simplifier/array_simplifier_params_helper.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/parsers/util/parser_params.hpp' -Generated 'src/opt/opt_params.hpp' -Generated 'src/sat/sat_simplifier_params.hpp' +Generated 'src/ast/normal_forms/nnf_params.hpp' Generated 'src/sat/sat_scc_params.hpp' -Generated 'src/sat/sat_asymm_branch_params.hpp' Generated 'src/sat/sat_params.hpp' -Generated 'src/muz/base/fixedpoint_params.hpp' +Generated 'src/sat/sat_asymm_branch_params.hpp' +Generated 'src/sat/sat_simplifier_params.hpp' +Generated 'src/math/realclosure/rcf_params.hpp' +Generated 'src/math/polynomial/algebraic_params.hpp' +Generated 'src/model/model_evaluator_params.hpp' +Generated 'src/model/model_params.hpp' +Generated 'src/parsers/util/parser_params.hpp' +Generated 'src/solver/combined_solver_params.hpp' Generated 'src/smt/params/smt_params_helper.hpp' -Generated 'src/interp/interp_params.hpp' Generated 'src/ast/pattern/database.h' Generated 'src/shell/install_tactic.cpp' Generated 'src/test/install_tactic.cpp' @@ -2583,26 +2617,26 @@ Compiling src/api/python/z3test.py ... Compiling src/api/python/z3types.py ... Compiling src/api/python/z3util.py ... -Copied 'z3num.py' -Copied 'z3types.py' -Copied 'z3test.py' -Copied 'z3.py' +Copied 'z3consts.py' +Copied 'z3util.py' Copied 'z3rcf.py' -Copied 'z3printer.py' +Copied 'z3test.py' Copied 'z3poly.py' +Copied 'z3printer.py' +Copied 'z3types.py' +Copied 'z3num.py' +Copied 'z3.py' Copied 'z3core.py' -Copied 'z3util.py' -Copied 'z3consts.py' +Generated 'z3poly.pyc' +Generated 'z3rcf.pyc' Generated 'z3test.pyc' -Generated 'z3num.pyc' -Generated 'z3core.pyc' Generated 'z3types.pyc' -Generated 'z3rcf.pyc' +Generated 'z3consts.pyc' Generated 'z3.pyc' -Generated 'z3poly.pyc' +Generated 'z3core.pyc' Generated 'z3printer.pyc' +Generated 'z3num.pyc' Generated 'z3util.pyc' -Generated 'z3consts.pyc' Testing ocamlc... Finding OCAML_LIB... OCAML_LIB=/usr/lib/ocaml @@ -2645,16 +2679,16 @@ make[1]: Leaving directory '/build/z3-4.4.1' jh_linkjars -O--parallel dh_auto_build -O--parallel - make -j3 + make -j4 make[1]: Entering directory '/build/z3-4.4.1' make -C build all make[2]: Entering directory '/build/z3-4.4.1/build' src/smt/smt_statistics.cpp src/interp/iz3profiling.cpp -src/util/luby.cpp src/util/common_msgs.cpp -src/util/approx_nat.cpp src/util/scoped_ctrl_c.cpp +src/util/luby.cpp +src/util/approx_nat.cpp src/api/dll/dll.cpp cp ../src/api/ml/z3enums.mli api/ml/z3enums.mli cp ../src/api/ml/z3native.mli api/ml/z3native.mli @@ -2663,462 +2697,431 @@ cp ../src/api/ml/z3native.ml api/ml/z3native.ml cp ../src/api/ml/z3.ml api/ml/z3.ml cp ../src/api/ml/z3native_stubs.c api/ml/z3native_stubs.c -src/util/approx_set.cpp src/util/cooperate.cpp src/util/timeit.cpp -src/util/memory_manager.cpp +src/util/approx_set.cpp src/util/z3_exception.cpp +src/util/memory_manager.cpp src/util/page.cpp ocamlc -I api/ml -c api/ml/z3enums.mli -src/api/api_log.cpp src/api/api_commands.cpp -src/util/timer.cpp -src/util/scoped_timer.cpp -src/util/timeout.cpp +src/api/api_log.cpp +src/util/lbool.cpp +src/util/stack.cpp src/util/bit_util.cpp +src/util/timer.cpp src/util/util.cpp +src/util/timeout.cpp +src/util/scoped_timer.cpp ocamlc -I api/ml -c api/ml/z3native.mli ocamlc -a -o api/ml/z3enums.ml -o api/ml/z3enums.cma src/shell/z3_log_frontend.cpp -src/util/hash.cpp -src/util/stack.cpp src/util/mpn.cpp -src/util/lbool.cpp src/util/fixed_bit_vector.cpp +src/util/hash.cpp ocamlc -I api/ml -c api/ml/z3.mli ocamlc -a -o api/ml/z3native.ml -o api/ml/z3native.cma src/api/z3_replayer.cpp -src/util/trace.cpp -src/util/rlimit.cpp -src/util/region.cpp src/util/warning.cpp -src/util/cmd_context_types.cpp +src/util/symbol.cpp src/util/prime_generator.cpp -src/util/small_object_allocator.cpp +src/util/smt2_util.cpp +src/util/rlimit.cpp +src/util/bit_vector.cpp +src/util/region.cpp src/util/debug.cpp src/util/permutation.cpp src/util/statistics.cpp -src/util/smt2_util.cpp -src/util/bit_vector.cpp -src/util/symbol.cpp +src/util/small_object_allocator.cpp +src/util/trace.cpp ocamlc -a -o api/ml/z3.ml -o api/ml/z3.cma src/api/api_log_macros.cpp src/interp/iz3scopes.cpp -src/sat/sat_watched.cpp +src/sat/sat_clause_set.cpp src/sat/sat_clause.cpp +src/sat/sat_watched.cpp src/sat/sat_model_converter.cpp src/sat/sat_clause_use_list.cpp -src/sat/sat_clause_set.cpp src/util/mpz.cpp -src/smt/params/qi_params.cpp -src/smt/params/dyn_ack_params.cpp -src/smt/params/theory_arith_params.cpp -src/smt/params/theory_pb_params.cpp -src/smt/params/theory_bv_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/util/cmd_context_types.cpp src/math/euclid/euclidean_solver.cpp src/math/realclosure/mpz_matrix.cpp src/math/interval/interval_mpq.cpp -src/sat/sat_config.cpp -src/util/gparams.cpp -src/util/mpff.cpp -src/util/mpf.cpp +src/util/hwf.cpp src/util/mpfx.cpp +src/util/mpff.cpp src/util/mpq.cpp src/util/mpq_inf.cpp -src/util/env_params.cpp -src/util/hwf.cpp +src/util/mpf.cpp src/shell/mem_initializer.cpp src/smt/old_interval.cpp -src/smt/params/theory_array_params.cpp +src/smt/params/theory_pb_params.cpp src/smt/params/preprocessor_params.cpp -src/tactic/arith/linear_equation.cpp +src/smt/params/theory_bv_params.cpp +src/smt/params/qi_params.cpp +src/smt/params/dyn_ack_params.cpp +src/smt/params/theory_array_params.cpp +src/smt/params/theory_arith_params.cpp +src/ast/pattern/pattern_inference_params.cpp +src/ast/simplifier/arith_simplifier_params.cpp +src/ast/simplifier/array_simplifier_params.cpp +src/ast/simplifier/bv_simplifier_params.cpp src/math/realclosure/realclosure.cpp -src/util/params.cpp +src/sat/sat_scc.cpp +src/sat/sat_sls.cpp +src/sat/sat_solver.cpp +src/sat/sat_cleaner.cpp +src/sat/dimacs.cpp +src/sat/sat_iff3_finder.cpp +src/sat/sat_integrity_checker.cpp +src/sat/sat_mus.cpp +src/sat/sat_config.cpp +src/sat/sat_asymm_branch.cpp +src/sat/sat_bceq.cpp +src/sat/sat_simplifier.cpp +src/sat/sat_elim_eqs.cpp +src/sat/sat_probing.cpp +src/util/env_params.cpp src/util/s_integer.cpp -src/util/inf_int_rational.cpp +src/util/params.cpp src/util/inf_rational.cpp +src/util/inf_int_rational.cpp +src/util/gparams.cpp src/util/rational.cpp +src/util/sexpr.cpp src/util/mpbq.cpp src/api/dll/mem_initializer.cpp -src/opt/hitting_sets.cpp +src/shell/dimacs_frontend.cpp src/muz/rel/tbv.cpp -src/muz/base/bind_variables.cpp src/smt/user_plugin/user_decl_plugin.cpp src/smt/smt_quantifier_stat.cpp -src/smt/uses_theory.cpp src/smt/proto_model/value_factory.cpp -src/smt/params/smt_params.cpp src/ast/simplifier/simplifier_plugin.cpp +src/tactic/arith/linear_equation.cpp src/tactic/arith/bound_propagator.cpp -src/parsers/util/simple_parser.cpp src/parsers/util/scanner.cpp -src/ast/occurs.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/parsers/util/simple_parser.cpp src/ast/num_occurs.cpp -src/ast/pb_decl_plugin.cpp -src/ast/act_cache.cpp +src/ast/has_free_vars.cpp src/ast/for_each_ast.cpp -src/ast/expr_substitution.cpp -src/ast/ast_lt.cpp -src/ast/expr_stat.cpp -src/ast/expr_abstract.cpp src/ast/decl_collector.cpp -src/ast/used_vars.cpp -src/ast/has_free_vars.cpp -src/ast/func_decl_dependencies.cpp -src/ast/for_each_expr.cpp +src/ast/expr_abstract.cpp +src/ast/expr_substitution.cpp src/ast/ast_util.cpp -src/ast/expr_map.cpp +src/ast/ast_lt.cpp src/math/subpaving/subpaving.cpp -src/math/subpaving/subpaving_hwf.cpp src/math/subpaving/subpaving_mpfx.cpp -src/math/subpaving/subpaving_mpff.cpp src/math/subpaving/subpaving_mpq.cpp +src/math/subpaving/subpaving_mpff.cpp +src/math/subpaving/subpaving_hwf.cpp src/math/subpaving/subpaving_mpf.cpp src/math/simplex/simplex.cpp src/math/hilbert/hilbert_basis.cpp -src/sat/sat_iff3_finder.cpp -src/sat/sat_elim_eqs.cpp -src/sat/sat_simplifier.cpp -src/sat/sat_cleaner.cpp -src/sat/sat_mus.cpp -src/sat/sat_sls.cpp -src/sat/sat_bceq.cpp -src/sat/sat_asymm_branch.cpp -src/sat/sat_integrity_checker.cpp -src/sat/sat_solver.cpp -src/sat/sat_scc.cpp -src/sat/dimacs.cpp -src/sat/sat_probing.cpp -src/util/sexpr.cpp src/util/inf_s_integer.cpp -src/api/dll/gparams_register_modules.cpp -src/shell/dimacs_frontend.cpp -src/shell/gparams_register_modules.cpp -src/qe/qe_util.cpp -src/smt/smt_value_sort.cpp +src/opt/hitting_sets.cpp +src/muz/base/bind_variables.cpp +src/smt/smt_almost_cg_table.cpp +src/smt/uses_theory.cpp src/smt/cost_evaluator.cpp -src/ast/simplifier/basic_simplifier_plugin.cpp +src/smt/smt_value_sort.cpp +src/smt/fingerprints.cpp +src/smt/params/smt_params.cpp src/ast/simplifier/datatype_simplifier_plugin.cpp -src/cmd_context/tactic_manager.cpp src/cmd_context/pdecl.cpp src/math/subpaving/tactic/expr2subpaving.cpp src/parsers/util/cost_parser.cpp -src/ast/rewriter/fpa_rewriter.cpp -src/ast/rewriter/expr_safe_replace.cpp src/ast/rewriter/datatype_rewriter.cpp -src/ast/rewriter/mk_simplified_app.cpp -src/ast/expr_functors.cpp -src/ast/seq_decl_plugin.cpp -src/ast/macro_substitution.cpp -src/ast/ast_translation.cpp src/ast/ast_smt_pp.cpp +src/ast/macro_substitution.cpp +src/ast/fpa_decl_plugin.cpp +src/ast/pb_decl_plugin.cpp +src/ast/for_each_expr.cpp +src/ast/expr_map.cpp +src/ast/func_decl_dependencies.cpp src/ast/format.cpp +src/ast/expr_stat.cpp src/ast/reg_decl_plugins.cpp -src/ast/fpa_decl_plugin.cpp +src/ast/seq_decl_plugin.cpp +src/ast/pp.cpp src/ast/ast_ll_pp.cpp +src/ast/ast_translation.cpp +src/ast/used_vars.cpp +src/ast/occurs.cpp +src/ast/act_cache.cpp src/nlsat/nlsat_types.cpp +src/nlsat/nlsat_clause.cpp src/math/polynomial/polynomial_cache.cpp +src/shell/main.cpp src/parsers/smt/smtlib.cpp +src/qe/qe_util.cpp src/smt/user_plugin/user_simplifier_plugin.cpp src/smt/smt_literal.cpp -src/smt/fingerprints.cpp +src/smt/theory_opt.cpp src/smt/arith_eq_solver.cpp src/smt/smt_farkas_util.cpp +src/smt/smt_cg_table.cpp src/smt/proto_model/numeral_factory.cpp src/ast/fpa/fpa2bv_converter.cpp -src/ast/simplifier/poly_simplifier_plugin.cpp src/ast/simplifier/inj_axiom.cpp -src/ast/simplifier/fpa_simplifier_plugin.cpp -src/ast/simplifier/bit2int.cpp -src/ast/simplifier/distribute_forall.cpp +src/ast/simplifier/poly_simplifier_plugin.cpp src/ast/simplifier/arith_simplifier_plugin.cpp +src/ast/simplifier/basic_simplifier_plugin.cpp src/ast/simplifier/bv_simplifier_plugin.cpp -src/ast/proof_checker/proof_checker.cpp +src/ast/simplifier/bit2int.cpp src/cmd_context/check_logic.cpp -src/interp/iz3mgr.cpp -src/tactic/arith/bv2real_rewriter.cpp +src/cmd_context/tactic_manager.cpp src/math/grobner/grobner.cpp src/parsers/util/pattern_validation.cpp +src/tactic/equiv_proof_converter.cpp src/tactic/proof_converter.cpp -src/model/func_interp.cpp -src/ast/normal_forms/defined_names.cpp -src/ast/normal_forms/nnf.cpp +src/tactic/replace_proof_converter.cpp src/ast/normal_forms/name_exprs.cpp -src/ast/normal_forms/pull_quant.cpp +src/ast/rewriter/pb_rewriter.cpp +src/ast/rewriter/mk_simplified_app.cpp +src/ast/rewriter/dl_rewriter.cpp src/ast/rewriter/expr_replacer.cpp -src/ast/rewriter/der.cpp -src/ast/rewriter/rewriter.cpp -src/ast/rewriter/var_subst.cpp -src/ast/rewriter/th_rewriter.cpp +src/ast/rewriter/expr_safe_replace.cpp +src/ast/rewriter/bool_rewriter.cpp src/ast/rewriter/bv_rewriter.cpp -src/ast/rewriter/array_rewriter.cpp -src/ast/rewriter/dl_rewriter.cpp -src/ast/rewriter/pb_rewriter.cpp -src/ast/rewriter/arith_rewriter.cpp +src/ast/rewriter/rewriter.cpp +src/ast/rewriter/fpa_rewriter.cpp src/ast/rewriter/factor_rewriter.cpp -src/ast/rewriter/bool_rewriter.cpp -src/ast/arith_decl_plugin.cpp +src/ast/rewriter/arith_rewriter.cpp +src/ast/rewriter/array_rewriter.cpp +src/ast/ast_smt2_pp.cpp src/ast/shared_occs.cpp src/ast/static_features.cpp -src/ast/ast.cpp -src/ast/ast_pp_util.cpp src/ast/expr2polynomial.cpp -src/ast/pp.cpp -src/ast/dl_decl_plugin.cpp -src/ast/ast_smt2_pp.cpp -src/ast/expr2var.cpp +src/ast/bv_decl_plugin.cpp +src/ast/expr_functors.cpp +src/ast/well_sorted.cpp src/ast/array_decl_plugin.cpp +src/ast/expr2var.cpp +src/ast/arith_decl_plugin.cpp +src/ast/ast.cpp +src/ast/dl_decl_plugin.cpp +src/ast/ast_pp_util.cpp src/ast/datatype_decl_plugin.cpp -src/ast/well_sorted.cpp -src/ast/bv_decl_plugin.cpp src/nlsat/nlsat_interval_set.cpp -src/nlsat/nlsat_clause.cpp -src/math/polynomial/sexpr2upolynomial.cpp -src/math/polynomial/rpolynomial.cpp src/math/polynomial/polynomial.cpp -src/shell/main.cpp +src/math/polynomial/upolynomial.cpp +src/math/polynomial/rpolynomial.cpp +src/math/polynomial/algebraic_numbers.cpp +src/api/dll/gparams_register_modules.cpp +src/shell/gparams_register_modules.cpp src/parsers/smt/smtparser.cpp -src/smt/watch_list.cpp src/smt/smt_clause.cpp -src/smt/smt_almost_cg_table.cpp src/smt/cached_var_subst.cpp -src/smt/theory_opt.cpp -src/smt/smt_cg_table.cpp -src/smt/elim_term_ite.cpp src/ast/rewriter/bit_blaster/bit_blaster_rewriter.cpp src/ast/rewriter/bit_blaster/bit_blaster.cpp -src/ast/simplifier/simplifier.cpp -src/ast/simplifier/array_simplifier_plugin.cpp src/ast/simplifier/push_app_ite.cpp +src/ast/simplifier/simplifier.cpp src/ast/simplifier/elim_bounds.cpp -src/ast/simplifier/pull_ite_tree.cpp +src/ast/simplifier/fpa_simplifier_plugin.cpp +src/ast/simplifier/array_simplifier_plugin.cpp src/ast/simplifier/bv_elim.cpp -src/interp/iz3pp.cpp +src/ast/simplifier/pull_ite_tree.cpp +src/ast/simplifier/distribute_forall.cpp +src/ast/proof_checker/proof_checker.cpp +src/interp/iz3mgr.cpp src/tactic/aig/aig.cpp +src/tactic/arith/bv2real_rewriter.cpp src/tactic/arith/bound_manager.cpp src/sat/tactic/atom2bool_var.cpp -src/ast/substitution/substitution_tree.cpp -src/ast/substitution/unifier.cpp src/ast/substitution/substitution.cpp src/ast/substitution/matcher.cpp +src/ast/substitution/unifier.cpp +src/ast/substitution/substitution_tree.cpp src/tactic/goal_num_occurs.cpp +src/tactic/goal_shared_occs.cpp src/tactic/goal.cpp src/tactic/goal_util.cpp -src/tactic/equiv_proof_converter.cpp -src/tactic/replace_proof_converter.cpp -src/tactic/goal_shared_occs.cpp +src/model/model_pp.cpp +src/model/func_interp.cpp src/model/model_core.cpp src/model/model_v2_pp.cpp -src/model/model_pp.cpp src/model/model_smt2_pp.cpp -src/ast/rewriter/ast_counter.cpp -src/ast/rewriter/quant_hoist.cpp +src/ast/normal_forms/pull_quant.cpp +src/ast/normal_forms/nnf.cpp +src/ast/normal_forms/defined_names.cpp +src/ast/rewriter/var_subst.cpp +src/ast/rewriter/der.cpp +src/ast/rewriter/th_rewriter.cpp src/ast/ast_printer.cpp -src/math/polynomial/algebraic_numbers.cpp -src/math/polynomial/upolynomial.cpp -src/math/polynomial/polynomial_factorization.cpp -src/math/polynomial/upolynomial_factorization.cpp -src/api/api_datatype.cpp +src/nlsat/nlsat_evaluator.cpp +src/nlsat/nlsat_explain.cpp +src/math/polynomial/sexpr2upolynomial.cpp +src/api/api_bv.cpp +src/api/api_array.cpp +src/api/api_stats.cpp src/api/api_numeral.cpp -src/api/api_solver_old.cpp -src/api/api_model.cpp +src/api/api_polynomial.cpp src/api/api_algebraic.cpp src/api/api_fpa.cpp -src/api/api_bv.cpp -src/api/api_array.cpp -src/api/api_params.cpp -src/api/api_pb.cpp +src/api/api_rcf.cpp +src/api/api_datatype.cpp src/api/api_goal.cpp -src/api/api_ast_vector.cpp src/api/api_ast.cpp -src/api/api_ast_map.cpp src/api/api_context.cpp -src/api/api_arith.cpp +src/api/api_ast_vector.cpp +src/api/api_params.cpp src/api/api_quant.cpp +src/api/api_ast_map.cpp +src/api/api_pb.cpp src/tactic/ufbv/ufbv_rewriter.cpp src/muz/pdr/pdr_sym_mux.cpp src/muz/rel/doc.cpp src/muz/base/dl_boogie_proof.cpp -src/qe/qe_bool_plugin.cpp -src/qe/qe_bv_plugin.cpp -src/qe/qe_datatype_plugin.cpp src/qe/qe_array_plugin.cpp src/qe/qe_arith_plugin.cpp -src/qe/qe_dl_plugin.cpp src/qe/nlarith_util.cpp +src/qe/qe_bv_plugin.cpp +src/qe/qe_bool_plugin.cpp +src/qe/qe_dl_plugin.cpp +src/qe/qe_datatype_plugin.cpp src/smt/expr_context_simplifier.cpp -src/smt/proto_model/array_factory.cpp +src/smt/elim_term_ite.cpp +src/smt/watch_list.cpp src/smt/proto_model/datatype_factory.cpp src/smt/proto_model/struct_factory.cpp +src/smt/proto_model/array_factory.cpp src/smt/proto_model/proto_model.cpp src/ast/pattern/pattern_inference.cpp src/ast/macros/macro_util.cpp src/ast/simplifier/maximise_ac_sharing.cpp -src/interp/iz3proof_itp.cpp +src/interp/iz3pp.cpp src/tactic/arith/bv2int_rewriter.cpp src/tactic/arith/probe_arith.cpp src/tactic/probe.cpp -src/model/model_evaluator.cpp src/model/model_implicant.cpp +src/model/model_evaluator.cpp src/model/model.cpp -src/nlsat/nlsat_evaluator.cpp -src/nlsat/nlsat_explain.cpp +src/model/model2expr.cpp +src/ast/rewriter/ast_counter.cpp +src/ast/rewriter/quant_hoist.cpp src/nlsat/nlsat_solver.cpp -src/api/api_stats.cpp -src/api/api_polynomial.cpp -src/api/api_rcf.cpp +src/math/polynomial/upolynomial_factorization.cpp +src/math/polynomial/polynomial_factorization.cpp +src/api/api_model.cpp +src/api/api_arith.cpp +src/api/api_solver_old.cpp src/api/api_user_theory.cpp src/opt/pb_sls.cpp -src/qe/vsubst_tactic.cpp src/qe/qe_arith.cpp src/tactic/bv/bit_blaster_model_converter.cpp -src/ast/macros/quasi_macros.cpp src/ast/macros/macro_manager.cpp -src/interp/iz3proof.cpp +src/ast/macros/quasi_macros.cpp src/interp/iz3foci.cpp src/solver/check_sat_result.cpp -src/tactic/arith/arith_bounds_tactic.cpp -src/sat/tactic/goal2sat.cpp -src/tactic/core/cofactor_elim_term_ite.cpp src/tactic/extension_model_converter.cpp src/tactic/model_converter.cpp -src/tactic/filter_model_converter.cpp -src/tactic/tactic.cpp -src/model/model2expr.cpp -src/api/api_tactic.cpp -src/opt/mss.cpp -src/opt/opt_pareto.cpp src/opt/mus.cpp -src/tactic/ufbv/quasi_macros_tactic.cpp -src/tactic/ufbv/ufbv_rewriter_tactic.cpp -src/tactic/ufbv/macro_finder_tactic.cpp +src/opt/opt_pareto.cpp +src/opt/mss.cpp src/tactic/fpa/fpa2bv_model_converter.cpp -src/tactic/nlsat_smt/nl_purify_tactic.cpp -src/qe/qe_sat_tactic.cpp -src/qe/qe_lite.cpp -src/qe/qe_tactic.cpp -src/smt/tactic/smt_tactic.cpp -src/tactic/bv/bv1_blaster_tactic.cpp -src/tactic/bv/bit_blaster_tactic.cpp -src/tactic/bv/max_bv_sharing_tactic.cpp -src/tactic/bv/bv_size_reduction_tactic.cpp +src/duality/duality_wrapper.cpp +src/duality/duality_profiling.cpp +src/qe/vsubst_tactic.cpp src/smt/smt_implied_equalities.cpp src/smt/smt_solver.cpp src/ast/macros/macro_finder.cpp src/cmd_context/context_params.cpp -src/interp/iz3translate_direct.cpp -src/interp/iz3translate.cpp -src/interp/iz3base.cpp src/interp/iz3checker.cpp -src/interp/iz3interp.cpp -src/solver/tactic2solver.cpp -src/solver/solver_na2as.cpp -src/solver/combined_solver.cpp +src/interp/iz3base.cpp +src/interp/iz3proof_itp.cpp +src/interp/iz3proof.cpp +src/interp/iz3translate.cpp src/solver/solver.cpp -src/tactic/aig/aig_tactic.cpp +src/solver/combined_solver.cpp +src/solver/solver_na2as.cpp +src/solver/tactic2solver.cpp src/nlsat/tactic/goal2nlsat.cpp -src/nlsat/tactic/nlsat_tactic.cpp -src/tactic/arith/fix_dl_var_tactic.cpp -src/tactic/arith/card2bv_tactic.cpp -src/tactic/arith/elim01_tactic.cpp -src/tactic/arith/recover_01_tactic.cpp -src/tactic/arith/eq2bv_tactic.cpp -src/tactic/arith/normalize_bounds_tactic.cpp -src/tactic/arith/nla2bv_tactic.cpp -src/tactic/arith/lia2pb_tactic.cpp -src/tactic/arith/pb2bv_tactic.cpp -src/tactic/arith/add_bounds_tactic.cpp -src/tactic/arith/factor_tactic.cpp src/tactic/arith/pb2bv_model_converter.cpp -src/tactic/arith/diff_neq_tactic.cpp -src/tactic/arith/lia2card_tactic.cpp -src/sat/tactic/sat_tactic.cpp -src/tactic/core/elim_term_ite_tactic.cpp -src/tactic/core/reduce_args_tactic.cpp -src/tactic/core/pb_preprocess_tactic.cpp -src/tactic/core/cofactor_term_ite_tactic.cpp -src/tactic/core/occf_tactic.cpp -src/tactic/core/split_clause_tactic.cpp -src/tactic/core/symmetry_reduce_tactic.cpp -src/tactic/core/propagate_values_tactic.cpp -src/tactic/core/blast_term_ite_tactic.cpp -src/tactic/core/distribute_forall_tactic.cpp -src/tactic/core/solve_eqs_tactic.cpp -src/tactic/core/nnf_tactic.cpp -src/tactic/core/elim_uncnstr_tactic.cpp -src/tactic/core/der_tactic.cpp -src/tactic/tactical.cpp +src/tactic/arith/arith_bounds_tactic.cpp +src/sat/tactic/goal2sat.cpp +src/tactic/core/cofactor_elim_term_ite.cpp src/tactic/horn_subsume_model_converter.cpp -src/api/api_solver.cpp -src/api/api_interp.cpp +src/tactic/tactic.cpp +src/tactic/filter_model_converter.cpp src/api/api_config_params.cpp +src/api/api_interp.cpp +src/api/api_solver.cpp src/parsers/smt/smtlib_solver.cpp src/tactic/portfolio/smt_strategic_solver.cpp -src/tactic/portfolio/default_tactic.cpp -src/sat/sat_solver/inc_sat_solver.cpp -src/tactic/ufbv/ufbv_tactic.cpp -src/tactic/fpa/qffp_tactic.cpp -src/tactic/fpa/fpa2bv_tactic.cpp -src/tactic/smtlogics/qfbv_tactic.cpp -src/tactic/smtlogics/qfauflia_tactic.cpp -src/tactic/smtlogics/nra_tactic.cpp -src/tactic/smtlogics/qfnia_tactic.cpp -src/tactic/smtlogics/qflia_tactic.cpp -src/tactic/smtlogics/qfaufbv_tactic.cpp -src/tactic/smtlogics/qfufbv_tactic.cpp -src/tactic/smtlogics/qfnra_tactic.cpp -src/tactic/smtlogics/qfuf_tactic.cpp -src/tactic/smtlogics/qfidl_tactic.cpp -src/tactic/smtlogics/qfufnra_tactic.cpp -src/tactic/smtlogics/quant_tactics.cpp -src/tactic/smtlogics/qflra_tactic.cpp +src/tactic/ufbv/macro_finder_tactic.cpp +src/tactic/ufbv/ufbv_rewriter_tactic.cpp +src/tactic/ufbv/quasi_macros_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_wrapper.cpp -src/duality/duality_profiling.cpp -src/duality/duality_solver.cpp +src/muz/base/proof_utils.cpp src/duality/duality_rpfp.cpp +src/duality/duality_solver.cpp src/qe/qe_cmd.cpp -src/tactic/sls/sls_tactic.cpp +src/qe/qe_lite.cpp +src/qe/qe_tactic.cpp +src/qe/qe_sat_tactic.cpp src/tactic/sls/sls_engine.cpp -src/smt/tactic/ctx_solver_simplify_tactic.cpp +src/smt/tactic/smt_tactic.cpp +src/tactic/bv/max_bv_sharing_tactic.cpp +src/tactic/bv/bit_blaster_tactic.cpp +src/tactic/bv/bv_size_reduction_tactic.cpp +src/tactic/bv/bv1_blaster_tactic.cpp src/smt/asserted_formulas.cpp src/cmd_context/extra_cmds/subpaving_cmds.cpp src/cmd_context/extra_cmds/dbg_cmds.cpp src/cmd_context/extra_cmds/polynomial_cmds.cpp -src/cmd_context/simplify_cmd.cpp -src/cmd_context/cmd_context.cpp -src/cmd_context/basic_cmds.cpp src/cmd_context/tactic_cmds.cpp -src/cmd_context/interpolant_cmds.cpp +src/cmd_context/simplify_cmd.cpp src/cmd_context/cmd_context_to_goal.cpp -src/cmd_context/echo_tactic.cpp src/cmd_context/cmd_util.cpp +src/cmd_context/echo_tactic.cpp +src/cmd_context/basic_cmds.cpp +src/cmd_context/cmd_context.cpp +src/cmd_context/interpolant_cmds.cpp src/cmd_context/parametric_cmd.cpp src/cmd_context/eval_cmd.cpp -src/math/subpaving/tactic/subpaving_tactic.cpp -src/nlsat/tactic/qfnra_nlsat_tactic.cpp -src/tactic/arith/purify_arith_tactic.cpp -src/tactic/arith/degree_shift_tactic.cpp -src/tactic/arith/fm_tactic.cpp -src/tactic/arith/propagate_ineqs_tactic.cpp -src/tactic/core/tseitin_cnf_tactic.cpp -src/tactic/core/simplify_tactic.cpp -src/tactic/core/ctx_simplify_tactic.cpp -src/api/dll/install_tactic.cpp -src/shell/install_tactic.cpp +src/interp/iz3translate_direct.cpp +src/interp/iz3interp.cpp +src/tactic/aig/aig_tactic.cpp +src/nlsat/tactic/nlsat_tactic.cpp +src/tactic/arith/pb2bv_tactic.cpp +src/tactic/arith/eq2bv_tactic.cpp +src/tactic/arith/add_bounds_tactic.cpp +src/tactic/arith/normalize_bounds_tactic.cpp +src/tactic/arith/fix_dl_var_tactic.cpp +src/tactic/arith/lia2card_tactic.cpp +src/tactic/arith/factor_tactic.cpp +src/tactic/arith/lia2pb_tactic.cpp +src/tactic/arith/recover_01_tactic.cpp +src/tactic/arith/elim01_tactic.cpp +src/tactic/arith/diff_neq_tactic.cpp +src/tactic/arith/card2bv_tactic.cpp +src/tactic/arith/nla2bv_tactic.cpp +src/sat/tactic/sat_tactic.cpp +src/tactic/core/split_clause_tactic.cpp +src/tactic/core/elim_term_ite_tactic.cpp +src/tactic/core/nnf_tactic.cpp +src/tactic/core/cofactor_term_ite_tactic.cpp +src/tactic/core/distribute_forall_tactic.cpp +src/tactic/core/reduce_args_tactic.cpp +src/tactic/core/blast_term_ite_tactic.cpp +src/tactic/core/occf_tactic.cpp +src/tactic/core/solve_eqs_tactic.cpp +src/tactic/core/propagate_values_tactic.cpp +src/tactic/core/symmetry_reduce_tactic.cpp +src/tactic/core/elim_uncnstr_tactic.cpp +src/tactic/core/der_tactic.cpp +src/tactic/core/pb_preprocess_tactic.cpp +src/tactic/tactical.cpp src/api/api_parsers.cpp +src/api/api_tactic.cpp src/opt/optsmt.cpp +src/opt/opt_solver.cpp In file included from ../src/opt/optsmt.cpp:35: ../src/smt/theory_arith.h: In member function 'bool smt::theory_arith::has_var(expr*) const': ../src/smt/theory_arith.h:489:58: warning: invalid use of incomplete type 'class smt::context' @@ -3162,67 +3165,99 @@ ../src/smt/smt_kernel.h:43:11: note: forward declaration of 'class smt::context' class context; ^~~~~~~ -src/opt/opt_solver.cpp +src/tactic/portfolio/default_tactic.cpp +src/sat/sat_solver/inc_sat_solver.cpp +src/tactic/ufbv/ufbv_tactic.cpp +src/tactic/fpa/fpa2bv_tactic.cpp +src/tactic/fpa/qffp_tactic.cpp +src/tactic/smtlogics/qflra_tactic.cpp +src/tactic/smtlogics/qfnia_tactic.cpp +src/tactic/smtlogics/nra_tactic.cpp +src/tactic/smtlogics/qfidl_tactic.cpp +src/tactic/smtlogics/qfauflia_tactic.cpp +src/tactic/smtlogics/qfufbv_tactic.cpp +src/tactic/smtlogics/qfaufbv_tactic.cpp +src/tactic/smtlogics/qfbv_tactic.cpp +src/tactic/smtlogics/qfnra_tactic.cpp +src/tactic/smtlogics/qfufnra_tactic.cpp +src/tactic/smtlogics/quant_tactics.cpp +src/tactic/smtlogics/qfuf_tactic.cpp +src/tactic/smtlogics/qflia_tactic.cpp +src/muz/pdr/pdr_smt_context_manager.cpp +src/muz/pdr/pdr_manager.cpp src/qe/qe.cpp src/tactic/sls/bvsls_opt_engine.cpp +src/tactic/sls/sls_tactic.cpp +src/smt/tactic/ctx_solver_simplify_tactic.cpp src/smt/tactic/unit_subsumption_tactic.cpp src/smt/user_plugin/user_smt_theory.cpp -src/smt/smt_enode.cpp -src/smt/smt_relevancy.cpp -src/smt/smt_model_checker.cpp -src/smt/theory_dummy.cpp -src/smt/theory_wmaxsat.cpp -src/smt/smt_quantifier.cpp -src/smt/smt_checker.cpp -src/smt/dyn_ack.cpp -src/smt/smt_context_pp.cpp -src/smt/smt_model_generator.cpp src/smt/theory_array_full.cpp -src/smt/smt_kernel.cpp src/smt/smt_justification.cpp -src/smt/theory_fpa.cpp -src/smt/arith_eq_adapter.cpp -src/smt/theory_datatype.cpp -src/smt/smt_case_split_queue.cpp +src/smt/smt_checker.cpp src/smt/smt_setup.cpp -src/smt/smt_context_inv.cpp -src/smt/theory_array.cpp -src/smt/theory_pb.cpp -src/smt/smt_model_finder.cpp -src/smt/smt_context.cpp -src/smt/theory_bv.cpp +src/smt/smt_relevancy.cpp +src/smt/theory_datatype.cpp src/smt/smt_theory.cpp -src/smt/smt_context_stat.cpp +src/smt/smt_kernel.cpp +src/smt/theory_pb.cpp +src/smt/smt_conflict_resolution.cpp +src/smt/smt_quantifier.cpp src/smt/mam.cpp +src/smt/qi_queue.cpp +src/smt/smt_context_pp.cpp +src/smt/smt_context.cpp +src/smt/theory_array_base.cpp +src/smt/theory_wmaxsat.cpp +src/smt/smt_model_generator.cpp src/smt/theory_dl.cpp +src/smt/smt_for_each_relevant_expr.cpp +src/smt/theory_array.cpp src/smt/smt_quick_checker.cpp -src/smt/qi_queue.cpp -src/smt/smt_conflict_resolution.cpp +src/smt/smt_case_split_queue.cpp +src/smt/smt_model_checker.cpp +src/smt/arith_eq_adapter.cpp +src/smt/theory_bv.cpp +src/smt/dyn_ack.cpp +src/smt/theory_fpa.cpp src/smt/smt_internalizer.cpp -src/smt/smt_for_each_relevant_expr.cpp -src/smt/theory_array_base.cpp +src/smt/smt_context_stat.cpp +src/smt/smt_model_finder.cpp +src/smt/theory_dummy.cpp +src/smt/smt_context_inv.cpp +src/smt/smt_enode.cpp src/ast/pattern/expr_pattern_match.cpp src/parsers/smt2/smt2parser.cpp src/parsers/smt2/smt2scanner.cpp +src/math/subpaving/tactic/subpaving_tactic.cpp +src/nlsat/tactic/qfnra_nlsat_tactic.cpp +src/tactic/arith/degree_shift_tactic.cpp +src/tactic/arith/fm_tactic.cpp +src/tactic/arith/propagate_ineqs_tactic.cpp +src/tactic/arith/purify_arith_tactic.cpp +src/tactic/core/tseitin_cnf_tactic.cpp +src/tactic/core/ctx_simplify_tactic.cpp +src/tactic/core/simplify_tactic.cpp +src/api/dll/install_tactic.cpp src/shell/smtlib_frontend.cpp -src/muz/pdr/pdr_manager.cpp +src/shell/install_tactic.cpp src/muz/pdr/pdr_util.cpp src/muz/pdr/pdr_prop_solver.cpp src/smt/theory_diff_logic.cpp -src/smt/theory_dense_diff_logic.cpp src/smt/theory_utvpi.cpp -src/opt/wmax.cpp -src/opt/maxres.cpp -src/opt/bcd2.cpp +src/smt/theory_dense_diff_logic.cpp src/opt/opt_cmds.cpp src/opt/maxhs.cpp -src/opt/opt_context.cpp +src/opt/wmax.cpp src/opt/fu_malik.cpp +src/opt/maxsls.cpp +src/opt/opt_context.cpp +src/opt/bcd2.cpp +src/opt/maxres.cpp src/muz/pdr/pdr_reachable_cache.cpp -src/muz/pdr/pdr_closure.cpp src/muz/dataflow/dataflow.cpp src/smt/theory_arith.cpp src/shell/opt_frontend.cpp +src/api/api_opt.cpp In file included from ../src/smt/theory_arith_def.h:22, from ../src/smt/theory_arith.cpp:20: ../src/smt/theory_arith.h: In member function 'bool smt::theory_arith::has_var(expr*) const': @@ -3278,79 +3313,78 @@ ../src/smt/smt_types.h:49:11: note: forward declaration of 'class smt::context' class context; ^~~~~~~ -src/api/api_opt.cpp src/opt/maxsmt.cpp -src/opt/maxsls.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/transforms/dl_mk_slice.cpp -src/muz/transforms/dl_mk_separate_negated_tails.cpp -src/muz/transforms/dl_mk_backwards.cpp -src/muz/transforms/dl_mk_bit_blast.cpp -src/muz/transforms/dl_mk_scale.cpp -src/muz/transforms/dl_mk_karr_invariants.cpp -src/muz/transforms/dl_mk_interp_tail_simplifier.cpp -src/muz/transforms/dl_mk_unbound_compressor.cpp -src/muz/transforms/dl_mk_quantifier_instantiation.cpp -src/muz/transforms/dl_mk_loop_counter.cpp -src/muz/transforms/dl_mk_quantifier_abstraction.cpp -src/muz/transforms/dl_mk_coi_filter.cpp +src/muz/pdr/pdr_closure.cpp +src/muz/pdr/pdr_generalizers.cpp +src/muz/pdr/pdr_context.cpp src/muz/transforms/dl_mk_magic_symbolic.cpp +src/muz/transforms/dl_mk_scale.cpp src/muz/transforms/dl_mk_filter_rules.cpp src/muz/transforms/dl_mk_magic_sets.cpp +src/muz/transforms/dl_mk_quantifier_abstraction.cpp +src/muz/transforms/dl_mk_coi_filter.cpp +src/muz/transforms/dl_mk_unbound_compressor.cpp +src/muz/transforms/dl_mk_backwards.cpp +src/muz/transforms/dl_mk_slice.cpp src/muz/transforms/dl_mk_rule_inliner.cpp -src/muz/base/dl_rule_subsumption_index.cpp -src/muz/base/dl_rule.cpp -src/muz/base/dl_util.cpp -src/muz/base/dl_rule_transformer.cpp +src/muz/transforms/dl_mk_bit_blast.cpp +src/muz/transforms/dl_mk_separate_negated_tails.cpp +src/muz/transforms/dl_mk_interp_tail_simplifier.cpp +src/muz/transforms/dl_mk_loop_counter.cpp +src/muz/transforms/dl_mk_array_blast.cpp +src/muz/transforms/dl_mk_karr_invariants.cpp +src/muz/transforms/dl_mk_quantifier_instantiation.cpp src/muz/base/rule_properties.cpp +src/muz/base/dl_rule_transformer.cpp src/muz/base/dl_costs.cpp src/muz/base/dl_rule_set.cpp src/muz/base/dl_context.cpp +src/muz/base/dl_rule.cpp +src/muz/base/dl_util.cpp +src/muz/base/dl_rule_subsumption_index.cpp src/muz/fp/horn_tactic.cpp -src/muz/pdr/pdr_generalizers.cpp src/muz/pdr/pdr_dl_interface.cpp -src/muz/pdr/pdr_context.cpp src/muz/transforms/dl_mk_subsumption_checker.cpp -src/muz/transforms/dl_mk_unfold.cpp -src/muz/transforms/dl_mk_array_blast.cpp -src/muz/transforms/dl_mk_coalesce.cpp src/muz/transforms/dl_transforms.cpp +src/muz/transforms/dl_mk_coalesce.cpp +src/muz/transforms/dl_mk_unfold.cpp src/muz/fp/dl_register_engine.cpp src/muz/duality/duality_dl_interface.cpp -src/muz/rel/dl_table.cpp -src/muz/rel/dl_check_table.cpp -src/muz/rel/dl_product_relation.cpp -src/muz/rel/dl_mk_partial_equiv.cpp -src/muz/rel/dl_table_relation.cpp -src/muz/rel/dl_lazy_table.cpp -src/muz/rel/dl_sieve_relation.cpp -src/muz/rel/dl_external_relation.cpp -src/muz/rel/karr_relation.cpp -src/muz/rel/dl_mk_similarity_compressor.cpp -src/muz/rel/udoc_relation.cpp -src/muz/rel/dl_sparse_table.cpp +src/muz/rel/dl_mk_simple_joins.cpp src/muz/rel/dl_instruction.cpp -src/muz/rel/dl_base.cpp src/muz/rel/check_relation.cpp -src/muz/rel/dl_interval_relation.cpp +src/muz/rel/dl_sparse_table.cpp +src/muz/rel/dl_mk_similarity_compressor.cpp src/muz/rel/aig_exporter.cpp -src/muz/rel/dl_mk_simple_joins.cpp +src/muz/rel/udoc_relation.cpp +src/muz/rel/dl_mk_partial_equiv.cpp +src/muz/rel/dl_external_relation.cpp +src/muz/rel/dl_lazy_table.cpp +src/muz/rel/dl_table.cpp +src/muz/rel/dl_base.cpp +src/muz/rel/dl_sieve_relation.cpp +src/muz/rel/dl_table_relation.cpp src/api/api_datalog.cpp src/muz/fp/dl_cmds.cpp -src/muz/rel/dl_relation_manager.cpp -src/muz/rel/dl_mk_explanations.cpp -src/muz/rel/dl_finite_product_relation.cpp +src/muz/rel/dl_check_table.cpp src/muz/rel/dl_compiler.cpp -src/shell/datalog_frontend.cpp +src/muz/rel/dl_interval_relation.cpp +src/muz/rel/karr_relation.cpp src/muz/rel/rel_context.cpp +src/muz/rel/dl_product_relation.cpp +src/muz/rel/dl_finite_product_relation.cpp +src/muz/rel/dl_mk_explanations.cpp +src/muz/rel/dl_relation_manager.cpp +src/shell/datalog_frontend.cpp src/muz/rel/dl_bound_relation.cpp -g++ -o z3 shell/main.o shell/smtlib_frontend.o shell/z3_log_frontend.o shell/datalog_frontend.o shell/dimacs_frontend.o shell/gparams_register_modules.o shell/install_tactic.o shell/mem_initializer.o shell/opt_frontend.o api/api.a opt/opt.a parsers/smt/smtparser.a tactic/portfolio/portfolio.a sat/sat_solver/sat_solver.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/dataflow/dataflow.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 -Wl,-z,now -fopenmp -lrt -g++ -o libz3.so -Wl,-z,relro -Wl,-z,now -fPIC -shared -Wl,-soname,libz3.so.4 api/dll/dll.o api/dll/gparams_register_modules.o api/dll/install_tactic.o api/dll/mem_initializer.o api/api_parsers.o api/api_stats.o api/api_polynomial.o api/api_rcf.o api/api_log_macros.o api/api_solver.o api/api_datatype.o api/z3_replayer.o api/api_numeral.o api/api_log.o api/api_solver_old.o api/api_model.o api/api_datalog.o api/api_algebraic.o api/api_fpa.o api/api_interp.o api/api_commands.o api/api_bv.o api/api_array.o api/api_params.o api/api_user_theory.o api/api_tactic.o api/api_pb.o api/api_goal.o api/api_opt.o api/api_ast_vector.o api/api_ast.o api/api_ast_map.o api/api_config_params.o api/api_context.o api/api_arith.o api/api_quant.o opt/opt.a parsers/smt/smtparser.a tactic/portfolio/portfolio.a sat/sat_solver/sat_solver.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/dataflow/dataflow.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 -mcs /lib:/usr/lib/mono/4.5 /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /filealign:512 /linkresource:libz3.dll /out:Microsoft.Z3.dll /target:library /doc:Microsoft.Z3.xml /optimize+ /platform:x86 ../src/api/dotnet/BitVecExpr.cs ../src/api/dotnet/Constructor.cs ../src/api/dotnet/Statistics.cs ../src/api/dotnet/EnumSort.cs ../src/api/dotnet/Global.cs ../src/api/dotnet/Version.cs ../src/api/dotnet/Z3Object.cs ../src/api/dotnet/ApplyResult.cs ../src/api/dotnet/InterpolationContext.cs ../src/api/dotnet/UninterpretedSort.cs ../src/api/dotnet/IntNum.cs ../src/api/dotnet/RealSort.cs ../src/api/dotnet/StringSymbol.cs ../src/api/dotnet/ArraySort.cs ../src/api/dotnet/FiniteDomainSort.cs ../src/api/dotnet/IntSymbol.cs ../src/api/dotnet/FPExpr.cs ../src/api/dotnet/IntSort.cs ../src/api/dotnet/Params.cs ../src/api/dotnet/Sort.cs ../src/api/dotnet/RatNum.cs ../src/api/dotnet/ArithExpr.cs ../src/api/dotnet/IDecRefQueue.cs ../src/api/dotnet/ArrayExpr.cs ../src/api/dotnet/FuncInterp.cs ../src/api/dotnet/RelationSort.cs ../src/api/dotnet/BitVecSort.cs ../src/api/dotnet/Probe.cs ../src/api/dotnet/FPNum.cs ../src/api/dotnet/Status.cs ../src/api/dotnet/BoolExpr.cs ../src/api/dotnet/DatatypeSort.cs ../src/api/dotnet/SetSort.cs ../src/api/dotnet/Symbol.cs ../src/api/dotnet/ASTMap.cs ../src/api/dotnet/FuncDecl.cs ../src/api/dotnet/Log.cs ../src/api/dotnet/Tactic.cs ../src/api/dotnet/BoolSort.cs ../src/api/dotnet/FPSort.cs ../src/api/dotnet/Quantifier.cs ../src/api/dotnet/ASTVector.cs ../src/api/dotnet/AlgebraicNum.cs ../src/api/dotnet/ConstructorList.cs ../src/api/dotnet/Expr.cs ../src/api/dotnet/Solver.cs ../src/api/dotnet/Native.cs ../src/api/dotnet/Goal.cs ../src/api/dotnet/FPRMNum.cs ../src/api/dotnet/ArithSort.cs ../src/api/dotnet/RealExpr.cs ../src/api/dotnet/TupleSort.cs ../src/api/dotnet/Optimize.cs ../src/api/dotnet/Fixedpoint.cs ../src/api/dotnet/Z3Exception.cs ../src/api/dotnet/Pattern.cs ../src/api/dotnet/FPRMSort.cs ../src/api/dotnet/Deprecated.cs ../src/api/dotnet/DatatypeExpr.cs ../src/api/dotnet/Model.cs ../src/api/dotnet/Context.cs ../src/api/dotnet/Enumerations.cs ../src/api/dotnet/ListSort.cs ../src/api/dotnet/IntExpr.cs ../src/api/dotnet/ParamDescrs.cs ../src/api/dotnet/FPRMExpr.cs ../src/api/dotnet/BitVecNum.cs ../src/api/dotnet/AST.cs ../src/api/dotnet/Properties/AssemblyInfo.cs +g++ -o z3 shell/gparams_register_modules.o shell/smtlib_frontend.o shell/mem_initializer.o shell/datalog_frontend.o shell/install_tactic.o shell/dimacs_frontend.o shell/z3_log_frontend.o shell/opt_frontend.o shell/main.o api/api.a opt/opt.a parsers/smt/smtparser.a tactic/portfolio/portfolio.a sat/sat_solver/sat_solver.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/dataflow/dataflow.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 -Wl,-z,now -fopenmp -lrt +g++ -o libz3.so -Wl,-z,relro -Wl,-z,now -fPIC -shared -Wl,-soname,libz3.so.4 api/dll/gparams_register_modules.o api/dll/mem_initializer.o api/dll/install_tactic.o api/dll/dll.o api/api_model.o api/api_parsers.o api/api_arith.o api/api_tactic.o api/api_datalog.o api/api_solver_old.o api/api_bv.o api/api_array.o api/api_stats.o api/api_numeral.o api/api_polynomial.o api/api_config_params.o api/z3_replayer.o api/api_algebraic.o api/api_fpa.o api/api_rcf.o api/api_datatype.o api/api_commands.o api/api_goal.o api/api_ast.o api/api_context.o api/api_interp.o api/api_user_theory.o api/api_ast_vector.o api/api_params.o api/api_log_macros.o api/api_quant.o api/api_ast_map.o api/api_solver.o api/api_pb.o api/api_log.o api/api_opt.o opt/opt.a parsers/smt/smtparser.a tactic/portfolio/portfolio.a sat/sat_solver/sat_solver.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/dataflow/dataflow.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 +mcs /lib:/usr/lib/mono/4.5 /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /filealign:512 /linkresource:libz3.dll /out:Microsoft.Z3.dll /target:library /doc:Microsoft.Z3.xml /optimize+ /platform:x86 ../src/api/dotnet/Optimize.cs ../src/api/dotnet/IntExpr.cs ../src/api/dotnet/ArraySort.cs ../src/api/dotnet/ASTMap.cs ../src/api/dotnet/Deprecated.cs ../src/api/dotnet/FPRMNum.cs ../src/api/dotnet/Pattern.cs ../src/api/dotnet/ASTVector.cs ../src/api/dotnet/Tactic.cs ../src/api/dotnet/TupleSort.cs ../src/api/dotnet/Enumerations.cs ../src/api/dotnet/IntSort.cs ../src/api/dotnet/RelationSort.cs ../src/api/dotnet/DatatypeSort.cs ../src/api/dotnet/BoolSort.cs ../src/api/dotnet/EnumSort.cs ../src/api/dotnet/Quantifier.cs ../src/api/dotnet/IntSymbol.cs ../src/api/dotnet/ArithExpr.cs ../src/api/dotnet/Z3Exception.cs ../src/api/dotnet/BitVecSort.cs ../src/api/dotnet/FuncInterp.cs ../src/api/dotnet/InterpolationContext.cs ../src/api/dotnet/ArrayExpr.cs ../src/api/dotnet/Log.cs ../src/api/dotnet/DatatypeExpr.cs ../src/api/dotnet/ApplyResult.cs ../src/api/dotnet/ArithSort.cs ../src/api/dotnet/IntNum.cs ../src/api/dotnet/UninterpretedSort.cs ../src/api/dotnet/BitVecNum.cs ../src/api/dotnet/Symbol.cs ../src/api/dotnet/RealSort.cs ../src/api/dotnet/FPRMSort.cs ../src/api/dotnet/ListSort.cs ../src/api/dotnet/FPSort.cs ../src/api/dotnet/Fixedpoint.cs ../src/api/dotnet/RatNum.cs ../src/api/dotnet/Z3Object.cs ../src/api/dotnet/Status.cs ../src/api/dotnet/AST.cs ../src/api/dotnet/RealExpr.cs ../src/api/dotnet/Goal.cs ../src/api/dotnet/Expr.cs ../src/api/dotnet/Solver.cs ../src/api/dotnet/IDecRefQueue.cs ../src/api/dotnet/FPNum.cs ../src/api/dotnet/FiniteDomainSort.cs ../src/api/dotnet/BoolExpr.cs ../src/api/dotnet/AlgebraicNum.cs ../src/api/dotnet/FPExpr.cs ../src/api/dotnet/Constructor.cs ../src/api/dotnet/Model.cs ../src/api/dotnet/Context.cs ../src/api/dotnet/Params.cs ../src/api/dotnet/Statistics.cs ../src/api/dotnet/Global.cs ../src/api/dotnet/Native.cs ../src/api/dotnet/FPRMExpr.cs ../src/api/dotnet/ParamDescrs.cs ../src/api/dotnet/BitVecExpr.cs ../src/api/dotnet/Probe.cs ../src/api/dotnet/ConstructorList.cs ../src/api/dotnet/Version.cs ../src/api/dotnet/StringSymbol.cs ../src/api/dotnet/FuncDecl.cs ../src/api/dotnet/SetSort.cs ../src/api/dotnet/Sort.cs ../src/api/dotnet/Properties/AssemblyInfo.cs g++ -Wdate-time -D_FORTIFY_SOURCE=2 -D_MP_INTERNAL -g -O2 -ffile-prefix-map=/build/z3-4.4.1=. -fstack-protector-strong -Wformat -Werror=format-security -fvisibility=hidden -c -mfpu=vfp -mfloat-abi=hard -fopenmp -O3 -D _EXTERNAL_RELEASE -fomit-frame-pointer -fno-strict-aliasing -D_LINUX_ -o api/java/Native.o -I"/usr/lib/jvm/java-11-openjdk-armhf/include" -I"/usr/lib/jvm/java-11-openjdk-armhf/include/linux" -I../src/api ../src/api/java/Native.cpp gcc -Wdate-time -D_FORTIFY_SOURCE=2 -D_MP_INTERNAL -g -O2 -ffile-prefix-map=/build/z3-4.4.1=. -fstack-protector-strong -Wformat -Werror=format-security -fvisibility=hidden -c -mfpu=vfp -mfloat-abi=hard -fopenmp -O3 -D _EXTERNAL_RELEASE -fomit-frame-pointer -fno-strict-aliasing -D_LINUX_ -I /usr/lib/ocaml -I ../src/api api/ml/z3native_stubs.c -o api/ml/z3native_stubs.o ../src/api/dotnet/InterpolationContext.cs(34,16): warning CS1574: XML comment on `Microsoft.Z3.InterpolationContext.InterpolationContext(System.Collections.Generic.Dictionary)' has cref attribute `Context.Context(Dictionary)' that could not be resolved @@ -3376,115 +3410,112 @@ make[2]: Entering directory '/build/z3-4.4.1' /usr/bin/make -C build test-z3 make[3]: Entering directory '/build/z3-4.4.1/build' -src/test/object_allocator.cpp -src/test/buffer.cpp -src/test/main.cpp -src/test/smt2print_parse.cpp -src/test/simplifier.cpp +src/test/f2n.cpp +src/test/symbol.cpp +src/test/polynorm.cpp +src/test/symbol_table.cpp +src/test/gparams_register_modules.cpp +src/test/prime_generator.cpp +src/test/uint_set.cpp src/test/map.cpp -src/test/horn_subsume_model_converter.cpp -src/test/heap.cpp -src/test/api_bug.cpp -src/test/dl_table.cpp +src/test/old_interval.cpp src/test/substitution.cpp -src/test/var_subst.cpp -src/test/upolynomial.cpp -src/test/ex.cpp -src/test/stack.cpp -src/test/simple_parser.cpp -src/test/dl_product_relation.cpp -src/test/string_buffer.cpp -src/test/ast.cpp -src/test/mpff.cpp -src/test/mpf.cpp +src/test/optional.cpp +src/test/hwf.cpp +src/test/buffer.cpp src/test/mpz.cpp src/test/ext_numeral.cpp -src/test/get_implied_equalities.cpp +src/test/dl_query.cpp +src/test/horn_subsume_model_converter.cpp src/test/polynomial_factorization.cpp -src/test/mpfx.cpp -src/test/dl_util.cpp -src/test/qe_arith.cpp -src/test/no_overflow.cpp -src/test/parray.cpp -src/test/mpq.cpp -src/test/model2expr.cpp -src/test/region.cpp -src/test/quant_elim.cpp -src/test/matcher.cpp +src/test/stack.cpp +src/test/theory_pb.cpp +src/test/api_bug.cpp +src/test/mem_initializer.cpp +src/test/var_subst.cpp src/test/rcf.cpp -src/test/pdr.cpp -src/test/expr_substitution.cpp -src/test/api.cpp -src/test/symbol_table.cpp -src/test/arith_rewriter.cpp -src/test/bits.cpp -src/test/sat_user_scope.cpp +src/test/interval.cpp +src/test/dl_product_relation.cpp +src/test/nlarith_util.cpp src/test/vector.cpp -src/test/tbv.cpp -src/test/total_order.cpp -src/test/arith_simplifier_plugin.cpp -src/test/proof_checker.cpp +src/test/ddnf.cpp src/test/expr_rand.cpp -src/test/prime_generator.cpp -src/test/chashtable.cpp -src/test/list.cpp -src/test/gparams_register_modules.cpp +src/test/model_retrieval.cpp +src/test/heap_trie.cpp +src/test/heap.cpp +src/test/arith_simplifier_plugin.cpp +src/test/total_order.cpp src/test/diff_logic.cpp -src/test/theory_pb.cpp -src/test/f2n.cpp -src/test/sorting_network.cpp -src/test/polynorm.cpp -src/test/random.cpp -src/test/hashtable.cpp src/test/smt_context.cpp -src/test/optional.cpp -src/test/check_assumptions.cpp -src/test/interval.cpp -src/test/hwf.cpp -src/test/heap_trie.cpp -src/test/simplex.cpp +src/test/hashtable.cpp +src/test/escaped.cpp src/test/dl_relation.cpp -src/test/datalog_parser.cpp -src/test/model_retrieval.cpp -src/test/udoc_relation.cpp +src/test/dl_context.cpp +src/test/bit_vector.cpp +src/test/random.cpp +src/test/inf_rational.cpp src/test/trigo.cpp -src/test/factor_rewriter.cpp -src/test/dl_query.cpp -src/test/hilbert_basis.cpp -src/test/nlsat.cpp +src/test/karr.cpp +src/test/simplifier.cpp +src/test/mpfx.cpp src/test/install_tactic.cpp +src/test/udoc_relation.cpp +src/test/mpff.cpp +src/test/pdr.cpp +src/test/region.cpp +src/test/check_assumptions.cpp +src/test/expr_substitution.cpp +src/test/fixed_bit_vector.cpp +src/test/list.cpp src/test/bv_simplifier_plugin.cpp -src/test/timeout.cpp +src/test/quant_elim.cpp +src/test/get_implied_equalities.cpp src/test/quant_solve.cpp -src/test/small_object_allocator.cpp -src/test/ddnf.cpp -src/test/polynomial.cpp +src/test/memory.cpp src/test/theory_dl.cpp -src/test/escaped.cpp -src/test/permutation.cpp -src/test/mem_initializer.cpp -src/test/fixed_bit_vector.cpp -src/test/karr.cpp -src/test/dl_context.cpp -src/test/bit_vector.cpp -src/test/inf_rational.cpp +src/test/mpq.cpp +src/test/ast.cpp +src/test/datalog_parser.cpp +src/test/polynomial.cpp src/test/doc.cpp -src/test/symbol.cpp -src/test/memory.cpp -src/test/algebraic.cpp -src/test/old_interval.cpp -src/test/for_each_file.cpp +src/test/timeout.cpp +src/test/parray.cpp +src/test/main.cpp +src/test/ex.cpp +src/test/bits.cpp +src/test/string_buffer.cpp +src/test/no_overflow.cpp +src/test/simple_parser.cpp +src/test/mpf.cpp +src/test/proof_checker.cpp +src/test/nlsat.cpp +src/test/tbv.cpp +src/test/dl_util.cpp +src/test/matcher.cpp +src/test/sorting_network.cpp +src/test/object_allocator.cpp +src/test/permutation.cpp src/test/rational.cpp -src/test/uint_set.cpp +src/test/sat_user_scope.cpp +src/test/dl_table.cpp +src/test/smt2print_parse.cpp +src/test/small_object_allocator.cpp +src/test/for_each_file.cpp +src/test/factor_rewriter.cpp +src/test/arith_rewriter.cpp +src/test/qe_arith.cpp +src/test/upolynomial.cpp +src/test/algebraic.cpp src/test/bit_blaster.cpp +src/test/simplex.cpp +src/test/model2expr.cpp +src/test/chashtable.cpp +src/test/api.cpp +src/test/hilbert_basis.cpp src/test/mpbq.cpp -src/test/nlarith_util.cpp -src/api/api_solver.cpp -src/api/api_interp.cpp src/test/fuzzing/expr_rand.cpp src/test/fuzzing/expr_delta.cpp -src/smt/smt_implied_equalities.cpp -g++ -o test-z3 test/object_allocator.o test/buffer.o test/main.o test/smt2print_parse.o test/simplifier.o test/map.o test/horn_subsume_model_converter.o test/heap.o test/api_bug.o test/dl_table.o test/substitution.o test/var_subst.o test/upolynomial.o test/ex.o test/stack.o test/simple_parser.o test/dl_product_relation.o test/string_buffer.o test/ast.o test/mpff.o test/mpf.o test/mpz.o test/ext_numeral.o test/get_implied_equalities.o test/polynomial_factorization.o test/mpfx.o test/dl_util.o test/qe_arith.o test/no_overflow.o test/parray.o test/mpq.o test/model2expr.o test/region.o test/quant_elim.o test/matcher.o test/rcf.o test/pdr.o test/expr_substitution.o test/api.o test/symbol_table.o test/arith_rewriter.o test/bits.o test/sat_user_scope.o test/vector.o test/tbv.o test/total_order.o test/arith_simplifier_plugin.o test/proof_checker.o test/expr_rand.o test/prime_generator.o test/chashtable.o test/list.o test/gparams_register_modules.o test/diff_logic.o test/theory_pb.o test/f2n.o test/sorting_network.o test/polynorm.o test/random.o test/hashtable.o test/smt_context.o test/optional.o test/check_assumptions.o test/interval.o test/hwf.o test/heap_trie.o test/simplex.o test/dl_relation.o test/datalog_parser.o test/model_retrieval.o test/udoc_relation.o test/trigo.o test/factor_rewriter.o test/dl_query.o test/hilbert_basis.o test/nlsat.o test/install_tactic.o test/bv_simplifier_plugin.o test/timeout.o test/quant_solve.o test/small_object_allocator.o test/ddnf.o test/polynomial.o test/theory_dl.o test/escaped.o test/permutation.o test/mem_initializer.o test/fixed_bit_vector.o test/karr.o test/dl_context.o test/bit_vector.o test/inf_rational.o test/doc.o test/symbol.o test/memory.o test/algebraic.o test/old_interval.o test/for_each_file.o test/rational.o test/uint_set.o test/bit_blaster.o test/mpbq.o test/nlarith_util.o api/api.a opt/opt.a parsers/smt/smtparser.a tactic/portfolio/portfolio.a sat/sat_solver/sat_solver.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/dataflow/dataflow.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 -Wl,-z,now -fopenmp -lrt +g++ -o test-z3 test/f2n.o test/symbol.o test/polynorm.o test/symbol_table.o test/gparams_register_modules.o test/prime_generator.o test/uint_set.o test/map.o test/old_interval.o test/substitution.o test/optional.o test/hwf.o test/buffer.o test/mpz.o test/ext_numeral.o test/dl_query.o test/horn_subsume_model_converter.o test/polynomial_factorization.o test/stack.o test/theory_pb.o test/api_bug.o test/mem_initializer.o test/var_subst.o test/rcf.o test/interval.o test/dl_product_relation.o test/nlarith_util.o test/vector.o test/ddnf.o test/expr_rand.o test/model_retrieval.o test/heap_trie.o test/heap.o test/arith_simplifier_plugin.o test/total_order.o test/diff_logic.o test/smt_context.o test/hashtable.o test/escaped.o test/dl_relation.o test/dl_context.o test/bit_vector.o test/random.o test/inf_rational.o test/trigo.o test/karr.o test/simplifier.o test/mpfx.o test/install_tactic.o test/udoc_relation.o test/mpff.o test/pdr.o test/region.o test/check_assumptions.o test/expr_substitution.o test/fixed_bit_vector.o test/list.o test/bv_simplifier_plugin.o test/quant_elim.o test/get_implied_equalities.o test/quant_solve.o test/memory.o test/theory_dl.o test/mpq.o test/ast.o test/datalog_parser.o test/polynomial.o test/doc.o test/timeout.o test/parray.o test/main.o test/ex.o test/bits.o test/string_buffer.o test/no_overflow.o test/simple_parser.o test/mpf.o test/proof_checker.o test/nlsat.o test/tbv.o test/dl_util.o test/matcher.o test/sorting_network.o test/object_allocator.o test/permutation.o test/rational.o test/sat_user_scope.o test/dl_table.o test/smt2print_parse.o test/small_object_allocator.o test/for_each_file.o test/factor_rewriter.o test/arith_rewriter.o test/qe_arith.o test/upolynomial.o test/algebraic.o test/bit_blaster.o test/simplex.o test/model2expr.o test/chashtable.o test/api.o test/hilbert_basis.o test/mpbq.o api/api.a opt/opt.a parsers/smt/smtparser.a tactic/portfolio/portfolio.a sat/sat_solver/sat_solver.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/dataflow/dataflow.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 -Wl,-z,now -fopenmp -lrt make[3]: Leaving directory '/build/z3-4.4.1/build' make[2]: Leaving directory '/build/z3-4.4.1' build/test-z3 -a @@ -3495,25 +3526,25 @@ resize 1000000000 out of memory PASS -(test vector :time 0.00 :before-memory 0.02 :after-memory 876.88) +(test vector :time 0.02 :before-memory 0.02 :after-memory 876.88) resize 1000000000 out of memory PASS -(test vector :time 0.00 :before-memory 876.88 :after-memory 2192.19) +(test vector :time 0.02 :before-memory 876.88 :after-memory 1461.46) PASS -(test symbol_table :time 0.00 :before-memory 2192.19 :after-memory 2192.19) +(test symbol_table :time 0.00 :before-memory 1461.46 :after-memory 1461.46) PASS -(test symbol_table :time 0.00 :before-memory 2192.19 :after-memory 2192.19) +(test symbol_table :time 0.00 :before-memory 1461.46 :after-memory 1461.46) PASS -(test region :time 0.00 :before-memory 2192.19 :after-memory 2192.19) +(test region :time 0.00 :before-memory 1461.46 :after-memory 1461.46) PASS -(test region :time 0.00 :before-memory 2192.19 :after-memory 2192.19) +(test region :time 0.00 :before-memory 1461.46 :after-memory 1461.46) foo boo foo PASS -(test symbol :time 0.00 :before-memory 2192.19 :after-memory 2192.19) +(test symbol :time 0.00 :before-memory 1461.46 :after-memory 1461.46) foo boo foo PASS -(test symbol :time 0.00 :before-memory 2192.19 :after-memory 2192.19) +(test symbol :time 0.00 :before-memory 1461.46 :after-memory 1461.46) i: 0 i: 1000 i: 2000 @@ -3615,7 +3646,7 @@ i: 98000 i: 99000 PASS -(test heap :time 0.05 :before-memory 2192.19 :after-memory 2192.19) +(test heap :time 0.17 :before-memory 1461.46 :after-memory 1461.46) i: 0 i: 1000 i: 2000 @@ -3717,11 +3748,11 @@ i: 98000 i: 99000 PASS -(test heap :time 0.04 :before-memory 2192.19 :after-memory 2192.19) +(test heap :time 0.13 :before-memory 1461.46 :after-memory 1461.46) PASS -(test hashtable :time 0.00 :before-memory 2192.19 :after-memory 2192.19) +(test hashtable :time 0.00 :before-memory 1461.46 :after-memory 1461.46) PASS -(test hashtable :time 0.00 :before-memory 2192.19 :after-memory 2192.19) +(test hashtable :time 0.00 :before-memory 1461.46 :after-memory 1461.46) sizeof(rational): 16 int64_max: 9223372036854775807, INT64_MAX: 9223372036854775807, int64_max.get_int64(): 9223372036854775807, int64_max.get_uint64(): 9223372036854775807 running tst6 @@ -3745,19 +3776,19 @@ 41 7 5 6 41 == 41 running rational_tester::tst1 -(multiplication with big rationals :time 14.54 :before-memory 2192.42 :after-memory 2241.85) -(multiplication with floats: :time 0.00 :before-memory 2241.85 :after-memory 2241.85) +(multiplication with big rationals :time 27.46 :before-memory 1461.69 :after-memory 1511.13) +(multiplication with floats: :time 0.00 :before-memory 1511.13 :after-memory 1511.13) Testing multiplication performace using small ints -(multiplication with rationals :time 0.03 :before-memory 2231.54 :after-memory 2231.54) -(multiplication with floats: :time 0.00 :before-memory 2231.54 :after-memory 2231.54) +(multiplication with rationals :time 0.05 :before-memory 1500.81 :after-memory 1500.81) +(multiplication with floats: :time 0.01 :before-memory 1500.81 :after-memory 1500.81) Testing multiplication performace using small rationals -(multiplication with rationals :time 0.81 :before-memory 2231.54 :after-memory 2231.54) -(multiplication with floats: :time 0.00 :before-memory 2231.54 :after-memory 2231.54) +(multiplication with rationals :time 1.27 :before-memory 1500.81 :after-memory 1500.81) +(multiplication with floats: :time 0.02 :before-memory 1500.81 :after-memory 1500.81) PASS -(test rational :time 17.70 :before-memory 2192.19 :after-memory 2195.49) +(test rational :time 34.72 :before-memory 1461.46 :after-memory 1464.77) sizeof(rational): 16 int64_max: 9223372036854775807, INT64_MAX: 9223372036854775807, int64_max.get_int64(): 9223372036854775807, int64_max.get_uint64(): 9223372036854775807 running tst6 @@ -3781,31 +3812,31 @@ 41 7 5 6 41 == 41 running rational_tester::tst1 -(multiplication with big rationals :time 14.60 :before-memory 2195.72 :after-memory 2241.93) -(multiplication with floats: :time 0.00 :before-memory 2241.93 :after-memory 2241.93) +(multiplication with big rationals :time 26.49 :before-memory 1465.00 :after-memory 1511.21) +(multiplication with floats: :time 0.00 :before-memory 1511.21 :after-memory 1511.21) Testing multiplication performace using small ints -(multiplication with rationals :time 0.03 :before-memory 2231.57 :after-memory 2231.57) -(multiplication with floats: :time 0.00 :before-memory 2231.57 :after-memory 2231.57) +(multiplication with rationals :time 0.05 :before-memory 1500.85 :after-memory 1500.85) +(multiplication with floats: :time 0.01 :before-memory 1500.85 :after-memory 1500.85) Testing multiplication performace using small rationals -(multiplication with rationals :time 0.80 :before-memory 2231.57 :after-memory 2231.57) -(multiplication with floats: :time 0.00 :before-memory 2231.57 :after-memory 2231.57) +(multiplication with rationals :time 1.27 :before-memory 1500.85 :after-memory 1500.85) +(multiplication with floats: :time 0.02 :before-memory 1500.85 :after-memory 1500.85) PASS -(test rational :time 17.74 :before-memory 2195.49 :after-memory 2195.52) +(test rational :time 32.90 :before-memory 1464.77 :after-memory 1464.80) PASS -(test inf_rational :time 0.00 :before-memory 2195.52 :after-memory 2195.52) +(test inf_rational :time 0.00 :before-memory 1464.80 :after-memory 1464.80) PASS -(test inf_rational :time 0.00 :before-memory 2195.52 :after-memory 2195.52) +(test inf_rational :time 0.00 :before-memory 1464.80 :after-memory 1464.80) PASS -(test ast :time 0.00 :before-memory 2195.52 :after-memory 2195.52) +(test ast :time 0.00 :before-memory 1464.80 :after-memory 1464.80) PASS -(test ast :time 0.00 :before-memory 2195.52 :after-memory 2195.52) +(test ast :time 0.00 :before-memory 1464.80 :after-memory 1464.80) PASS -(test optional :time 0.00 :before-memory 2195.52 :after-memory 2195.52) +(test optional :time 0.00 :before-memory 1464.80 :after-memory 1464.80) PASS -(test optional :time 0.00 :before-memory 2195.52 :after-memory 2195.52) +(test optional :time 0.00 :before-memory 1464.80 :after-memory 1464.80) b: 000001000001100000001000000000100001000000000000000000000000000000000000000001111000000000000000000010000000000 b: 0000010000011000000010000000001000010000000000000000000000000000000000000000011110000000000000000000100000000000000000000000000 b: 00000100000110000000100000000010000100000000000000000000000000000000000000000111100000000000000000001000000000000000000000000000 @@ -3824,7 +3855,7 @@ ------ b1: 00100 PASS -(test bit_vector :time 0.00 :before-memory 2195.52 :after-memory 2195.52) +(test bit_vector :time 0.00 :before-memory 1464.80 :after-memory 1464.80) b: 000001000001100000001000000000100001000000000000000000000000000000000000000001111000000000000000000010000000000 b: 0000010000011000000010000000001000010000000000000000000000000000000000000000011110000000000000000000100000000000000000000000000 b: 00000100000110000000100000000010000100000000000000000000000000000000000000000111100000000000000000001000000000000000000000000000 @@ -3843,17 +3874,17 @@ ------ b1: 00100 PASS -(test bit_vector :time 0.00 :before-memory 2195.52 :after-memory 2195.52) +(test bit_vector :time 0.00 :before-memory 1464.80 :after-memory 1464.80) 0000010000 0100001110 0100011110 PASS -(test fixed_bit_vector :time 0.00 :before-memory 2195.52 :after-memory 2195.52) +(test fixed_bit_vector :time 0.00 :before-memory 1464.80 :after-memory 1464.80) 0000010000 0100001110 0100011110 PASS -(test fixed_bit_vector :time 0.00 :before-memory 2195.52 :after-memory 2195.52) +(test fixed_bit_vector :time 0.00 :before-memory 1464.80 :after-memory 1464.80) [] [] [] @@ -3883,7 +3914,7 @@ 00000000000011111 111111111111x1011 -> 111111111111x01 PASS -(test tbv :time 0.00 :before-memory 2195.52 :after-memory 2195.52) +(test tbv :time 0.00 :before-memory 1464.80 :after-memory 1464.80) [] [] [] @@ -3913,7 +3944,7 @@ 00000000000011111 111111111111x1011 -> 111111111111x01 PASS -(test tbv :time 0.00 :before-memory 2195.52 :after-memory 2195.52) +(test tbv :time 0.00 :before-memory 1464.80 :after-memory 1464.80) xxxx \ {xxx0} xxx (or (and true (not (not true))) (and true (not (not false)))) true @@ -3959,7 +3990,7 @@ 1111111111111111111111111111111111111111111111111111111111111111111111} -> 11111111111111111111111111111111111111111111111111111111111111111xx1 \ { 11111111111111111111111111111111111111111111111111111111111111111111} PASS -(test doc :time 109.56 :before-memory 2195.52 :after-memory 2195.56) +(test doc :time 213.46 :before-memory 1464.80 :after-memory 1464.84) xxxx \ {xxx0} xxx (or (and true (not (not true))) (and true (not (not false)))) true @@ -4005,7 +4036,7 @@ 1111111111111111111111111111111111111111111111111111111111111111111111} -> 11111111111111111111111111111111111111111111111111111111111111111xx1 \ { 11111111111111111111111111111111111111111111111111111111111111111111} PASS -(test doc :time 108.93 :before-memory 2195.56 :after-memory 2195.56) +(test doc :time 222.34 :before-memory 1464.84 :after-memory 1464.84) {xxx \ {0x1}} {xxx \ {0x0, 1x1}} {0xxx \ {00xx, 0101, 0111}} @@ -11527,7 +11558,7 @@ xxxxxx1xxxxxxxx0xx} PASS -(test udoc_relation :time 10.92 :before-memory 2195.56 :after-memory 2195.58) +(test udoc_relation :time 24.72 :before-memory 1464.84 :after-memory 1464.86) {xxx \ {0x1}} {xxx \ {0x0, 1x1}} {0xxx \ {00xx, 0101, 0111}} @@ -19049,35 +19080,35 @@ xxxxxx1xxxxxxxx0xx} PASS -(test udoc_relation :time 11.51 :before-memory 2195.58 :after-memory 2195.58) +(test udoc_relation :time 22.47 :before-memory 1464.86 :after-memory 1464.86) PASS -(test string_buffer :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test string_buffer :time 0.01 :before-memory 1464.86 :after-memory 1464.86) PASS -(test string_buffer :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test string_buffer :time 0.01 :before-memory 1464.86 :after-memory 1464.86) PASS -(test map :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test map :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test map :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test map :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test diff_logic :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test diff_logic :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test diff_logic :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test diff_logic :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test uint_set :time 0.08 :before-memory 2195.58 :after-memory 2195.58) +(test uint_set :time 0.22 :before-memory 1464.86 :after-memory 1464.86) PASS -(test uint_set :time 0.08 :before-memory 2195.58 :after-memory 2195.58) +(test uint_set :time 0.22 :before-memory 1464.86 :after-memory 1464.86) PASS -(test list :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test list :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test list :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test list :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test small_object_allocator :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test small_object_allocator :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test small_object_allocator :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test small_object_allocator :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test timeout :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test timeout :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test timeout :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test timeout :time 0.00 :before-memory 1464.86 :after-memory 1464.86) [hypothesis]: a #5 := (not a) [hypothesis]: #5 @@ -19093,7 +19124,7 @@ #7 := [unit-resolution #4 #6]: false [lemma #7]: #10 PASS -(test proof_checker :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test proof_checker :time 0.00 :before-memory 1464.86 :after-memory 1464.86) [hypothesis]: a #5 := (not a) [hypothesis]: #5 @@ -19109,11 +19140,11 @@ #7 := [unit-resolution #4 #6]: false [lemma #7]: #10 PASS -(test proof_checker :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test proof_checker :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test simplifier :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test simplifier :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test simplifier :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test simplifier :time 0.00 :before-memory 1464.86 :after-memory 1464.86) compare: 0 >> 0 = 0 with #x00000000 0 compare: 0 >> 1 = 0 with #x00000000 @@ -19277,7 +19308,7 @@ compare: -43556211 >> 4251411085 = -1 with #xffffffff -1 PASS -(test bv_simplifier_plugin :time 0.02 :before-memory 2195.58 :after-memory 2195.58) +(test bv_simplifier_plugin :time 0.04 :before-memory 1464.86 :after-memory 1464.86) compare: 0 >> 0 = 0 with #x00000000 0 compare: 0 >> 1 = 0 with #x00000000 @@ -19441,11 +19472,11 @@ compare: -43556211 >> 4251411085 = -1 with #xffffffff -1 PASS -(test bv_simplifier_plugin :time 0.02 :before-memory 2195.58 :after-memory 2195.58) +(test bv_simplifier_plugin :time 0.04 :before-memory 1464.86 :after-memory 1464.86) PASS -(test bit_blaster :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test bit_blaster :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test bit_blaster :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test bit_blaster :time 0.00 :before-memory 1464.86 :after-memory 1464.86) (forall ((y S)) (and (p y (:var 1)) (p (:var 2) (:var 3)))) (forall ((y S)) (and (p y (:var 2)) (p (:var 1) (:var 3)))) (forall ((y S)) (and (p y (:var 2)) (p (:var 1) (:var 3)))) @@ -19453,7 +19484,7 @@ (forall ((y S) (x S)) (and (p x y) (p (:var 3) (:var 2)))) (forall ((y S) (x S)) (and (p x y) (p (:var 3) (:var 2)))) PASS -(test var_subst :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test var_subst :time 0.01 :before-memory 1464.86 :after-memory 1464.86) (forall ((y S)) (and (p y (:var 1)) (p (:var 2) (:var 3)))) (forall ((y S)) (and (p y (:var 2)) (p (:var 1) (:var 3)))) (forall ((y S)) (and (p y (:var 2)) (p (:var 1) (:var 3)))) @@ -19461,23 +19492,23 @@ (forall ((y S) (x S)) (and (p x y) (p (:var 3) (:var 2)))) (forall ((y S) (x S)) (and (p x y) (p (:var 3) (:var 2)))) PASS -(test var_subst :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test var_subst :time 0.01 :before-memory 1464.86 :after-memory 1464.86) ERROR: unexpected character: '255 ÿ'. WARNING: parser error WARNING: parser error WARNING: parser error PASS -(test simple_parser :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test simple_parser :time 0.00 :before-memory 1464.86 :after-memory 1464.86) ERROR: unexpected character: '255 ÿ'. WARNING: parser error WARNING: parser error WARNING: parser error PASS -(test simple_parser :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test simple_parser :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test api :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test api :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test api :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test api :time 0.00 :before-memory 1464.86 :after-memory 1464.86) x: (1, 2), y: (-2, 3), z: (-1, 5) x: (1, 2), y: (-2, 3), z: (-4, 6) [10, 10] @@ -19501,7 +19532,7 @@ [10, 20] / (0, 1] = [10, oo) [5, oo) PASS -(test old_interval :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test old_interval :time 0.00 :before-memory 1464.86 :after-memory 1464.86) x: (1, 2), y: (-2, 3), z: (-1, 5) x: (1, 2), y: (-2, 3), z: (-4, 6) [10, 10] @@ -19525,7 +19556,7 @@ [10, 20] / (0, 1] = [10, oo) [5, oo) PASS -(test old_interval :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test old_interval :time 0.00 :before-memory 1464.86 :after-memory 1464.86) Class a |-> 0 Class b |-> 0 Class c |-> 2 @@ -19547,7 +19578,7 @@ Class (store ((as const (Array Int Int)) 1) 2 b) |-> 3 Class (store (store ((as const (Array Int Int)) 1) 2 b) 1 a) |-> 2 PASS -(test get_implied_equalities :time 0.01 :before-memory 2195.58 :after-memory 2195.58) +(test get_implied_equalities :time 0.02 :before-memory 1464.86 :after-memory 1464.86) Class a |-> 0 Class b |-> 0 Class c |-> 2 @@ -19569,23 +19600,23 @@ Class (store ((as const (Array Int Int)) 1) 2 b) |-> 3 Class (store (store ((as const (Array Int Int)) 1) 2 b) 1 a) |-> 2 PASS -(test get_implied_equalities :time 0.01 :before-memory 2195.58 :after-memory 2195.58) +(test get_implied_equalities :time 0.02 :before-memory 1464.86 :after-memory 1464.86) not solved 1 3 0 0 PASS -(test arith_simplifier_plugin :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test arith_simplifier_plugin :time 0.00 :before-memory 1464.86 :after-memory 1464.86) not solved 1 3 0 0 PASS -(test arith_simplifier_plugin :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test arith_simplifier_plugin :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test matcher :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test matcher :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test matcher :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test matcher :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test object_allocator :time 0.09 :before-memory 2195.58 :after-memory 2195.58) +(test object_allocator :time 0.18 :before-memory 1464.86 :after-memory 1464.86) PASS -(test object_allocator :time 0.10 :before-memory 2195.58 :after-memory 2195.58) +(test object_allocator :time 0.21 :before-memory 1464.86 :after-memory 1464.86) i: 0, a: 1 i: 1, a: 2 i: 2, a: 4 @@ -20058,7 +20089,7 @@ 18446744073709551616 v2: 115792089237316195423570985008687907853269984665640564039457584007913129639936 PASS -(test mpz :time 0.25 :before-memory 2195.58 :after-memory 2195.58) +(test mpz :time 0.71 :before-memory 1464.86 :after-memory 1464.86) i: 0, a: 1 i: 1, a: 2 i: 2, a: 4 @@ -20531,7 +20562,7 @@ 18446744073709551616 v2: 115792089237316195423570985008687907853269984665640564039457584007913129639936 PASS -(test mpz :time 0.26 :before-memory 2195.58 :after-memory 2195.58) +(test mpz :time 0.48 :before-memory 1464.86 :after-memory 1464.86) 1 11/10 1/3 @@ -20542,7 +20573,7 @@ 1/3: 0.3333333333? 1/4: 0.25 PASS -(test mpq :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test mpq :time 0.00 :before-memory 1464.86 :after-memory 1464.86) 1 11/10 1/3 @@ -20553,11 +20584,11 @@ 1/3: 0.3333333333? 1/4: 0.25 PASS -(test mpq :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test mpq :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test mpf :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test mpf :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test mpf :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test mpf :time 0.00 :before-memory 1464.86 :after-memory 1464.86) **************************************************************************************************** 1 3 2 **************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************** @@ -20567,7 +20598,7 @@ **************************************************************************************************** **************************************************************************************************** PASS -(test total_order :time 0.69 :before-memory 2195.58 :after-memory 2195.58) +(test total_order :time 11.04 :before-memory 1464.86 :after-memory 1464.86) **************************************************************************************************** 1 3 2 **************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************************** @@ -20577,39 +20608,39 @@ **************************************************************************************************** **************************************************************************************************** PASS -(test total_order :time 0.69 :before-memory 2195.58 :after-memory 2195.58) +(test total_order :time 27.86 :before-memory 1464.86 :after-memory 1464.86) PASS -(test dl_table :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test dl_table :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test dl_table :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test dl_table :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test dl_context :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test dl_context :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test dl_context :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test dl_context :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test dl_util :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test dl_util :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test dl_util :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test dl_util :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test dl_product_relation :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test dl_product_relation :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test dl_product_relation :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test dl_product_relation :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test dl_relation :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test dl_relation :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test dl_relation :time 0.00 :before-memory 2195.58 :after-memory 2195.58) -max. heap size: 4822.79 Mbytes -max. heap size: 4822.79 Mbytes +(test dl_relation :time 0.00 :before-memory 1464.86 :after-memory 1464.86) +max. heap size: 2630.62 Mbytes +max. heap size: 2630.62 Mbytes PASS -(test parray :time 0.19 :before-memory 2195.58 :after-memory 2195.58) -max. heap size: 4822.79 Mbytes -max. heap size: 4822.79 Mbytes +(test parray :time 5.46 :before-memory 1464.86 :after-memory 1464.86) +max. heap size: 2630.62 Mbytes +max. heap size: 2630.62 Mbytes PASS -(test parray :time 0.19 :before-memory 2195.58 :after-memory 2195.58) +(test parray :time 5.01 :before-memory 1464.86 :after-memory 1464.86) PASS -(test stack :time 0.71 :before-memory 2195.58 :after-memory 2195.58) +(test stack :time 11.18 :before-memory 1464.86 :after-memory 1464.86) PASS -(test stack :time 0.71 :before-memory 2195.58 :after-memory 2195.58) +(test stack :time 2.85 :before-memory 1464.86 :after-memory 1464.86) [\"hello\"\"world\" ] @@ -20636,7 +20667,7 @@ [] [] PASS -(test escaped :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test escaped :time 0.00 :before-memory 1464.86 :after-memory 1464.86) [\"hello\"\"world\" ] @@ -20663,11 +20694,11 @@ [] [] PASS -(test escaped :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test escaped :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test buffer :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test buffer :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test buffer :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test buffer :time 0.00 :before-memory 1464.86 :after-memory 1464.86) 10 20 30 12 10 12 10 13 @@ -20678,7 +20709,7 @@ size: 7 7 size: 669 669 PASS -(test chashtable :time 0.16 :before-memory 2195.58 :after-memory 2195.58) +(test chashtable :time 0.29 :before-memory 1464.86 :after-memory 1464.86) 10 20 30 12 10 12 10 13 @@ -20689,19 +20720,19 @@ size: 4 4 size: 649 649 PASS -(test chashtable :time 0.15 :before-memory 2195.58 :after-memory 2195.58) +(test chashtable :time 0.29 :before-memory 1464.86 :after-memory 1464.86) testing exception Format 12 twelve PASS -(test ex :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test ex :time 0.00 :before-memory 1464.86 :after-memory 1464.86) testing exception Format 12 twelve PASS -(test ex :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test ex :time 0.00 :before-memory 1464.86 :after-memory 1464.86) PASS -(test nlarith_util :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test nlarith_util :time 0.01 :before-memory 1464.86 :after-memory 1464.86) PASS -(test nlarith_util :time 0.00 :before-memory 2195.58 :after-memory 2195.58) +(test nlarith_util :time 0.00 :before-memory 1464.86 :after-memory 1464.86) Using Z3 Version 4.4 (build 1, revision 0) result 1 model : mySet -> (_ as-array k!3) @@ -20724,7 +20755,7 @@ } PASS -(test api_bug :time 0.00 :before-memory 2195.58 :after-memory 2196.06) +(test api_bug :time 0.01 :before-memory 1464.86 :after-memory 1465.33) Using Z3 Version 4.4 (build 1, revision 0) result 1 model : mySet -> (_ as-array k!3) @@ -20747,29 +20778,29 @@ } PASS -(test api_bug :time 0.00 :before-memory 2196.06 :after-memory 2196.53) +(test api_bug :time 0.01 :before-memory 1465.33 :after-memory 1465.81) 0.0 (<= (+ (* (/ 13.0 10.0) x y) (* (/ 23.0 10.0) y y) (* (- 2.0) x)) (/ 11.0 10.0)) (<= (+ (* (/ 13.0 11.0) x y) (* (/ 23.0 11.0) y y) (* (- (/ 20.0 11.0)) x)) 1.0) (= (+ (* 3.0 x x) (* (- 4.0) y)) (- 7.0)) (= (+ (* x x) (* (- (/ 4.0 3.0)) y)) (- (/ 7.0 3.0))) PASS -(test arith_rewriter :time 0.01 :before-memory 2196.53 :after-memory 2196.56) +(test arith_rewriter :time 0.01 :before-memory 1465.81 :after-memory 1465.83) 0.0 (<= (+ (* (/ 13.0 10.0) x y) (* (/ 23.0 10.0) y y) (* (- 2.0) x)) (/ 11.0 10.0)) (<= (+ (* (/ 13.0 11.0) x y) (* (/ 23.0 11.0) y y) (* (- (/ 20.0 11.0)) x)) 1.0) (= (+ (* 3.0 x x) (* (- 4.0) y)) (- 7.0)) (= (+ (* x x) (* (- (/ 4.0 3.0)) y)) (- (/ 7.0 3.0))) PASS -(test arith_rewriter :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test arith_rewriter :time 0.01 :before-memory 1465.83 :after-memory 1465.83) PASS -(test check_assumptions :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test check_assumptions :time 0.00 :before-memory 1465.83 :after-memory 1465.83) PASS -(test check_assumptions :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test check_assumptions :time 0.01 :before-memory 1465.83 :after-memory 1465.83) PASS -(test smt_context :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test smt_context :time 0.00 :before-memory 1465.83 :after-memory 1465.83) PASS -(test smt_context :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test smt_context :time 0.00 :before-memory 1465.83 :after-memory 1465.83) b -> 63 a -> 47 b -> 46 @@ -20777,7 +20808,7 @@ c -> 47 l_false PASS -(test theory_dl :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test theory_dl :time 0.03 :before-memory 1465.83 :after-memory 1465.83) b -> 63 a -> 47 b -> 46 @@ -20785,7 +20816,7 @@ c -> 47 l_false PASS -(test theory_dl :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test theory_dl :time 0.04 :before-memory 1465.83 :after-memory 1465.83) satisfiable a1 -> (_ as-array k!0) k!0 -> { @@ -20923,7 +20954,7 @@ -------------------------- unknown PASS -(test model_retrieval :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test model_retrieval :time 0.01 :before-memory 1465.83 :after-memory 1465.83) satisfiable a1 -> (_ as-array k!0) k!0 -> { @@ -21061,13 +21092,13 @@ -------------------------- unknown PASS -(test model_retrieval :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test model_retrieval :time 0.01 :before-memory 1465.83 :after-memory 1465.83) (<= 0.0 (* 2.0 z z)) -> (or (= 0.0 z) (= 0.0 (- 2.0)) (< (- 2.0) 0.0)) PASS -(test factor_rewriter :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test factor_rewriter :time 0.00 :before-memory 1465.83 :after-memory 1465.83) (<= 0.0 (* 2.0 z z)) -> (or (= 0.0 z) (= 0.0 (- 2.0)) (< (- 2.0) 0.0)) PASS -(test factor_rewriter :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test factor_rewriter :time 0.00 :before-memory 1465.83 :after-memory 1465.83) (declare-datatypes (T) ((list (nil) (cons (car T) (cdr list))))) (declare-const x Int) (declare-const l (list Int)) @@ -21154,7 +21185,7 @@ (bvule x (bvmul y (concat ((_ extract 2 0) x) ((_ extract 3 3) #xf0)))) PASS -(test smt2print_parse :time 0.02 :before-memory 2196.56 :after-memory 2196.56) +(test smt2print_parse :time 0.06 :before-memory 1465.83 :after-memory 1465.83) (declare-datatypes (T) ((list (nil) (cons (car T) (cdr list))))) (declare-const x Int) (declare-const l (list Int)) @@ -21241,15 +21272,15 @@ (bvule x (bvmul y (concat ((_ extract 2 0) x) ((_ extract 3 3) #xf0)))) PASS -(test smt2print_parse :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test smt2print_parse :time 0.04 :before-memory 1465.83 :after-memory 1465.83) VAR 0:0 --> 0 (:var 1) PASS -(test substitution :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test substitution :time 0.00 :before-memory 1465.83 :after-memory 1465.83) VAR 0:0 --> 0 (:var 1) PASS -(test substitution :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test substitution :time 0.00 :before-memory 1465.83 :after-memory 1465.83) --------- p: x0 x1^2 + x0 x1 + x1 + 2 q: x0 x1 + 3 @@ -21289,7 +21320,7 @@ q: x3 x9 + x2 x5 + x4 - x1 S_0: 0 PASS -(test polynomial :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test polynomial :time 0.01 :before-memory 1465.83 :after-memory 1465.83) --------- p: x0 x1^2 + x0 x1 + x1 + 2 q: x0 x1 + 3 @@ -21329,7 +21360,7 @@ q: x3 x9 + x2 x5 + x4 - x1 S_0: 0 PASS -(test polynomial :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test polynomial :time 0.01 :before-memory 1465.83 :after-memory 1465.83) Testing GCD @@ -21672,160 +21703,160 @@ r: 3 x - 2 expected: 3 x - 2 isolating roots of: x^70 - 6 x^65 - x^60 + 60 x^55 - 54 x^50 - 230 x^45 + 274 x^40 + 542 x^35 - 615 x^30 - 1120 x^25 + 1500 x^20 - 160 x^15 - 395 x^10 + 76 x^5 + 34 -(isolate time :time 0.02 :before-memory 2196.71 :after-memory 2196.85) -(sturm time :time 0.00 :before-memory 2196.85 :after-memory 2196.86) +(isolate time :time 0.03 :before-memory 1465.99 :after-memory 1466.13) +(sturm time :time 0.00 :before-memory 1466.13 :after-memory 1466.14) square free part: x^70 - 6 x^65 - x^60 + 60 x^55 - 54 x^50 - 230 x^45 + 274 x^40 + 542 x^35 - 615 x^30 - 1120 x^25 + 1500 x^20 - 160 x^15 - 395 x^10 + 76 x^5 + 34 -(sqf time :time 0.00 :before-memory 2196.86 :after-memory 2196.86) -(fourier time :time 0.00 :before-memory 2196.86 :after-memory 2196.89) +(sqf time :time 0.00 :before-memory 1466.14 :after-memory 1466.14) +(fourier time :time 0.01 :before-memory 1466.14 :after-memory 1466.16) num. roots: 6 sign var(-oo): 16 sign var(+oo): 10 roots: -intervals: (1.25, 1.5) (1.203125, 1.21875) (1.1875, 1.203125) (0, 1) (-0.875, -0.8125) (-0.8125, -0.75)(interval check :time 0.02 :before-memory 2196.89 :after-memory 2197.01) +intervals: (1.25, 1.5) (1.203125, 1.21875) (1.1875, 1.203125) (0, 1) (-0.875, -0.8125) (-0.8125, -0.75)(interval check :time 0.03 :before-memory 1466.16 :after-memory 1466.29) isolating roots of: x^2 - 3 x + 2 -(isolate time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(sturm time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(isolate time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(sturm time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) square free part: x^2 - 3 x + 2 -(sqf time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(fourier time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(sqf time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(fourier time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) num. roots: 2 sign var(-oo): 2 sign var(+oo): 0 roots: 2 -intervals: (0, 2)(interval check :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +intervals: (0, 2)(interval check :time 0.00 :before-memory 1465.89 :after-memory 1465.89) isolating roots of: x^5 - 2 x^4 + x^3 -(isolate time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(sturm time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(isolate time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(sturm time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) square free part: x^2 - x -(sqf time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(fourier time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(sqf time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(fourier time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) num. roots: 2 sign var(-oo): 2 sign var(+oo): 0 roots: 0 -intervals: (0, 4)(interval check :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +intervals: (0, 4)(interval check :time 0.00 :before-memory 1465.89 :after-memory 1465.89) isolating roots of: x^5 - x - 1 -(isolate time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(sturm time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(isolate time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(sturm time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) square free part: x^5 - x - 1 -(sqf time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(fourier time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(sqf time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(fourier time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) num. roots: 1 sign var(-oo): 2 sign var(+oo): 1 roots: -intervals: (0, 4)(interval check :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +intervals: (0, 4)(interval check :time 0.00 :before-memory 1465.89 :after-memory 1465.89) isolating roots of: x^6 - x^5 - 16 x^4 + 10 x^3 + 69 x^2 - 9 x - 54 -(isolate time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(sturm time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(isolate time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(sturm time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) square free part: x^5 + 2 x^4 - 10 x^3 - 20 x^2 + 9 x + 18 -(sqf time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(fourier time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(sqf time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(fourier time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) num. roots: 5 sign var(-oo): 5 sign var(+oo): 0 roots: -2 -intervals: (2, 4) (0, 2) (-4, -2) (-2, 0)(interval check :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +intervals: (2, 4) (0, 2) (-4, -2) (-2, 0)(interval check :time 0.00 :before-memory 1465.91 :after-memory 1465.91) isolating roots of: 100000000 x^2 - 630000 x + 992 -(isolate time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(sturm time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(isolate time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(sturm time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) square free part: 100000000 x^2 - 630000 x + 992 -(sqf time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(fourier time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(sqf time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(fourier time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) num. roots: 2 sign var(-oo): 2 sign var(+oo): 0 roots: -intervals: (0.0031738281?, 0.0034179687?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +intervals: (0.0031738281?, 0.0034179687?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 1465.91 :after-memory 1465.91) isolating roots of: 1000000000000 x^3 - 9600000000 x^2 + 30710000 x - 32736 -(isolate time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(sturm time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(isolate time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(sturm time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) square free part: 1000000000000 x^3 - 9600000000 x^2 + 30710000 x - 32736 -(sqf time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(fourier time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(sqf time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(fourier time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) num. roots: 3 sign var(-oo): 3 sign var(+oo): 0 roots: -intervals: (0.0032958984?, 0.0034179687?) (0.0031738281?, 0.0032958984?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +intervals: (0.0032958984?, 0.0034179687?) (0.0031738281?, 0.0032958984?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 1465.91 :after-memory 1465.91) isolating roots of: 1000 x^11 - 1167 x^10 - 2000 x^6 + 2334 x^5 - 1000 x^3 + 1167 x^2 + 1000 x - 1167 -(isolate time :time 0.00 :before-memory 2196.64 :after-memory 2196.64) -(sturm time :time 0.00 :before-memory 2196.64 :after-memory 2196.74) +(isolate time :time 0.00 :before-memory 1465.92 :after-memory 1465.92) +(sturm time :time 0.00 :before-memory 1465.92 :after-memory 1466.01) square free part: 1000 x^11 - 1167 x^10 - 2000 x^6 + 2334 x^5 - 1000 x^3 + 1167 x^2 + 1000 x - 1167 -(sqf time :time 0.00 :before-memory 2196.74 :after-memory 2196.74) -(fourier time :time 0.00 :before-memory 2196.74 :after-memory 2196.74) +(sqf time :time 0.00 :before-memory 1466.01 :after-memory 1466.01) +(fourier time :time 0.00 :before-memory 1466.01 :after-memory 1466.02) num. roots: 3 sign var(-oo): 6 sign var(+oo): 3 roots: -intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.00 :before-memory 2196.74 :after-memory 2196.76) +intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.00 :before-memory 1466.02 :after-memory 1466.04) isolating roots of: 32768 x^11 - 4160512 x^10 + 174665408 x^9 - 3092100952 x^8 + 24729859214 x^7 - 89699170501 x^6 + 140975222734 x^5 - 87882836696 x^4 + 23405003968 x^3 - 2729126912 x^2 + 132087808 x - 2097152 -(isolate time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) -(sturm time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) +(isolate time :time 0.00 :before-memory 1466.07 :after-memory 1466.08) +(sturm time :time 0.00 :before-memory 1466.08 :after-memory 1466.08) square free part: 32768 x^11 - 4160512 x^10 + 174665408 x^9 - 3092100952 x^8 + 24729859214 x^7 - 89699170501 x^6 + 140975222734 x^5 - 87882836696 x^4 + 23405003968 x^3 - 2729126912 x^2 + 132087808 x - 2097152 -(sqf time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) -(fourier time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) +(sqf time :time 0.00 :before-memory 1466.08 :after-memory 1466.08) +(fourier time :time 0.00 :before-memory 1466.08 :after-memory 1466.08) num. roots: 11 sign var(-oo): 11 sign var(+oo): 0 roots: 64 32 16 8 4 2 0.5 0.25 0.125 0.0625 -intervals: (0, 0.0625)(interval check :time 0.00 :before-memory 2196.80 :after-memory 2196.80) +intervals: (0, 0.0625)(interval check :time 0.00 :before-memory 1466.08 :after-memory 1466.08) isolating roots of: 1000000 x^22 - 2334000 x^21 + 1361889 x^20 - 4000000 x^17 + 9336000 x^16 - 5447556 x^15 - 2000000 x^14 + 4668000 x^13 + 3276222 x^12 - 14004000 x^11 + 8171334 x^10 + 4000000 x^9 - 9336000 x^8 + 1447556 x^7 + 10336000 x^6 - 7781556 x^5 - 638111 x^4 + 4668000 x^3 - 1723778 x^2 - 2334000 x + 1361889 -(isolate time :time 0.00 :before-memory 2196.81 :after-memory 2196.82) -(sturm time :time 0.00 :before-memory 2196.82 :after-memory 2196.83) +(isolate time :time 0.00 :before-memory 1466.09 :after-memory 1466.09) +(sturm time :time 0.00 :before-memory 1466.09 :after-memory 1466.11) square free part: 1000 x^11 - 1167 x^10 - 2000 x^6 + 2334 x^5 - 1000 x^3 + 1167 x^2 + 1000 x - 1167 -(sqf time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) -(fourier time :time 0.00 :before-memory 2196.83 :after-memory 2196.84) +(sqf time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) +(fourier time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) num. roots: 3 sign var(-oo): 6 sign var(+oo): 3 roots: -intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.00 :before-memory 2196.84 :after-memory 2196.84) +intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.00 :before-memory 1466.11 :after-memory 1466.11) isolating roots of: x^17 + 5 x^16 + 3 x^15 + 10 x^13 + 13 x^10 + x^9 + 8 x^5 + 3 x^2 + 7 -(isolate time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) -(sturm time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) +(isolate time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) +(sturm time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) square free part: x^17 + 5 x^16 + 3 x^15 + 10 x^13 + 13 x^10 + x^9 + 8 x^5 + 3 x^2 + 7 -(sqf time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) -(fourier time :time 0.00 :before-memory 2196.83 :after-memory 2196.84) +(sqf time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) +(fourier time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) num. roots: 3 sign var(-oo): 10 sign var(+oo): 7 roots: -intervals: (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 2196.84 :after-memory 2196.84) +intervals: (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 1466.11 :after-memory 1466.11) isolating roots of: x^33 + 5 x^32 + 3 x^31 - 4 x^30 - 12 x^29 - 24 x^28 - 12 x^27 - 5 x^26 + 42 x^25 + 51 x^24 + 18 x^23 + 9 x^22 - 19 x^21 - 10 x^20 - 2 x^19 - 8 x^18 - 5 x^17 - 94 x^16 - 91 x^15 + 22 x^14 + 18 x^13 + 62 x^12 + 62 x^11 + 19 x^10 + 2 x^9 + 10 x^8 + 10 x^7 - 9 x^6 - 64 x^5 - 44 x^4 - 4 x^3 + 40 x^2 + 56 x + 28 -(isolate time :time 0.00 :before-memory 2196.83 :after-memory 2196.84) -(sturm time :time 0.00 :before-memory 2196.84 :after-memory 2196.88) +(isolate time :time 0.01 :before-memory 1466.11 :after-memory 1466.11) +(sturm time :time 0.01 :before-memory 1466.11 :after-memory 1466.16) square free part: x^25 + 5 x^24 + 3 x^23 - 2 x^22 - x^21 - 12 x^20 - 8 x^19 - 8 x^18 + 3 x^17 + 6 x^16 - 20 x^15 + 5 x^14 + 14 x^13 - x^12 + 26 x^11 + 15 x^10 - 6 x^9 - x^8 - 6 x^7 + 13 x^6 - x^5 - 7 x^4 - x^3 + 6 x^2 + 14 x + 14 -(sqf time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) -(fourier time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +(sqf time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) +(fourier time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) num. roots: 5 sign var(-oo): 15 sign var(+oo): 10 roots: -intervals: (1.25, 1.5) (1, 1.25) (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 2196.88 :after-memory 2196.89) +intervals: (1.25, 1.5) (1, 1.25) (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 1466.16 :after-memory 1466.16) isolating roots of: 900 x^19 - 6000113760 x^18 + 10000758403594816 x^17 - 1264023965440000000 x^16 + 39942400000000000000 x^15 - 2700000000000 x^14 + 18000341280000000000 x^13 - 30002275210784448000000000 x^12 + 3792071896320000000000000000 x^11 - 119827200000000000000000000000 x^10 + 2700000000000000000000 x^9 - 18000341280000000000000000000 x^8 + 30002275210784448000000000000000000 x^7 - 3792071896320000000000000000000000000 x^6 + 119827200000000000000000000000000000000 x^5 - 900000000000000000000000000000 x^4 + 6000113760000000000000000000000000000 x^3 - 10000758403594816000000000000000000000000000 x^2 + 1264023965440000000000000000000000000000000000 x - 39942400000000000000000000000000000000000000000 -(isolate time :time 0.00 :before-memory 2196.87 :after-memory 2196.88) -(sturm time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +(isolate time :time 0.01 :before-memory 1466.15 :after-memory 1466.16) +(sturm time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) square free part: 15 x^7 - 50000948 x^6 + 3160000000 x^5 - 15000000000 x^2 + 50000948000000000 x - 3160000000000000000 -(sqf time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) -(fourier time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +(sqf time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) +(fourier time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) num. roots: 3 sign var(-oo): 5 sign var(+oo): 2 roots: -intervals: (2097152, 4194304) (63.125, 63.25) (63, 63.125)(interval check :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +intervals: (2097152, 4194304) (63.125, 63.25) (63, 63.125)(interval check :time 0.00 :before-memory 1466.16 :after-memory 1466.16) upolynomial sturm seq... x^16 - 136 x^14 + 6476 x^12 - 141912 x^10 + 1513334 x^8 - 7453176 x^6 + 13950764 x^4 - 5596840 x^2 + 46225 @@ -21937,148 +21968,148 @@ _r: 16 x^2 - 40 x - 24 _q: 16 x^2 - 40 x - 24 isolating roots of: x^2 - 3 x + 2 -(isolate time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(sturm time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(isolate time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(sturm time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) square free part: x^2 - 3 x + 2 -(sqf time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(fourier time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(sqf time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(fourier time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) num. roots: 2 sign var(-oo): 2 sign var(+oo): 0 roots: 2 -intervals: (0, 2)(interval check :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +intervals: (0, 2)(interval check :time 0.00 :before-memory 1465.89 :after-memory 1465.89) isolating roots of: x^5 - 2 x^4 + x^3 -(isolate time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(sturm time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(isolate time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(sturm time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) square free part: x^2 - x -(sqf time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(fourier time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(sqf time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(fourier time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) num. roots: 2 sign var(-oo): 2 sign var(+oo): 0 roots: 0 -intervals: (0, 4)(interval check :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +intervals: (0, 4)(interval check :time 0.00 :before-memory 1465.89 :after-memory 1465.89) isolating roots of: x^5 - x - 1 -(isolate time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(sturm time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(isolate time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(sturm time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) square free part: x^5 - x - 1 -(sqf time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(fourier time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(sqf time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(fourier time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) num. roots: 1 sign var(-oo): 2 sign var(+oo): 1 roots: -intervals: (0, 4)(interval check :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +intervals: (0, 4)(interval check :time 0.00 :before-memory 1465.89 :after-memory 1465.89) isolating roots of: x^6 - x^5 - 16 x^4 + 10 x^3 + 69 x^2 - 9 x - 54 -(isolate time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(sturm time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(isolate time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(sturm time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) square free part: x^5 + 2 x^4 - 10 x^3 - 20 x^2 + 9 x + 18 -(sqf time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(fourier time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(sqf time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(fourier time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) num. roots: 5 sign var(-oo): 5 sign var(+oo): 0 roots: -2 -intervals: (2, 4) (0, 2) (-4, -2) (-2, 0)(interval check :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +intervals: (2, 4) (0, 2) (-4, -2) (-2, 0)(interval check :time 0.00 :before-memory 1465.91 :after-memory 1465.91) isolating roots of: 100000000 x^2 - 630000 x + 992 -(isolate time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(sturm time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(isolate time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(sturm time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) square free part: 100000000 x^2 - 630000 x + 992 -(sqf time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(fourier time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(sqf time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(fourier time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) num. roots: 2 sign var(-oo): 2 sign var(+oo): 0 roots: -intervals: (0.0031738281?, 0.0034179687?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +intervals: (0.0031738281?, 0.0034179687?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 1465.91 :after-memory 1465.91) isolating roots of: 1000000000000 x^3 - 9600000000 x^2 + 30710000 x - 32736 -(isolate time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(sturm time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(isolate time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(sturm time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) square free part: 1000000000000 x^3 - 9600000000 x^2 + 30710000 x - 32736 -(sqf time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(fourier time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(sqf time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(fourier time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) num. roots: 3 sign var(-oo): 3 sign var(+oo): 0 roots: -intervals: (0.0032958984?, 0.0034179687?) (0.0031738281?, 0.0032958984?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +intervals: (0.0032958984?, 0.0034179687?) (0.0031738281?, 0.0032958984?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 1465.91 :after-memory 1465.91) isolating roots of: 1000 x^11 - 1167 x^10 - 2000 x^6 + 2334 x^5 - 1000 x^3 + 1167 x^2 + 1000 x - 1167 -(isolate time :time 0.00 :before-memory 2196.64 :after-memory 2196.64) -(sturm time :time 0.00 :before-memory 2196.64 :after-memory 2196.74) +(isolate time :time 0.00 :before-memory 1465.92 :after-memory 1465.92) +(sturm time :time 0.00 :before-memory 1465.92 :after-memory 1466.01) square free part: 1000 x^11 - 1167 x^10 - 2000 x^6 + 2334 x^5 - 1000 x^3 + 1167 x^2 + 1000 x - 1167 -(sqf time :time 0.00 :before-memory 2196.74 :after-memory 2196.74) -(fourier time :time 0.00 :before-memory 2196.74 :after-memory 2196.74) +(sqf time :time 0.00 :before-memory 1466.01 :after-memory 1466.01) +(fourier time :time 0.00 :before-memory 1466.01 :after-memory 1466.02) num. roots: 3 sign var(-oo): 6 sign var(+oo): 3 roots: -intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.00 :before-memory 2196.74 :after-memory 2196.76) +intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.00 :before-memory 1466.02 :after-memory 1466.04) isolating roots of: 32768 x^11 - 4160512 x^10 + 174665408 x^9 - 3092100952 x^8 + 24729859214 x^7 - 89699170501 x^6 + 140975222734 x^5 - 87882836696 x^4 + 23405003968 x^3 - 2729126912 x^2 + 132087808 x - 2097152 -(isolate time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) -(sturm time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) +(isolate time :time 0.00 :before-memory 1466.07 :after-memory 1466.08) +(sturm time :time 0.00 :before-memory 1466.08 :after-memory 1466.08) square free part: 32768 x^11 - 4160512 x^10 + 174665408 x^9 - 3092100952 x^8 + 24729859214 x^7 - 89699170501 x^6 + 140975222734 x^5 - 87882836696 x^4 + 23405003968 x^3 - 2729126912 x^2 + 132087808 x - 2097152 -(sqf time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) -(fourier time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) +(sqf time :time 0.00 :before-memory 1466.08 :after-memory 1466.08) +(fourier time :time 0.00 :before-memory 1466.08 :after-memory 1466.08) num. roots: 11 sign var(-oo): 11 sign var(+oo): 0 roots: 64 32 16 8 4 2 0.5 0.25 0.125 0.0625 -intervals: (0, 0.0625)(interval check :time 0.00 :before-memory 2196.80 :after-memory 2196.80) +intervals: (0, 0.0625)(interval check :time 0.00 :before-memory 1466.08 :after-memory 1466.08) isolating roots of: 1000000 x^22 - 2334000 x^21 + 1361889 x^20 - 4000000 x^17 + 9336000 x^16 - 5447556 x^15 - 2000000 x^14 + 4668000 x^13 + 3276222 x^12 - 14004000 x^11 + 8171334 x^10 + 4000000 x^9 - 9336000 x^8 + 1447556 x^7 + 10336000 x^6 - 7781556 x^5 - 638111 x^4 + 4668000 x^3 - 1723778 x^2 - 2334000 x + 1361889 -(isolate time :time 0.00 :before-memory 2196.81 :after-memory 2196.82) -(sturm time :time 0.00 :before-memory 2196.82 :after-memory 2196.83) +(isolate time :time 0.00 :before-memory 1466.09 :after-memory 1466.09) +(sturm time :time 0.00 :before-memory 1466.09 :after-memory 1466.11) square free part: 1000 x^11 - 1167 x^10 - 2000 x^6 + 2334 x^5 - 1000 x^3 + 1167 x^2 + 1000 x - 1167 -(sqf time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) -(fourier time :time 0.00 :before-memory 2196.83 :after-memory 2196.84) +(sqf time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) +(fourier time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) num. roots: 3 sign var(-oo): 6 sign var(+oo): 3 roots: -intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.00 :before-memory 2196.84 :after-memory 2196.84) +intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.00 :before-memory 1466.11 :after-memory 1466.11) isolating roots of: x^17 + 5 x^16 + 3 x^15 + 10 x^13 + 13 x^10 + x^9 + 8 x^5 + 3 x^2 + 7 -(isolate time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) -(sturm time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) +(isolate time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) +(sturm time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) square free part: x^17 + 5 x^16 + 3 x^15 + 10 x^13 + 13 x^10 + x^9 + 8 x^5 + 3 x^2 + 7 -(sqf time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) -(fourier time :time 0.00 :before-memory 2196.83 :after-memory 2196.84) +(sqf time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) +(fourier time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) num. roots: 3 sign var(-oo): 10 sign var(+oo): 7 roots: -intervals: (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 2196.84 :after-memory 2196.84) +intervals: (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 1466.11 :after-memory 1466.11) isolating roots of: x^33 + 5 x^32 + 3 x^31 - 4 x^30 - 12 x^29 - 24 x^28 - 12 x^27 - 5 x^26 + 42 x^25 + 51 x^24 + 18 x^23 + 9 x^22 - 19 x^21 - 10 x^20 - 2 x^19 - 8 x^18 - 5 x^17 - 94 x^16 - 91 x^15 + 22 x^14 + 18 x^13 + 62 x^12 + 62 x^11 + 19 x^10 + 2 x^9 + 10 x^8 + 10 x^7 - 9 x^6 - 64 x^5 - 44 x^4 - 4 x^3 + 40 x^2 + 56 x + 28 -(isolate time :time 0.00 :before-memory 2196.83 :after-memory 2196.84) -(sturm time :time 0.00 :before-memory 2196.84 :after-memory 2196.88) +(isolate time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) +(sturm time :time 0.01 :before-memory 1466.11 :after-memory 1466.16) square free part: x^25 + 5 x^24 + 3 x^23 - 2 x^22 - x^21 - 12 x^20 - 8 x^19 - 8 x^18 + 3 x^17 + 6 x^16 - 20 x^15 + 5 x^14 + 14 x^13 - x^12 + 26 x^11 + 15 x^10 - 6 x^9 - x^8 - 6 x^7 + 13 x^6 - x^5 - 7 x^4 - x^3 + 6 x^2 + 14 x + 14 -(sqf time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) -(fourier time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +(sqf time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) +(fourier time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) num. roots: 5 sign var(-oo): 15 sign var(+oo): 10 roots: -intervals: (1.25, 1.5) (1, 1.25) (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 2196.88 :after-memory 2196.89) +intervals: (1.25, 1.5) (1, 1.25) (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 1466.16 :after-memory 1466.16) isolating roots of: 900 x^19 - 6000113760 x^18 + 10000758403594816 x^17 - 1264023965440000000 x^16 + 39942400000000000000 x^15 - 2700000000000 x^14 + 18000341280000000000 x^13 - 30002275210784448000000000 x^12 + 3792071896320000000000000000 x^11 - 119827200000000000000000000000 x^10 + 2700000000000000000000 x^9 - 18000341280000000000000000000 x^8 + 30002275210784448000000000000000000 x^7 - 3792071896320000000000000000000000000 x^6 + 119827200000000000000000000000000000000 x^5 - 900000000000000000000000000000 x^4 + 6000113760000000000000000000000000000 x^3 - 10000758403594816000000000000000000000000000 x^2 + 1264023965440000000000000000000000000000000000 x - 39942400000000000000000000000000000000000000000 -(isolate time :time 0.00 :before-memory 2196.87 :after-memory 2196.88) -(sturm time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +(isolate time :time 0.01 :before-memory 1466.15 :after-memory 1466.16) +(sturm time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) square free part: 15 x^7 - 50000948 x^6 + 3160000000 x^5 - 15000000000 x^2 + 50000948000000000 x - 3160000000000000000 -(sqf time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) -(fourier time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +(sqf time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) +(fourier time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) num. roots: 3 sign var(-oo): 5 sign var(+oo): 2 roots: -intervals: (2097152, 4194304) (63.125, 63.25) (63, 63.125)(interval check :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +intervals: (2097152, 4194304) (63.125, 63.25) (63, 63.125)(interval check :time 0.00 :before-memory 1466.16 :after-memory 1466.16) p: x0^5 + 2 x0^4 - 10 x0^3 - 20 x0^2 + 9 x0 + 18 q: x^5 + 2 x^4 - 10 x^3 - 20 x^2 + 9 x + 18 @@ -22138,7 +22169,7 @@ V: 3 x^2 - x - 3 D: 1 PASS -(test upolynomial :time 1.73 :before-memory 2196.56 :after-memory 2196.56) +(test upolynomial :time 4.16 :before-memory 1465.83 :after-memory 1465.83) Testing GCD @@ -22481,160 +22512,160 @@ r: 3 x - 2 expected: 3 x - 2 isolating roots of: x^70 - 6 x^65 - x^60 + 60 x^55 - 54 x^50 - 230 x^45 + 274 x^40 + 542 x^35 - 615 x^30 - 1120 x^25 + 1500 x^20 - 160 x^15 - 395 x^10 + 76 x^5 + 34 -(isolate time :time 0.02 :before-memory 2196.71 :after-memory 2196.85) -(sturm time :time 0.00 :before-memory 2196.85 :after-memory 2196.86) +(isolate time :time 0.05 :before-memory 1465.99 :after-memory 1466.13) +(sturm time :time 0.01 :before-memory 1466.13 :after-memory 1466.14) square free part: x^70 - 6 x^65 - x^60 + 60 x^55 - 54 x^50 - 230 x^45 + 274 x^40 + 542 x^35 - 615 x^30 - 1120 x^25 + 1500 x^20 - 160 x^15 - 395 x^10 + 76 x^5 + 34 -(sqf time :time 0.00 :before-memory 2196.86 :after-memory 2196.86) -(fourier time :time 0.00 :before-memory 2196.86 :after-memory 2196.89) +(sqf time :time 0.00 :before-memory 1466.14 :after-memory 1466.14) +(fourier time :time 0.01 :before-memory 1466.14 :after-memory 1466.16) num. roots: 6 sign var(-oo): 16 sign var(+oo): 10 roots: -intervals: (1.25, 1.5) (1.203125, 1.21875) (1.1875, 1.203125) (0, 1) (-0.875, -0.8125) (-0.8125, -0.75)(interval check :time 0.02 :before-memory 2196.89 :after-memory 2197.01) +intervals: (1.25, 1.5) (1.203125, 1.21875) (1.1875, 1.203125) (0, 1) (-0.875, -0.8125) (-0.8125, -0.75)(interval check :time 0.03 :before-memory 1466.16 :after-memory 1466.29) isolating roots of: x^2 - 3 x + 2 -(isolate time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(sturm time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(isolate time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(sturm time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) square free part: x^2 - 3 x + 2 -(sqf time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(fourier time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(sqf time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(fourier time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) num. roots: 2 sign var(-oo): 2 sign var(+oo): 0 roots: 2 -intervals: (0, 2)(interval check :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +intervals: (0, 2)(interval check :time 0.00 :before-memory 1465.89 :after-memory 1465.89) isolating roots of: x^5 - 2 x^4 + x^3 -(isolate time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(sturm time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(isolate time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(sturm time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) square free part: x^2 - x -(sqf time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(fourier time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(sqf time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(fourier time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) num. roots: 2 sign var(-oo): 2 sign var(+oo): 0 roots: 0 -intervals: (0, 4)(interval check :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +intervals: (0, 4)(interval check :time 0.00 :before-memory 1465.89 :after-memory 1465.89) isolating roots of: x^5 - x - 1 -(isolate time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(sturm time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(isolate time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(sturm time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) square free part: x^5 - x - 1 -(sqf time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(fourier time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(sqf time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(fourier time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) num. roots: 1 sign var(-oo): 2 sign var(+oo): 1 roots: -intervals: (0, 4)(interval check :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +intervals: (0, 4)(interval check :time 0.00 :before-memory 1465.89 :after-memory 1465.89) isolating roots of: x^6 - x^5 - 16 x^4 + 10 x^3 + 69 x^2 - 9 x - 54 -(isolate time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(sturm time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(isolate time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(sturm time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) square free part: x^5 + 2 x^4 - 10 x^3 - 20 x^2 + 9 x + 18 -(sqf time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(fourier time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(sqf time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(fourier time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) num. roots: 5 sign var(-oo): 5 sign var(+oo): 0 roots: -2 -intervals: (2, 4) (0, 2) (-4, -2) (-2, 0)(interval check :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +intervals: (2, 4) (0, 2) (-4, -2) (-2, 0)(interval check :time 0.00 :before-memory 1465.91 :after-memory 1465.91) isolating roots of: 100000000 x^2 - 630000 x + 992 -(isolate time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(sturm time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(isolate time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(sturm time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) square free part: 100000000 x^2 - 630000 x + 992 -(sqf time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(fourier time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(sqf time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(fourier time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) num. roots: 2 sign var(-oo): 2 sign var(+oo): 0 roots: -intervals: (0.0031738281?, 0.0034179687?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +intervals: (0.0031738281?, 0.0034179687?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 1465.91 :after-memory 1465.91) isolating roots of: 1000000000000 x^3 - 9600000000 x^2 + 30710000 x - 32736 -(isolate time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(sturm time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(isolate time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(sturm time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) square free part: 1000000000000 x^3 - 9600000000 x^2 + 30710000 x - 32736 -(sqf time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(fourier time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(sqf time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(fourier time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) num. roots: 3 sign var(-oo): 3 sign var(+oo): 0 roots: -intervals: (0.0032958984?, 0.0034179687?) (0.0031738281?, 0.0032958984?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +intervals: (0.0032958984?, 0.0034179687?) (0.0031738281?, 0.0032958984?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 1465.91 :after-memory 1465.91) isolating roots of: 1000 x^11 - 1167 x^10 - 2000 x^6 + 2334 x^5 - 1000 x^3 + 1167 x^2 + 1000 x - 1167 -(isolate time :time 0.00 :before-memory 2196.64 :after-memory 2196.64) -(sturm time :time 0.00 :before-memory 2196.64 :after-memory 2196.74) +(isolate time :time 0.01 :before-memory 1465.92 :after-memory 1465.92) +(sturm time :time 0.00 :before-memory 1465.92 :after-memory 1466.01) square free part: 1000 x^11 - 1167 x^10 - 2000 x^6 + 2334 x^5 - 1000 x^3 + 1167 x^2 + 1000 x - 1167 -(sqf time :time 0.00 :before-memory 2196.74 :after-memory 2196.74) -(fourier time :time 0.00 :before-memory 2196.74 :after-memory 2196.74) +(sqf time :time 0.00 :before-memory 1466.01 :after-memory 1466.01) +(fourier time :time 0.00 :before-memory 1466.01 :after-memory 1466.02) num. roots: 3 sign var(-oo): 6 sign var(+oo): 3 roots: -intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.00 :before-memory 2196.74 :after-memory 2196.76) +intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.00 :before-memory 1466.02 :after-memory 1466.04) isolating roots of: 32768 x^11 - 4160512 x^10 + 174665408 x^9 - 3092100952 x^8 + 24729859214 x^7 - 89699170501 x^6 + 140975222734 x^5 - 87882836696 x^4 + 23405003968 x^3 - 2729126912 x^2 + 132087808 x - 2097152 -(isolate time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) -(sturm time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) +(isolate time :time 0.00 :before-memory 1466.07 :after-memory 1466.08) +(sturm time :time 0.00 :before-memory 1466.08 :after-memory 1466.08) square free part: 32768 x^11 - 4160512 x^10 + 174665408 x^9 - 3092100952 x^8 + 24729859214 x^7 - 89699170501 x^6 + 140975222734 x^5 - 87882836696 x^4 + 23405003968 x^3 - 2729126912 x^2 + 132087808 x - 2097152 -(sqf time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) -(fourier time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) +(sqf time :time 0.00 :before-memory 1466.08 :after-memory 1466.08) +(fourier time :time 0.00 :before-memory 1466.08 :after-memory 1466.08) num. roots: 11 sign var(-oo): 11 sign var(+oo): 0 roots: 64 32 16 8 4 2 0.5 0.25 0.125 0.0625 -intervals: (0, 0.0625)(interval check :time 0.00 :before-memory 2196.80 :after-memory 2196.80) +intervals: (0, 0.0625)(interval check :time 0.00 :before-memory 1466.08 :after-memory 1466.08) isolating roots of: 1000000 x^22 - 2334000 x^21 + 1361889 x^20 - 4000000 x^17 + 9336000 x^16 - 5447556 x^15 - 2000000 x^14 + 4668000 x^13 + 3276222 x^12 - 14004000 x^11 + 8171334 x^10 + 4000000 x^9 - 9336000 x^8 + 1447556 x^7 + 10336000 x^6 - 7781556 x^5 - 638111 x^4 + 4668000 x^3 - 1723778 x^2 - 2334000 x + 1361889 -(isolate time :time 0.00 :before-memory 2196.81 :after-memory 2196.82) -(sturm time :time 0.00 :before-memory 2196.82 :after-memory 2196.83) +(isolate time :time 0.01 :before-memory 1466.09 :after-memory 1466.09) +(sturm time :time 0.01 :before-memory 1466.09 :after-memory 1466.11) square free part: 1000 x^11 - 1167 x^10 - 2000 x^6 + 2334 x^5 - 1000 x^3 + 1167 x^2 + 1000 x - 1167 -(sqf time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) -(fourier time :time 0.00 :before-memory 2196.83 :after-memory 2196.84) +(sqf time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) +(fourier time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) num. roots: 3 sign var(-oo): 6 sign var(+oo): 3 roots: -intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.00 :before-memory 2196.84 :after-memory 2196.84) +intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.00 :before-memory 1466.11 :after-memory 1466.11) isolating roots of: x^17 + 5 x^16 + 3 x^15 + 10 x^13 + 13 x^10 + x^9 + 8 x^5 + 3 x^2 + 7 -(isolate time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) -(sturm time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) +(isolate time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) +(sturm time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) square free part: x^17 + 5 x^16 + 3 x^15 + 10 x^13 + 13 x^10 + x^9 + 8 x^5 + 3 x^2 + 7 -(sqf time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) -(fourier time :time 0.00 :before-memory 2196.83 :after-memory 2196.84) +(sqf time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) +(fourier time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) num. roots: 3 sign var(-oo): 10 sign var(+oo): 7 roots: -intervals: (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 2196.84 :after-memory 2196.84) +intervals: (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 1466.11 :after-memory 1466.11) isolating roots of: x^33 + 5 x^32 + 3 x^31 - 4 x^30 - 12 x^29 - 24 x^28 - 12 x^27 - 5 x^26 + 42 x^25 + 51 x^24 + 18 x^23 + 9 x^22 - 19 x^21 - 10 x^20 - 2 x^19 - 8 x^18 - 5 x^17 - 94 x^16 - 91 x^15 + 22 x^14 + 18 x^13 + 62 x^12 + 62 x^11 + 19 x^10 + 2 x^9 + 10 x^8 + 10 x^7 - 9 x^6 - 64 x^5 - 44 x^4 - 4 x^3 + 40 x^2 + 56 x + 28 -(isolate time :time 0.00 :before-memory 2196.83 :after-memory 2196.84) -(sturm time :time 0.00 :before-memory 2196.84 :after-memory 2196.88) +(isolate time :time 0.01 :before-memory 1466.11 :after-memory 1466.11) +(sturm time :time 0.02 :before-memory 1466.11 :after-memory 1466.16) square free part: x^25 + 5 x^24 + 3 x^23 - 2 x^22 - x^21 - 12 x^20 - 8 x^19 - 8 x^18 + 3 x^17 + 6 x^16 - 20 x^15 + 5 x^14 + 14 x^13 - x^12 + 26 x^11 + 15 x^10 - 6 x^9 - x^8 - 6 x^7 + 13 x^6 - x^5 - 7 x^4 - x^3 + 6 x^2 + 14 x + 14 -(sqf time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) -(fourier time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +(sqf time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) +(fourier time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) num. roots: 5 sign var(-oo): 15 sign var(+oo): 10 roots: -intervals: (1.25, 1.5) (1, 1.25) (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 2196.88 :after-memory 2196.89) +intervals: (1.25, 1.5) (1, 1.25) (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 1466.16 :after-memory 1466.16) isolating roots of: 900 x^19 - 6000113760 x^18 + 10000758403594816 x^17 - 1264023965440000000 x^16 + 39942400000000000000 x^15 - 2700000000000 x^14 + 18000341280000000000 x^13 - 30002275210784448000000000 x^12 + 3792071896320000000000000000 x^11 - 119827200000000000000000000000 x^10 + 2700000000000000000000 x^9 - 18000341280000000000000000000 x^8 + 30002275210784448000000000000000000 x^7 - 3792071896320000000000000000000000000 x^6 + 119827200000000000000000000000000000000 x^5 - 900000000000000000000000000000 x^4 + 6000113760000000000000000000000000000 x^3 - 10000758403594816000000000000000000000000000 x^2 + 1264023965440000000000000000000000000000000000 x - 39942400000000000000000000000000000000000000000 -(isolate time :time 0.00 :before-memory 2196.87 :after-memory 2196.88) -(sturm time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +(isolate time :time 0.02 :before-memory 1466.15 :after-memory 1466.16) +(sturm time :time 0.01 :before-memory 1466.16 :after-memory 1466.16) square free part: 15 x^7 - 50000948 x^6 + 3160000000 x^5 - 15000000000 x^2 + 50000948000000000 x - 3160000000000000000 -(sqf time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) -(fourier time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +(sqf time :time 0.01 :before-memory 1466.16 :after-memory 1466.16) +(fourier time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) num. roots: 3 sign var(-oo): 5 sign var(+oo): 2 roots: -intervals: (2097152, 4194304) (63.125, 63.25) (63, 63.125)(interval check :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +intervals: (2097152, 4194304) (63.125, 63.25) (63, 63.125)(interval check :time 0.00 :before-memory 1466.16 :after-memory 1466.16) upolynomial sturm seq... x^16 - 136 x^14 + 6476 x^12 - 141912 x^10 + 1513334 x^8 - 7453176 x^6 + 13950764 x^4 - 5596840 x^2 + 46225 @@ -22746,148 +22777,148 @@ _r: 16 x^2 - 40 x - 24 _q: 16 x^2 - 40 x - 24 isolating roots of: x^2 - 3 x + 2 -(isolate time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(sturm time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(isolate time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(sturm time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) square free part: x^2 - 3 x + 2 -(sqf time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(fourier time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(sqf time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(fourier time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) num. roots: 2 sign var(-oo): 2 sign var(+oo): 0 roots: 2 -intervals: (0, 2)(interval check :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +intervals: (0, 2)(interval check :time 0.00 :before-memory 1465.89 :after-memory 1465.89) isolating roots of: x^5 - 2 x^4 + x^3 -(isolate time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(sturm time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(isolate time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(sturm time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) square free part: x^2 - x -(sqf time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(fourier time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(sqf time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(fourier time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) num. roots: 2 sign var(-oo): 2 sign var(+oo): 0 roots: 0 -intervals: (0, 4)(interval check :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +intervals: (0, 4)(interval check :time 0.00 :before-memory 1465.89 :after-memory 1465.89) isolating roots of: x^5 - x - 1 -(isolate time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(sturm time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(isolate time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(sturm time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) square free part: x^5 - x - 1 -(sqf time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) -(fourier time :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +(sqf time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) +(fourier time :time 0.00 :before-memory 1465.89 :after-memory 1465.89) num. roots: 1 sign var(-oo): 2 sign var(+oo): 1 roots: -intervals: (0, 4)(interval check :time 0.00 :before-memory 2196.61 :after-memory 2196.61) +intervals: (0, 4)(interval check :time 0.00 :before-memory 1465.89 :after-memory 1465.89) isolating roots of: x^6 - x^5 - 16 x^4 + 10 x^3 + 69 x^2 - 9 x - 54 -(isolate time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(sturm time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(isolate time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(sturm time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) square free part: x^5 + 2 x^4 - 10 x^3 - 20 x^2 + 9 x + 18 -(sqf time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(fourier time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(sqf time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(fourier time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) num. roots: 5 sign var(-oo): 5 sign var(+oo): 0 roots: -2 -intervals: (2, 4) (0, 2) (-4, -2) (-2, 0)(interval check :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +intervals: (2, 4) (0, 2) (-4, -2) (-2, 0)(interval check :time 0.00 :before-memory 1465.91 :after-memory 1465.91) isolating roots of: 100000000 x^2 - 630000 x + 992 -(isolate time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(sturm time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(isolate time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(sturm time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) square free part: 100000000 x^2 - 630000 x + 992 -(sqf time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(fourier time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(sqf time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(fourier time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) num. roots: 2 sign var(-oo): 2 sign var(+oo): 0 roots: -intervals: (0.0031738281?, 0.0034179687?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +intervals: (0.0031738281?, 0.0034179687?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 1465.91 :after-memory 1465.91) isolating roots of: 1000000000000 x^3 - 9600000000 x^2 + 30710000 x - 32736 -(isolate time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(sturm time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(isolate time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(sturm time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) square free part: 1000000000000 x^3 - 9600000000 x^2 + 30710000 x - 32736 -(sqf time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) -(fourier time :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +(sqf time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) +(fourier time :time 0.00 :before-memory 1465.91 :after-memory 1465.91) num. roots: 3 sign var(-oo): 3 sign var(+oo): 0 roots: -intervals: (0.0032958984?, 0.0034179687?) (0.0031738281?, 0.0032958984?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 2196.63 :after-memory 2196.63) +intervals: (0.0032958984?, 0.0034179687?) (0.0031738281?, 0.0032958984?) (0.0029296875, 0.0031738281?)(interval check :time 0.00 :before-memory 1465.91 :after-memory 1465.91) isolating roots of: 1000 x^11 - 1167 x^10 - 2000 x^6 + 2334 x^5 - 1000 x^3 + 1167 x^2 + 1000 x - 1167 -(isolate time :time 0.00 :before-memory 2196.64 :after-memory 2196.64) -(sturm time :time 0.00 :before-memory 2196.64 :after-memory 2196.74) +(isolate time :time 0.00 :before-memory 1465.92 :after-memory 1465.92) +(sturm time :time 0.00 :before-memory 1465.92 :after-memory 1466.01) square free part: 1000 x^11 - 1167 x^10 - 2000 x^6 + 2334 x^5 - 1000 x^3 + 1167 x^2 + 1000 x - 1167 -(sqf time :time 0.00 :before-memory 2196.74 :after-memory 2196.74) -(fourier time :time 0.00 :before-memory 2196.74 :after-memory 2196.74) +(sqf time :time 0.00 :before-memory 1466.01 :after-memory 1466.01) +(fourier time :time 0.00 :before-memory 1466.01 :after-memory 1466.02) num. roots: 3 sign var(-oo): 6 sign var(+oo): 3 roots: -intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.00 :before-memory 2196.74 :after-memory 2196.76) +intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.01 :before-memory 1466.02 :after-memory 1466.04) isolating roots of: 32768 x^11 - 4160512 x^10 + 174665408 x^9 - 3092100952 x^8 + 24729859214 x^7 - 89699170501 x^6 + 140975222734 x^5 - 87882836696 x^4 + 23405003968 x^3 - 2729126912 x^2 + 132087808 x - 2097152 -(isolate time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) -(sturm time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) +(isolate time :time 0.01 :before-memory 1466.07 :after-memory 1466.08) +(sturm time :time 0.00 :before-memory 1466.08 :after-memory 1466.08) square free part: 32768 x^11 - 4160512 x^10 + 174665408 x^9 - 3092100952 x^8 + 24729859214 x^7 - 89699170501 x^6 + 140975222734 x^5 - 87882836696 x^4 + 23405003968 x^3 - 2729126912 x^2 + 132087808 x - 2097152 -(sqf time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) -(fourier time :time 0.00 :before-memory 2196.80 :after-memory 2196.80) +(sqf time :time 0.00 :before-memory 1466.08 :after-memory 1466.08) +(fourier time :time 0.00 :before-memory 1466.08 :after-memory 1466.08) num. roots: 11 sign var(-oo): 11 sign var(+oo): 0 roots: 64 32 16 8 4 2 0.5 0.25 0.125 0.0625 -intervals: (0, 0.0625)(interval check :time 0.00 :before-memory 2196.80 :after-memory 2196.80) +intervals: (0, 0.0625)(interval check :time 0.00 :before-memory 1466.08 :after-memory 1466.08) isolating roots of: 1000000 x^22 - 2334000 x^21 + 1361889 x^20 - 4000000 x^17 + 9336000 x^16 - 5447556 x^15 - 2000000 x^14 + 4668000 x^13 + 3276222 x^12 - 14004000 x^11 + 8171334 x^10 + 4000000 x^9 - 9336000 x^8 + 1447556 x^7 + 10336000 x^6 - 7781556 x^5 - 638111 x^4 + 4668000 x^3 - 1723778 x^2 - 2334000 x + 1361889 -(isolate time :time 0.00 :before-memory 2196.81 :after-memory 2196.82) -(sturm time :time 0.00 :before-memory 2196.82 :after-memory 2196.83) +(isolate time :time 0.01 :before-memory 1466.09 :after-memory 1466.09) +(sturm time :time 0.01 :before-memory 1466.09 :after-memory 1466.11) square free part: 1000 x^11 - 1167 x^10 - 2000 x^6 + 2334 x^5 - 1000 x^3 + 1167 x^2 + 1000 x - 1167 -(sqf time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) -(fourier time :time 0.00 :before-memory 2196.83 :after-memory 2196.84) +(sqf time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) +(fourier time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) num. roots: 3 sign var(-oo): 6 sign var(+oo): 3 roots: -intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.00 :before-memory 2196.84 :after-memory 2196.84) +intervals: (1.1672363281?, 1.1674804687?) (1.1669921875, 1.1672363281?) (0, 1)(interval check :time 0.00 :before-memory 1466.11 :after-memory 1466.11) isolating roots of: x^17 + 5 x^16 + 3 x^15 + 10 x^13 + 13 x^10 + x^9 + 8 x^5 + 3 x^2 + 7 -(isolate time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) -(sturm time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) +(isolate time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) +(sturm time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) square free part: x^17 + 5 x^16 + 3 x^15 + 10 x^13 + 13 x^10 + x^9 + 8 x^5 + 3 x^2 + 7 -(sqf time :time 0.00 :before-memory 2196.83 :after-memory 2196.83) -(fourier time :time 0.00 :before-memory 2196.83 :after-memory 2196.84) +(sqf time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) +(fourier time :time 0.00 :before-memory 1466.11 :after-memory 1466.11) num. roots: 3 sign var(-oo): 10 sign var(+oo): 7 roots: -intervals: (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 2196.84 :after-memory 2196.84) +intervals: (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 1466.11 :after-memory 1466.11) isolating roots of: x^33 + 5 x^32 + 3 x^31 - 4 x^30 - 12 x^29 - 24 x^28 - 12 x^27 - 5 x^26 + 42 x^25 + 51 x^24 + 18 x^23 + 9 x^22 - 19 x^21 - 10 x^20 - 2 x^19 - 8 x^18 - 5 x^17 - 94 x^16 - 91 x^15 + 22 x^14 + 18 x^13 + 62 x^12 + 62 x^11 + 19 x^10 + 2 x^9 + 10 x^8 + 10 x^7 - 9 x^6 - 64 x^5 - 44 x^4 - 4 x^3 + 40 x^2 + 56 x + 28 -(isolate time :time 0.00 :before-memory 2196.83 :after-memory 2196.84) -(sturm time :time 0.00 :before-memory 2196.84 :after-memory 2196.88) +(isolate time :time 0.01 :before-memory 1466.11 :after-memory 1466.11) +(sturm time :time 0.02 :before-memory 1466.11 :after-memory 1466.16) square free part: x^25 + 5 x^24 + 3 x^23 - 2 x^22 - x^21 - 12 x^20 - 8 x^19 - 8 x^18 + 3 x^17 + 6 x^16 - 20 x^15 + 5 x^14 + 14 x^13 - x^12 + 26 x^11 + 15 x^10 - 6 x^9 - x^8 - 6 x^7 + 13 x^6 - x^5 - 7 x^4 - x^3 + 6 x^2 + 14 x + 14 -(sqf time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) -(fourier time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +(sqf time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) +(fourier time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) num. roots: 5 sign var(-oo): 15 sign var(+oo): 10 roots: -intervals: (1.25, 1.5) (1, 1.25) (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 2196.88 :after-memory 2196.89) +intervals: (1.25, 1.5) (1, 1.25) (-8, -4) (-2, -1.5) (-1.5, -1)(interval check :time 0.00 :before-memory 1466.16 :after-memory 1466.16) isolating roots of: 900 x^19 - 6000113760 x^18 + 10000758403594816 x^17 - 1264023965440000000 x^16 + 39942400000000000000 x^15 - 2700000000000 x^14 + 18000341280000000000 x^13 - 30002275210784448000000000 x^12 + 3792071896320000000000000000 x^11 - 119827200000000000000000000000 x^10 + 2700000000000000000000 x^9 - 18000341280000000000000000000 x^8 + 30002275210784448000000000000000000 x^7 - 3792071896320000000000000000000000000 x^6 + 119827200000000000000000000000000000000 x^5 - 900000000000000000000000000000 x^4 + 6000113760000000000000000000000000000 x^3 - 10000758403594816000000000000000000000000000 x^2 + 1264023965440000000000000000000000000000000000 x - 39942400000000000000000000000000000000000000000 -(isolate time :time 0.00 :before-memory 2196.87 :after-memory 2196.88) -(sturm time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +(isolate time :time 0.02 :before-memory 1466.15 :after-memory 1466.16) +(sturm time :time 0.01 :before-memory 1466.16 :after-memory 1466.16) square free part: 15 x^7 - 50000948 x^6 + 3160000000 x^5 - 15000000000 x^2 + 50000948000000000 x - 3160000000000000000 -(sqf time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) -(fourier time :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +(sqf time :time 0.01 :before-memory 1466.16 :after-memory 1466.16) +(fourier time :time 0.00 :before-memory 1466.16 :after-memory 1466.16) num. roots: 3 sign var(-oo): 5 sign var(+oo): 2 roots: -intervals: (2097152, 4194304) (63.125, 63.25) (63, 63.125)(interval check :time 0.00 :before-memory 2196.88 :after-memory 2196.88) +intervals: (2097152, 4194304) (63.125, 63.25) (63, 63.125)(interval check :time 0.00 :before-memory 1466.16 :after-memory 1466.16) p: x0^5 + 2 x0^4 - 10 x0^3 - 20 x0^2 + 9 x0 + 18 q: x^5 + 2 x^4 - 10 x^3 - 20 x^2 + 9 x + 18 @@ -22947,7 +22978,7 @@ V: 3 x^2 - x - 3 D: 1 PASS -(test upolynomial :time 1.73 :before-memory 2196.56 :after-memory 2196.56) +(test upolynomial :time 6.73 :before-memory 1465.83 :after-memory 1465.83) root: 2 root: (#^4 - 4, 2) -------------- @@ -23434,7 +23465,7 @@ 823515360433462125/2^60 < 5/7 < 411757680216731065/2^59 0.71428571428571428509? < 0.71428571428571428571? < 0.71428571428571428943? PASS -(test algebraic :time 2.00 :before-memory 2196.56 :after-memory 2196.56) +(test algebraic :time 6.28 :before-memory 1465.83 :after-memory 1465.83) root: 2 root: (#^4 - 4, 2) -------------- @@ -23921,11 +23952,11 @@ 823515360433462125/2^60 < 5/7 < 411757680216731065/2^59 0.71428571428571428509? < 0.71428571428571428571? < 0.71428571428571428943? PASS -(test algebraic :time 1.99 :before-memory 2196.56 :after-memory 2196.56) +(test algebraic :time 4.89 :before-memory 1465.83 :after-memory 1465.83) PASS -(test polynomial_factorization :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test polynomial_factorization :time 0.00 :before-memory 1465.83 :after-memory 1465.83) PASS -(test polynomial_factorization :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test polynomial_factorization :time 0.00 :before-memory 1465.83 :after-memory 1465.83) 2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, @@ -24838,7 +24869,7 @@ 104659, 104677, 104681, 104683, 104693, 104701, 104707, 104711, 104717, 104723, 104729, PASS -(test prime_generator :time 0.15 :before-memory 2196.56 :after-memory 2196.56) +(test prime_generator :time 0.80 :before-memory 1465.83 :after-memory 1465.83) 2, 3, 5, 7, 11, 13, 17, 19, 23, 29, 31, 37, 41, 43, 47, 53, 59, 61, 67, 71, 73, 79, 83, @@ -25751,11 +25782,11 @@ 104659, 104677, 104681, 104683, 104693, 104701, 104707, 104711, 104717, 104723, 104729, PASS -(test prime_generator :time 0.15 :before-memory 2196.56 :after-memory 2196.56) +(test prime_generator :time 0.46 :before-memory 1465.83 :after-memory 1465.83) PASS -(test permutation :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test permutation :time 0.00 :before-memory 1465.83 :after-memory 1465.83) PASS -(test permutation :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test permutation :time 0.00 :before-memory 1465.83 :after-memory 1465.83) 1) {(-oo, ~p1, -1.4142135623?), (1.4142135623?, ~p1, oo)} 2) {(-oo, ~p1, -1.4142135623?), (1.4142135623?, ~p1, oo)} ------------------ @@ -26623,7 +26654,7 @@ s2: {(1, p2, 2), [2, p1, oo)} union(s1, s2): {(-oo, p1, 1], (1, p2, 2), [2, p1, oo)}* PASS -(test nlsat :time 0.07 :before-memory 2196.56 :after-memory 2196.56) +(test nlsat :time 0.15 :before-memory 1465.83 :after-memory 1465.83) 1) {(-oo, ~p1, -1.4142135623?), (1.4142135623?, ~p1, oo)} 2) {(-oo, ~p1, -1.4142135623?), (1.4142135623?, ~p1, oo)} ------------------ @@ -27491,15 +27522,15 @@ s2: {(1, p2, 2), [2, p1, oo)} union(s1, s2): {(-oo, p1, 1], (1, p2, 2), [2, p1, oo)}* PASS -(test nlsat :time 0.07 :before-memory 2196.56 :after-memory 2196.56) +(test nlsat :time 0.21 :before-memory 1465.83 :after-memory 1465.83) PASS -(test ext_numeral :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test ext_numeral :time 0.00 :before-memory 1465.83 :after-memory 1465.83) PASS -(test ext_numeral :time 0.00 :before-memory 2196.56 :after-memory 2196.56) +(test ext_numeral :time 0.00 :before-memory 1465.83 :after-memory 1465.83) PASS -(test interval :time 3.94 :before-memory 2196.56 :after-memory 2196.56) +(test interval :time 14.39 :before-memory 1465.83 :after-memory 1465.83) PASS -(test interval :time 3.74 :before-memory 2196.56 :after-memory 2196.56) +(test interval :time 24.73 :before-memory 1465.83 :after-memory 1465.83) floor(11/3): 3 ceil(11/3): 4 floor(-11/3): -4 @@ -27514,7 +27545,7 @@ floor(11): 11 ceil(11): 11 PASS -(test f2n :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test f2n :time 0.01 :before-memory 1465.84 :after-memory 1465.84) floor(11/3): 3 ceil(11/3): 4 floor(-11/3): -4 @@ -27529,19 +27560,19 @@ floor(11): 11 ceil(11): 11 PASS -(test f2n :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test f2n :time 0.01 :before-memory 1465.84 :after-memory 1465.84) 28.7092 PASS -(test hwf :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test hwf :time 0.01 :before-memory 1465.84 :after-memory 1465.84) 28.7092 PASS -(test hwf :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test hwf :time 0.01 :before-memory 1465.84 :after-memory 1465.84) e float... PASS -(test trigo :time 1.05 :before-memory 2196.56 :after-memory 2196.56) +(test trigo :time 2.74 :before-memory 1465.84 :after-memory 1465.84) e float... PASS -(test trigo :time 1.06 :before-memory 2196.56 :after-memory 2196.56) +(test trigo :time 2.58 :before-memory 1465.84 :after-memory 1465.84) shr({0, 0}, 1) shl({0, 2}, 10) for sz = 1 @@ -27594,7 +27625,7 @@ shift by 1, k times self-shl PASS -(test bits :time 1.56 :before-memory 2196.56 :after-memory 2196.56) +(test bits :time 11.38 :before-memory 1465.84 :after-memory 1465.84) shr({0, 0}, 1) shl({0, 2}, 10) for sz = 1 @@ -27647,7 +27678,7 @@ shift by 1, k times self-shl PASS -(test bits :time 1.55 :before-memory 2196.56 :after-memory 2196.56) +(test bits :time 7.07 :before-memory 1465.84 :after-memory 1465.84) 36637340735244577447646647796940134554460176108377786095865669439633741578249/2^67 1066286953144141515008134528672675792897940150822331957049483591681/2^32 496528555240547989964547813251929261208484019535748268035/2 @@ -27655,7 +27686,7 @@ -1066286953144141515008134528672675792897940150822331957049483591681/2^32 283568639100782052886145506193140176213/2^127 PASS -(test mpbq :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test mpbq :time 0.01 :before-memory 1465.84 :after-memory 1465.84) 36637340735244577447646647796940134554460176108377786095865669439633741578249/2^67 1066286953144141515008134528672675792897940150822331957049483591681/2^32 496528555240547989964547813251929261208484019535748268035/2 @@ -27663,7 +27694,7 @@ -1066286953144141515008134528672675792897940150822331957049483591681/2^32 283568639100782052886145506193140176213/2^127 PASS -(test mpbq :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test mpbq :time 0.01 :before-memory 1465.84 :after-memory 1465.84) 1 + 2 == 3 0000000000000010.aaaaaaaa 16.6666666665114462375640869140625 @@ -27671,7 +27702,7 @@ 16.66666666674427688121795654296875 -0.25 PASS -(test mpfx :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test mpfx :time 0.01 :before-memory 1465.84 :after-memory 1465.84) 1 + 2 == 3 0000000000000010.aaaaaaaa 16.6666666665114462375640869140625 @@ -27679,7 +27710,7 @@ 16.66666666674427688121795654296875 -0.25 PASS -(test mpfx :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test mpfx :time 0.01 :before-memory 1465.84 :after-memory 1465.84) 8000000000000000*2^-63 ffffffffffffffff*2^0 1/18446744073709551615 <= 9223372036854775809/2^127 @@ -27827,7 +27858,7 @@ (- 2.0) (/ 6148914691236517205.0 (^ 2.0 64.0)) PASS -(test mpff :time 4.28 :before-memory 2196.56 :after-memory 2196.56) +(test mpff :time 8.85 :before-memory 1465.84 :after-memory 1465.84) 8000000000000000*2^-63 ffffffffffffffff*2^0 1/18446744073709551615 <= 9223372036854775809/2^127 @@ -27975,7 +28006,7 @@ (- 2.0) (/ 6148914691236517205.0 (^ 2.0 64.0)) PASS -(test mpff :time 4.22 :before-memory 2196.56 :after-memory 2196.56) +(test mpff :time 13.51 :before-memory 1465.84 :after-memory 1465.84) (define-fun q ((x!1 Int) (x!2 Int)) Bool false) (define-fun p ((x!1 Int) (x!2 Int)) Bool @@ -28003,7 +28034,7 @@ (define-fun r ((x!1 Int) (x!2 Int)) Bool false) PASS -(test horn_subsume_model_converter :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test horn_subsume_model_converter :time 0.03 :before-memory 1465.84 :after-memory 1465.84) (define-fun q ((x!1 Int) (x!2 Int)) Bool false) (define-fun p ((x!1 Int) (x!2 Int)) Bool @@ -28031,7 +28062,7 @@ (define-fun r ((x!1 Int) (x!2 Int)) Bool false) PASS -(test horn_subsume_model_converter :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test horn_subsume_model_converter :time 0.02 :before-memory 1465.84 :after-memory 1465.84) (define-fun x () Int 0) (define-fun p ((x!1 Int) (x!2 Int)) Int @@ -28054,7 +28085,7 @@ (= (p A B) a!1))) a!1)) PASS -(test model2expr :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test model2expr :time 0.02 :before-memory 1465.84 :after-memory 1465.84) (define-fun x () Int 0) (define-fun p ((x!1 Int) (x!2 Int)) Int @@ -28077,7 +28108,7 @@ (= (p A B) a!1))) a!1)) PASS -(test model2expr :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test model2expr :time 0.02 :before-memory 1465.84 :after-memory 1465.84) hilbert basis test hb.basis_size: 76 hb.index.num_insert: 76 @@ -28113,7 +28144,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 304 heap_trie.num_nodes: 3270 -time: 0.01 +time: 0.02 hb.basis_size: 76 hb.index.num_insert: 380 hb.index.size: 76 @@ -28122,7 +28153,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 380 heap_trie.num_nodes: 3342 -time: 0.01 +time: 0.02 hb.basis_size: 76 hb.index.num_insert: 456 hb.index.size: 76 @@ -28131,7 +28162,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 456 heap_trie.num_nodes: 3416 -time: 0.01 +time: 0.02 hb.basis_size: 76 hb.index.num_insert: 532 hb.index.size: 76 @@ -28140,7 +28171,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 532 heap_trie.num_nodes: 3492 -time: 0.01 +time: 0.02 hb.basis_size: 76 hb.index.num_insert: 608 hb.index.size: 76 @@ -28149,7 +28180,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 608 heap_trie.num_nodes: 3570 -time: 0.01 +time: 0.02 hb.basis_size: 76 hb.index.num_insert: 684 hb.index.size: 76 @@ -28158,7 +28189,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 684 heap_trie.num_nodes: 3650 -time: 0.01 +time: 0.02 hb.basis_size: 76 hb.index.num_insert: 760 hb.index.size: 76 @@ -28167,7 +28198,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 760 heap_trie.num_nodes: 3732 -time: 0.01 +time: 0.02 hb.basis_size: 76 hb.index.num_insert: 836 hb.index.size: 76 @@ -28176,7 +28207,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 836 heap_trie.num_nodes: 3816 -time: 0.01 +time: 0.03 hb.basis_size: 76 hb.index.num_insert: 912 hb.index.size: 76 @@ -28185,7 +28216,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 912 heap_trie.num_nodes: 3902 -time: 0.02 +time: 0.03 hb.basis_size: 76 hb.index.num_insert: 988 hb.index.size: 76 @@ -28194,7 +28225,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 988 heap_trie.num_nodes: 3990 -time: 0.02 +time: 0.03 hb.basis_size: 76 hb.index.num_insert: 1064 hb.index.size: 76 @@ -28203,7 +28234,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1064 heap_trie.num_nodes: 4080 -time: 0.02 +time: 0.03 hb.basis_size: 76 hb.index.num_insert: 1140 hb.index.size: 76 @@ -28212,7 +28243,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1140 heap_trie.num_nodes: 4097 -time: 0.02 +time: 0.03 hb.basis_size: 76 hb.index.num_insert: 1216 hb.index.size: 76 @@ -28221,7 +28252,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1216 heap_trie.num_nodes: 4188 -time: 0.02 +time: 0.03 hb.basis_size: 76 hb.index.num_insert: 1292 hb.index.size: 76 @@ -28230,7 +28261,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1292 heap_trie.num_nodes: 4289 -time: 0.02 +time: 0.04 hb.basis_size: 76 hb.index.num_insert: 1368 hb.index.size: 76 @@ -28239,7 +28270,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1368 heap_trie.num_nodes: 4400 -time: 0.02 +time: 0.04 hb.basis_size: 76 hb.index.num_insert: 1444 hb.index.size: 76 @@ -28248,7 +28279,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1444 heap_trie.num_nodes: 4719 -time: 0.02 +time: 0.04 hb.basis_size: 76 hb.index.num_insert: 1520 hb.index.size: 76 @@ -28257,7 +28288,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1520 heap_trie.num_nodes: 4898 -time: 0.02 +time: 0.04 hb.basis_size: 76 hb.index.num_insert: 1596 hb.index.size: 76 @@ -28266,7 +28297,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1596 heap_trie.num_nodes: 5087 -time: 0.02 +time: 0.04 hb.basis_size: 76 hb.index.num_insert: 1672 hb.index.size: 76 @@ -28275,7 +28306,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1672 heap_trie.num_nodes: 5109 -time: 0.02 +time: 0.04 hb.basis_size: 76 hb.index.num_insert: 1748 hb.index.size: 76 @@ -28284,7 +28315,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1748 heap_trie.num_nodes: 5441 -time: 0.02 +time: 0.04 hb.basis_size: 76 hb.index.num_insert: 1824 hb.index.size: 76 @@ -28293,7 +28324,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1824 heap_trie.num_nodes: 5708 -time: 0.02 +time: 0.05 hb.basis_size: 76 hb.index.num_insert: 1900 hb.index.size: 76 @@ -28302,7 +28333,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1900 heap_trie.num_nodes: 5712 -time: 0.02 +time: 0.05 hb.basis_size: 76 hb.index.num_insert: 1976 hb.index.size: 76 @@ -28311,7 +28342,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1976 heap_trie.num_nodes: 5737 -time: 0.03 +time: 0.05 hb.basis_size: 76 hb.index.num_insert: 2052 hb.index.size: 76 @@ -28320,7 +28351,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 2052 heap_trie.num_nodes: 6082 -time: 0.03 +time: 0.06 hb.basis_size: 76 hb.index.num_insert: 2128 hb.index.size: 76 @@ -28329,7 +28360,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 2128 heap_trie.num_nodes: 6086 -time: 0.03 +time: 0.06 hb.basis_size: 76 hb.index.num_insert: 2204 hb.index.size: 76 @@ -28338,7 +28369,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 2204 heap_trie.num_nodes: 6090 -time: 0.03 +time: 0.07 hb.basis_size: 76 hb.index.num_insert: 2280 hb.index.size: 76 @@ -28347,7 +28378,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 2280 heap_trie.num_nodes: 6118 -time: 0.03 +time: 0.08 sat inequalities: + x1 + x16 + x31 + x46 + x61 >= 0 @@ -28465,9 +28496,9 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 2280 heap_trie.num_nodes: 6118 -time: 0.413326 secs +time: 1.01316 secs PASS -(test hilbert_basis :time 0.42 :before-memory 2196.56 :after-memory 2196.56) +(test hilbert_basis :time 1.04 :before-memory 1465.84 :after-memory 1465.84) hilbert basis test hb.basis_size: 76 hb.index.num_insert: 76 @@ -28476,7 +28507,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 76 heap_trie.num_nodes: 3066 -time: 0.01 +time: 0.02 hb.basis_size: 76 hb.index.num_insert: 152 hb.index.size: 76 @@ -28485,7 +28516,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 152 heap_trie.num_nodes: 3132 -time: 0.01 +time: 0.02 hb.basis_size: 76 hb.index.num_insert: 228 hb.index.size: 76 @@ -28494,7 +28525,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 228 heap_trie.num_nodes: 3200 -time: 0.01 +time: 0.02 hb.basis_size: 76 hb.index.num_insert: 304 hb.index.size: 76 @@ -28503,7 +28534,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 304 heap_trie.num_nodes: 3270 -time: 0.01 +time: 0.02 hb.basis_size: 76 hb.index.num_insert: 380 hb.index.size: 76 @@ -28512,7 +28543,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 380 heap_trie.num_nodes: 3342 -time: 0.01 +time: 0.02 hb.basis_size: 76 hb.index.num_insert: 456 hb.index.size: 76 @@ -28521,7 +28552,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 456 heap_trie.num_nodes: 3416 -time: 0.01 +time: 0.03 hb.basis_size: 76 hb.index.num_insert: 532 hb.index.size: 76 @@ -28530,7 +28561,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 532 heap_trie.num_nodes: 3492 -time: 0.01 +time: 0.03 hb.basis_size: 76 hb.index.num_insert: 608 hb.index.size: 76 @@ -28539,7 +28570,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 608 heap_trie.num_nodes: 3570 -time: 0.01 +time: 0.03 hb.basis_size: 76 hb.index.num_insert: 684 hb.index.size: 76 @@ -28548,7 +28579,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 684 heap_trie.num_nodes: 3650 -time: 0.01 +time: 0.03 hb.basis_size: 76 hb.index.num_insert: 760 hb.index.size: 76 @@ -28557,7 +28588,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 760 heap_trie.num_nodes: 3732 -time: 0.01 +time: 0.03 hb.basis_size: 76 hb.index.num_insert: 836 hb.index.size: 76 @@ -28566,7 +28597,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 836 heap_trie.num_nodes: 3816 -time: 0.01 +time: 0.03 hb.basis_size: 76 hb.index.num_insert: 912 hb.index.size: 76 @@ -28575,7 +28606,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 912 heap_trie.num_nodes: 3902 -time: 0.02 +time: 0.03 hb.basis_size: 76 hb.index.num_insert: 988 hb.index.size: 76 @@ -28584,7 +28615,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 988 heap_trie.num_nodes: 3990 -time: 0.02 +time: 0.03 hb.basis_size: 76 hb.index.num_insert: 1064 hb.index.size: 76 @@ -28593,7 +28624,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1064 heap_trie.num_nodes: 4080 -time: 0.02 +time: 0.03 hb.basis_size: 76 hb.index.num_insert: 1140 hb.index.size: 76 @@ -28602,7 +28633,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1140 heap_trie.num_nodes: 4097 -time: 0.02 +time: 0.04 hb.basis_size: 76 hb.index.num_insert: 1216 hb.index.size: 76 @@ -28611,7 +28642,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1216 heap_trie.num_nodes: 4188 -time: 0.02 +time: 0.04 hb.basis_size: 76 hb.index.num_insert: 1292 hb.index.size: 76 @@ -28620,7 +28651,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1292 heap_trie.num_nodes: 4289 -time: 0.02 +time: 0.04 hb.basis_size: 76 hb.index.num_insert: 1368 hb.index.size: 76 @@ -28629,7 +28660,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1368 heap_trie.num_nodes: 4400 -time: 0.02 +time: 0.04 hb.basis_size: 76 hb.index.num_insert: 1444 hb.index.size: 76 @@ -28638,7 +28669,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1444 heap_trie.num_nodes: 4719 -time: 0.02 +time: 0.04 hb.basis_size: 76 hb.index.num_insert: 1520 hb.index.size: 76 @@ -28647,7 +28678,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1520 heap_trie.num_nodes: 4898 -time: 0.02 +time: 0.05 hb.basis_size: 76 hb.index.num_insert: 1596 hb.index.size: 76 @@ -28656,7 +28687,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1596 heap_trie.num_nodes: 5087 -time: 0.02 +time: 0.05 hb.basis_size: 76 hb.index.num_insert: 1672 hb.index.size: 76 @@ -28665,7 +28696,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1672 heap_trie.num_nodes: 5109 -time: 0.02 +time: 0.05 hb.basis_size: 76 hb.index.num_insert: 1748 hb.index.size: 76 @@ -28674,7 +28705,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1748 heap_trie.num_nodes: 5441 -time: 0.02 +time: 0.05 hb.basis_size: 76 hb.index.num_insert: 1824 hb.index.size: 76 @@ -28683,7 +28714,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1824 heap_trie.num_nodes: 5708 -time: 0.02 +time: 0.06 hb.basis_size: 76 hb.index.num_insert: 1900 hb.index.size: 76 @@ -28692,7 +28723,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1900 heap_trie.num_nodes: 5712 -time: 0.02 +time: 0.06 hb.basis_size: 76 hb.index.num_insert: 1976 hb.index.size: 76 @@ -28701,7 +28732,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 1976 heap_trie.num_nodes: 5737 -time: 0.03 +time: 0.06 hb.basis_size: 76 hb.index.num_insert: 2052 hb.index.size: 76 @@ -28710,7 +28741,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 2052 heap_trie.num_nodes: 6082 -time: 0.03 +time: 0.06 hb.basis_size: 76 hb.index.num_insert: 2128 hb.index.size: 76 @@ -28719,7 +28750,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 2128 heap_trie.num_nodes: 6086 -time: 0.03 +time: 0.06 hb.basis_size: 76 hb.index.num_insert: 2204 hb.index.size: 76 @@ -28728,7 +28759,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 2204 heap_trie.num_nodes: 6090 -time: 0.03 +time: 0.06 hb.basis_size: 76 hb.index.num_insert: 2280 hb.index.size: 76 @@ -28737,7 +28768,7 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 2280 heap_trie.num_nodes: 6118 -time: 0.03 +time: 0.06 sat inequalities: + x1 + x16 + x31 + x46 + x61 >= 0 @@ -28855,9 +28886,9 @@ heap_trie.num_2_children: 74 heap_trie.num_inserts: 2280 heap_trie.num_nodes: 6118 -time: 0.413967 secs +time: 1.13172 secs PASS -(test hilbert_basis :time 0.42 :before-memory 2196.56 :after-memory 2196.56) +(test hilbert_basis :time 1.15 :before-memory 1465.84 :after-memory 1465.84) find_le: 1 2 3 |-> 1 3 heap_trie.num_1_children: 4 heap_trie.num_2_children: 2 @@ -28907,7 +28938,7 @@ 2 refs: 1 3 refs: 1 value: 2 PASS -(test heap_trie :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test heap_trie :time 0.01 :before-memory 1465.84 :after-memory 1465.84) find_le: 1 2 3 |-> 1 3 heap_trie.num_1_children: 4 heap_trie.num_2_children: 2 @@ -28957,7 +28988,7 @@ 2 refs: 1 3 refs: 1 value: 2 PASS -(test heap_trie :time 0.01 :before-memory 2196.56 :after-memory 2196.56) +(test heap_trie :time 0.01 :before-memory 1465.84 :after-memory 1465.84) ND 1 0 = 0 0 2 = 0 @@ -28990,7 +29021,7 @@ 0 0 = -1 0 0 = 1 PASS -(test karr :time 0.01 :before-memory 2196.56 :after-memory 2196.58) +(test karr :time 0.01 :before-memory 1465.84 :after-memory 1465.86) ND 1 0 = 0 0 2 = 0 @@ -29023,15 +29054,15 @@ 0 0 = -1 0 0 = 1 PASS -(test karr :time 0.01 :before-memory 2196.58 :after-memory 2196.59) +(test karr :time 0.01 :before-memory 1465.86 :after-memory 1465.87) PASS -(test no_overflow :time 0.01 :before-memory 2196.59 :after-memory 2196.59) +(test no_overflow :time 0.01 :before-memory 1465.87 :after-memory 1465.87) PASS -(test no_overflow :time 0.01 :before-memory 2196.59 :after-memory 2196.59) +(test no_overflow :time 0.01 :before-memory 1465.87 :after-memory 1465.87) PASS -(test memory :time 0.01 :before-memory 2196.59 :after-memory 2196.59) +(test memory :time 0.01 :before-memory 1465.87 :after-memory 1465.87) PASS -(test memory :time 0.01 :before-memory 2196.59 :after-memory 2196.59) +(test memory :time 0.01 :before-memory 1465.87 :after-memory 1465.87) Expecting colon in declaration (first occurrence of a predicate must be a declaration) at line 2 '' found ',' Parser did not succeed on string @@ -29073,7 +29104,7 @@ H :- C1(X,a\,\b), C2(Y,a,X) . PASS -(test datalog_parser :time 76.88 :before-memory 2196.59 :after-memory 4244.59) +(test datalog_parser :time 150.69 :before-memory 1465.87 :after-memory 3513.87) Expecting colon in declaration (first occurrence of a predicate must be a declaration) at line 2 '' found ',' Parser did not succeed on string @@ -29115,7 +29146,7 @@ H :- C1(X,a\,\b), C2(Y,a,X) . PASS -(test datalog_parser :time 76.84 :before-memory 4244.59 :after-memory 6292.59) +(test datalog_parser :time 135.57 :before-memory 3513.87 :after-memory 5561.87) rm -f interval_lemma_* trigo-lemmas.math make[1]: Leaving directory '/build/z3-4.4.1' fakeroot debian/rules binary @@ -29134,7 +29165,7 @@ make[1]: Entering directory '/build/z3-4.4.1' mkdir -p debian/tmp/usr/lib/python2.7/dist-packages/ dh_auto_install - make -j3 install DESTDIR=/build/z3-4.4.1/debian/tmp AM_UPDATE_INFO_DIR=no + make -j4 install DESTDIR=/build/z3-4.4.1/debian/tmp AM_UPDATE_INFO_DIR=no make[2]: Entering directory '/build/z3-4.4.1' make -C build install make[3]: Entering directory '/build/z3-4.4.1/build' @@ -29207,26 +29238,26 @@ dh_installdeb -O--parallel dh_ocaml -O--parallel dh_gencontrol -O--parallel +dpkg-gencontrol: warning: Depends field of package libz3-cil: substitution variable ${shlibs:Depends} used, but is not defined dpkg-gencontrol: warning: Depends field of package python-z3: substitution variable ${shlibs:Depends} used, but is not defined dpkg-gencontrol: warning: package python-z3: substitution variable ${python:Provides} unused, but is defined dpkg-gencontrol: warning: package python-z3: substitution variable ${python:Versions} unused, but is defined -dpkg-gencontrol: warning: Depends field of package libz3-cil: substitution variable ${shlibs:Depends} used, but is not defined dpkg-gencontrol: warning: package libz3-ocaml-dev: substitution variable ${ocaml:Provides} unused, but is defined dpkg-gencontrol: warning: package libz3-ocaml-dev: substitution variable ${ocaml:Provides} unused, but is defined dh_md5sums -O--parallel dh_builddeb -O--parallel -dpkg-deb: building package 'libz3-dev' in '../libz3-dev_4.4.1-1~deb10u1_armhf.deb'. -dpkg-deb: building package 'libz3-ocaml-dev-dbgsym' in '../libz3-ocaml-dev-dbgsym_4.4.1-1~deb10u1_armhf.deb'. dpkg-deb: building package 'z3' in '../z3_4.4.1-1~deb10u1_armhf.deb'. +dpkg-deb: building package 'libz3-4-dbgsym' in '../libz3-4-dbgsym_4.4.1-1~deb10u1_armhf.deb'. dpkg-deb: building package 'libz3-java' in '../libz3-java_4.4.1-1~deb10u1_armhf.deb'. -dpkg-deb: building package 'python-z3' in '../python-z3_4.4.1-1~deb10u1_armhf.deb'. -dpkg-deb: building package 'libz3-jni' in '../libz3-jni_4.4.1-1~deb10u1_armhf.deb'. -dpkg-deb: building package 'libz3-jni-dbgsym' in '../libz3-jni-dbgsym_4.4.1-1~deb10u1_armhf.deb'. dpkg-deb: building package 'libz3-cil' in '../libz3-cil_4.4.1-1~deb10u1_armhf.deb'. +dpkg-deb: building package 'libz3-jni' in '../libz3-jni_4.4.1-1~deb10u1_armhf.deb'. dpkg-deb: building package 'libz3-ocaml-dev' in '../libz3-ocaml-dev_4.4.1-1~deb10u1_armhf.deb'. +dpkg-deb: building package 'libz3-jni-dbgsym' in '../libz3-jni-dbgsym_4.4.1-1~deb10u1_armhf.deb'. +dpkg-deb: building package 'libz3-ocaml-dev-dbgsym' in '../libz3-ocaml-dev-dbgsym_4.4.1-1~deb10u1_armhf.deb'. dpkg-deb: building package 'z3-dbgsym' in '../z3-dbgsym_4.4.1-1~deb10u1_armhf.deb'. +dpkg-deb: building package 'libz3-dev' in '../libz3-dev_4.4.1-1~deb10u1_armhf.deb'. +dpkg-deb: building package 'python-z3' in '../python-z3_4.4.1-1~deb10u1_armhf.deb'. dpkg-deb: building package 'libz3-4' in '../libz3-4_4.4.1-1~deb10u1_armhf.deb'. -dpkg-deb: building package 'libz3-4-dbgsym' in '../libz3-4-dbgsym_4.4.1-1~deb10u1_armhf.deb'. dpkg-genbuildinfo --build=binary dpkg-genchanges --build=binary >../z3_4.4.1-1~deb10u1_armhf.changes dpkg-genchanges: warning: the current version (4.4.1-1~deb10u1) is earlier than the previous one (4.4.1-1) @@ -29234,12 +29265,14 @@ dpkg-source --after-build . dpkg-buildpackage: info: binary-only upload (no source included) I: copying local configuration +I: user script /srv/workspace/pbuilder/15030/tmp/hooks/B01_cleanup starting +I: user script /srv/workspace/pbuilder/15030/tmp/hooks/B01_cleanup finished I: unmounting dev/ptmx filesystem I: unmounting dev/pts filesystem I: unmounting dev/shm filesystem I: unmounting proc filesystem I: unmounting sys filesystem I: cleaning the build env -I: removing directory /srv/workspace/pbuilder/13915 and its subdirectories -I: Current time: Wed Aug 12 14:10:58 -12 2020 -I: pbuilder-time-stamp: 1597284658 +I: removing directory /srv/workspace/pbuilder/15030 and its subdirectories +I: Current time: Thu Aug 13 18:51:50 +14 2020 +I: pbuilder-time-stamp: 1597294310