Input buildinfo: https://buildinfos.debian.net/buildinfo-pool/b/boogie/boogie_2.4.1+dfsg-0.1_all.buildinfo Use metasnap for getting required timestamps New buildinfo file: /tmp/boogie-2.4.1+dfsg-0.1d27k1joe/boogie_2.4.1+dfsg-0.1_all.buildinfo Get source package info: boogie=2.4.1+dfsg-0.1 Source URL: http://snapshot.notset.fr/mr/package/boogie/2.4.1+dfsg-0.1/srcfiles?fileinfo=1 env -i PATH=/usr/sbin:/usr/bin:/sbin:/bin TMPDIR=/tmp mmdebstrap --arch=amd64 --include=autoconf=2.69-11 automake=1:1.16.1-4 autopoint=0.19.8.1-10 autotools-dev=20180224.1 base-files=11 base-passwd=3.5.47 bash=5.0-5 binutils=2.33.1-6 binutils-common=2.33.1-6 binutils-x86-64-linux-gnu=2.33.1-6 bsdmainutils=11.1.2+b1 bsdutils=1:2.34-0.1 build-essential=12.8 bzip2=1.0.8-2 ca-certificates=20190110 cli-common=0.10 cli-common-dev=0.10 coreutils=8.30-3+b1 cpp=4:9.2.1-3.1 cpp-9=9.2.1-21 dash=0.5.10.2-6 debconf=1.5.73 debhelper=12.7.2 debianutils=4.9.1 dh-autoreconf=19 dh-strip-nondeterminism=1.6.3-1 diffutils=1:3.7-3 dpkg=1.19.7 dpkg-dev=1.19.7 dwz=0.13-5 fdisk=2.34-0.1 file=1:5.37-6 findutils=4.7.0-1 fontconfig-config=2.13.1-2 fonts-dejavu-core=2.37-1 g++=4:9.2.1-3.1 g++-9=9.2.1-21 gcc=4:9.2.1-3.1 gcc-9=9.2.1-21 gcc-9-base=9.2.1-21 gettext=0.19.8.1-10 gettext-base=0.19.8.1-10 grep=3.3-1 groff-base=1.22.4-4 gzip=1.9-3+b1 hostname=3.23 init-system-helpers=1.57 intltool-debian=0.35.0+20060710.5 libacl1=2.2.53-5 libarchive-zip-perl=1.67-1 libasan5=9.2.1-21 libatomic1=9.2.1-21 libattr1=1:2.4.48-5 libaudit-common=1:2.8.5-2 libaudit1=1:2.8.5-2+b1 libbinutils=2.33.1-6 libblkid1=2.34-0.1 libbsd0=0.10.0-1 libbz2-1.0=1.0.8-2 libc-bin=2.29-6 libc-dev-bin=2.29-6 libc6=2.29-6 libc6-dev=2.29-6 libcairo2=1.16.0-4 libcap-ng0=0.7.9-2.1+b1 libcc1-0=9.2.1-21 libcroco3=0.6.13-1 libcrypt1=1:4.4.10-7 libcrypt1-dev=1:4.4.10-7 libdb5.3=5.3.28+dfsg1-0.6 libdebconfclient0=0.250 libdebhelper-perl=12.7.2 libdpkg-perl=1.19.7 libelf1=0.176-1.1 libencode-locale-perl=1.05-1 libexif12=0.6.21-5.1 libexpat1=2.2.9-1 libfdisk1=2.34-0.1 libffi6=3.2.1-9 libfile-listing-perl=6.04-1 libfile-stripnondeterminism-perl=1.6.3-1 libfontconfig1=2.13.1-2+b1 libfreetype6=2.10.1-2 libgcc-9-dev=9.2.1-21 libgcc1=1:9.2.1-21 libgcrypt20=1.8.5-3 libgdbm-compat4=1.18.1-5 libgdbm6=1.18.1-5 libgdiplus=6.0.4+dfsg-1 libgif7=5.1.9-1 libglib2.0-0=2.62.3-2 libgmp10=2:6.1.2+dfsg-4 libgomp1=9.2.1-21 libgpg-error0=1.36-7 libhtml-parser-perl=3.72-3+b4 libhtml-tagset-perl=3.20-4 libhtml-tree-perl=5.07-2 libhttp-cookies-perl=6.08-1 libhttp-date-perl=6.05-1 libhttp-message-perl=6.18-1 libhttp-negotiate-perl=6.01-1 libicu63=63.2-2 libio-html-perl=1.001-1 libio-socket-ssl-perl=2.066-1 libisl22=0.22-2 libitm1=9.2.1-21 libjbig0=2.1-3.1+b2 libjpeg62-turbo=1:1.5.2-2+b1 liblsan0=9.2.1-21 liblwp-mediatypes-perl=6.04-1 liblwp-protocol-https-perl=6.07-2 liblz4-1=1.9.2-2 liblzma5=5.2.4-1+b1 libmagic-mgc=1:5.37-6 libmagic1=1:5.37-6 libmono-2.0-dev=5.18.0.240+dfsg-5 libmono-accessibility4.0-cil=5.18.0.240+dfsg-5 libmono-cairo4.0-cil=5.18.0.240+dfsg-5 libmono-cecil-private-cil=5.18.0.240+dfsg-5 libmono-cil-dev=5.18.0.240+dfsg-5 libmono-codecontracts4.0-cil=5.18.0.240+dfsg-5 libmono-compilerservices-symbolwriter4.0-cil=5.18.0.240+dfsg-5 libmono-corlib4.5-cil=5.18.0.240+dfsg-5 libmono-cscompmgd0.0-cil=5.18.0.240+dfsg-5 libmono-csharp4.0c-cil=5.18.0.240+dfsg-5 libmono-custommarshalers4.0-cil=5.18.0.240+dfsg-5 libmono-data-tds4.0-cil=5.18.0.240+dfsg-5 libmono-db2-1.0-cil=5.18.0.240+dfsg-5 libmono-debugger-soft4.0a-cil=5.18.0.240+dfsg-5 libmono-http4.0-cil=5.18.0.240+dfsg-5 libmono-i18n-cjk4.0-cil=5.18.0.240+dfsg-5 libmono-i18n-mideast4.0-cil=5.18.0.240+dfsg-5 libmono-i18n-other4.0-cil=5.18.0.240+dfsg-5 libmono-i18n-rare4.0-cil=5.18.0.240+dfsg-5 libmono-i18n-west4.0-cil=5.18.0.240+dfsg-5 libmono-i18n4.0-all=5.18.0.240+dfsg-5 libmono-i18n4.0-cil=5.18.0.240+dfsg-5 libmono-ldap4.0-cil=5.18.0.240+dfsg-5 libmono-management4.0-cil=5.18.0.240+dfsg-5 libmono-messaging-rabbitmq4.0-cil=5.18.0.240+dfsg-5 libmono-messaging4.0-cil=5.18.0.240+dfsg-5 libmono-microsoft-build-engine4.0-cil=5.18.0.240+dfsg-5 libmono-microsoft-build-framework4.0-cil=5.18.0.240+dfsg-5 libmono-microsoft-build-tasks-v4.0-4.0-cil=5.18.0.240+dfsg-5 libmono-microsoft-build-utilities-v4.0-4.0-cil=5.18.0.240+dfsg-5 libmono-microsoft-build4.0-cil=5.18.0.240+dfsg-5 libmono-microsoft-csharp4.0-cil=5.18.0.240+dfsg-5 libmono-microsoft-visualc10.0-cil=5.18.0.240+dfsg-5 libmono-microsoft-web-infrastructure1.0-cil=5.18.0.240+dfsg-5 libmono-oracle4.0-cil=5.18.0.240+dfsg-5 libmono-parallel4.0-cil=5.18.0.240+dfsg-5 libmono-peapi4.0a-cil=5.18.0.240+dfsg-5 libmono-posix4.0-cil=5.18.0.240+dfsg-5 libmono-rabbitmq4.0-cil=5.18.0.240+dfsg-5 libmono-relaxng4.0-cil=5.18.0.240+dfsg-5 libmono-security4.0-cil=5.18.0.240+dfsg-5 libmono-sharpzip4.84-cil=5.18.0.240+dfsg-5 libmono-simd4.0-cil=5.18.0.240+dfsg-5 libmono-smdiagnostics0.0-cil=5.18.0.240+dfsg-5 libmono-sqlite4.0-cil=5.18.0.240+dfsg-5 libmono-system-componentmodel-composition4.0-cil=5.18.0.240+dfsg-5 libmono-system-componentmodel-dataannotations4.0-cil=5.18.0.240+dfsg-5 libmono-system-configuration-install4.0-cil=5.18.0.240+dfsg-5 libmono-system-configuration4.0-cil=5.18.0.240+dfsg-5 libmono-system-core4.0-cil=5.18.0.240+dfsg-5 libmono-system-data-datasetextensions4.0-cil=5.18.0.240+dfsg-5 libmono-system-data-entity4.0-cil=5.18.0.240+dfsg-5 libmono-system-data-linq4.0-cil=5.18.0.240+dfsg-5 libmono-system-data-services-client4.0-cil=5.18.0.240+dfsg-5 libmono-system-data-services4.0-cil=5.18.0.240+dfsg-5 libmono-system-data4.0-cil=5.18.0.240+dfsg-5 libmono-system-deployment4.0-cil=5.18.0.240+dfsg-5 libmono-system-design4.0-cil=5.18.0.240+dfsg-5 libmono-system-drawing-design4.0-cil=5.18.0.240+dfsg-5 libmono-system-drawing4.0-cil=5.18.0.240+dfsg-5 libmono-system-dynamic4.0-cil=5.18.0.240+dfsg-5 libmono-system-enterpriseservices4.0-cil=5.18.0.240+dfsg-5 libmono-system-identitymodel-selectors4.0-cil=5.18.0.240+dfsg-5 libmono-system-identitymodel4.0-cil=5.18.0.240+dfsg-5 libmono-system-io-compression-filesystem4.0-cil=5.18.0.240+dfsg-5 libmono-system-io-compression4.0-cil=5.18.0.240+dfsg-5 libmono-system-json-microsoft4.0-cil=5.18.0.240+dfsg-5 libmono-system-json4.0-cil=5.18.0.240+dfsg-5 libmono-system-ldap-protocols4.0-cil=5.18.0.240+dfsg-5 libmono-system-ldap4.0-cil=5.18.0.240+dfsg-5 libmono-system-management4.0-cil=5.18.0.240+dfsg-5 libmono-system-messaging4.0-cil=5.18.0.240+dfsg-5 libmono-system-net-http-formatting4.0-cil=5.18.0.240+dfsg-5 libmono-system-net-http-webrequest4.0-cil=5.18.0.240+dfsg-5 libmono-system-net-http4.0-cil=5.18.0.240+dfsg-5 libmono-system-net4.0-cil=5.18.0.240+dfsg-5 libmono-system-numerics-vectors4.0-cil=5.18.0.240+dfsg-5 libmono-system-numerics4.0-cil=5.18.0.240+dfsg-5 libmono-system-reactive-core2.2-cil=5.18.0.240+dfsg-5 libmono-system-reactive-debugger2.2-cil=5.18.0.240+dfsg-5 libmono-system-reactive-experimental2.2-cil=5.18.0.240+dfsg-5 libmono-system-reactive-interfaces2.2-cil=5.18.0.240+dfsg-5 libmono-system-reactive-linq2.2-cil=5.18.0.240+dfsg-5 libmono-system-reactive-observable-aliases0.0-cil=5.18.0.240+dfsg-5 libmono-system-reactive-platformservices2.2-cil=5.18.0.240+dfsg-5 libmono-system-reactive-providers2.2-cil=5.18.0.240+dfsg-5 libmono-system-reactive-runtime-remoting2.2-cil=5.18.0.240+dfsg-5 libmono-system-reactive-windows-forms2.2-cil=5.18.0.240+dfsg-5 libmono-system-reactive-windows-threading2.2-cil=5.18.0.240+dfsg-5 libmono-system-reflection-context4.0-cil=5.18.0.240+dfsg-5 libmono-system-runtime-caching4.0-cil=5.18.0.240+dfsg-5 libmono-system-runtime-durableinstancing4.0-cil=5.18.0.240+dfsg-5 libmono-system-runtime-serialization-formatters-soap4.0-cil=5.18.0.240+dfsg-5 libmono-system-runtime-serialization4.0-cil=5.18.0.240+dfsg-5 libmono-system-runtime4.0-cil=5.18.0.240+dfsg-5 libmono-system-security4.0-cil=5.18.0.240+dfsg-5 libmono-system-servicemodel-activation4.0-cil=5.18.0.240+dfsg-5 libmono-system-servicemodel-discovery4.0-cil=5.18.0.240+dfsg-5 libmono-system-servicemodel-internals0.0-cil=5.18.0.240+dfsg-5 libmono-system-servicemodel-routing4.0-cil=5.18.0.240+dfsg-5 libmono-system-servicemodel-web4.0-cil=5.18.0.240+dfsg-5 libmono-system-servicemodel4.0a-cil=5.18.0.240+dfsg-5 libmono-system-serviceprocess4.0-cil=5.18.0.240+dfsg-5 libmono-system-threading-tasks-dataflow4.0-cil=5.18.0.240+dfsg-5 libmono-system-transactions4.0-cil=5.18.0.240+dfsg-5 libmono-system-web-abstractions4.0-cil=5.18.0.240+dfsg-5 libmono-system-web-applicationservices4.0-cil=5.18.0.240+dfsg-5 libmono-system-web-dynamicdata4.0-cil=5.18.0.240+dfsg-5 libmono-system-web-extensions-design4.0-cil=5.18.0.240+dfsg-5 libmono-system-web-extensions4.0-cil=5.18.0.240+dfsg-5 libmono-system-web-http-selfhost4.0-cil=5.18.0.240+dfsg-5 libmono-system-web-http-webhost4.0-cil=5.18.0.240+dfsg-5 libmono-system-web-http4.0-cil=5.18.0.240+dfsg-5 libmono-system-web-mobile4.0-cil=5.18.0.240+dfsg-5 libmono-system-web-mvc3.0-cil=5.18.0.240+dfsg-5 libmono-system-web-razor2.0-cil=5.18.0.240+dfsg-5 libmono-system-web-regularexpressions4.0-cil=5.18.0.240+dfsg-5 libmono-system-web-routing4.0-cil=5.18.0.240+dfsg-5 libmono-system-web-services4.0-cil=5.18.0.240+dfsg-5 libmono-system-web-webpages-deployment2.0-cil=5.18.0.240+dfsg-5 libmono-system-web-webpages-razor2.0-cil=5.18.0.240+dfsg-5 libmono-system-web-webpages2.0-cil=5.18.0.240+dfsg-5 libmono-system-web4.0-cil=5.18.0.240+dfsg-5 libmono-system-windows-forms-datavisualization4.0a-cil=5.18.0.240+dfsg-5 libmono-system-windows-forms4.0-cil=5.18.0.240+dfsg-5 libmono-system-windows4.0-cil=5.18.0.240+dfsg-5 libmono-system-workflow-activities4.0-cil=5.18.0.240+dfsg-5 libmono-system-workflow-componentmodel4.0-cil=5.18.0.240+dfsg-5 libmono-system-workflow-runtime4.0-cil=5.18.0.240+dfsg-5 libmono-system-xaml4.0-cil=5.18.0.240+dfsg-5 libmono-system-xml-linq4.0-cil=5.18.0.240+dfsg-5 libmono-system-xml-serialization4.0-cil=5.18.0.240+dfsg-5 libmono-system-xml4.0-cil=5.18.0.240+dfsg-5 libmono-system4.0-cil=5.18.0.240+dfsg-5 libmono-tasklets4.0-cil=5.18.0.240+dfsg-5 libmono-webbrowser4.0-cil=5.18.0.240+dfsg-5 libmono-webmatrix-data4.0-cil=5.18.0.240+dfsg-5 libmono-windowsbase4.0-cil=5.18.0.240+dfsg-5 libmono-xbuild-tasks4.0-cil=5.18.0.240+dfsg-5 libmonoboehm-2.0-1=5.18.0.240+dfsg-5 libmonosgen-2.0-1=5.18.0.240+dfsg-5 libmonosgen-2.0-dev=5.18.0.240+dfsg-5 libmount1=2.34-0.1 libmpc3=1.1.0-1 libmpfr6=4.0.2-1 libncursesw6=6.1+20191019-1 libnet-http-perl=6.19-1 libnet-ssleay-perl=1.88-2 libnunit-cil-dev=2.6.4+dfsg-1 libnunit-console-runner2.6.3-cil=2.6.4+dfsg-1 libnunit-core-interfaces2.6.3-cil=2.6.4+dfsg-1 libnunit-core2.6.3-cil=2.6.4+dfsg-1 libnunit-framework2.6.3-cil=2.6.4+dfsg-1 libnunit-mocks2.6.3-cil=2.6.4+dfsg-1 libnunit-util2.6.3-cil=2.6.4+dfsg-1 libpam-modules=1.3.1-5 libpam-modules-bin=1.3.1-5 libpam-runtime=1.3.1-5 libpam0g=1.3.1-5 libpcre2-8-0=10.34-7 libpcre3=2:8.39-12+b1 libperl5.30=5.30.0-9 libpipeline1=1.5.1-3 libpixman-1-0=0.36.0-1 libpng16-16=1.6.37-1 libquadmath0=9.2.1-21 libseccomp2=2.4.2-2 libselinux1=3.0-1 libsigsegv2=2.12-2 libsmartcols1=2.34-0.1 libsqlite3-0=3.30.1-1 libssl1.1=1.1.1d-2 libstdc++-9-dev=9.2.1-21 libstdc++6=9.2.1-21 libsub-override-perl=0.09-2 libsystemd0=244-3 libtiff5=4.1.0+git191117-1 libtimedate-perl=2.3000-2 libtinfo6=6.1+20191019-1 libtool=2.4.6-11 libtry-tiny-perl=0.30-1 libtsan0=9.2.1-21 libubsan1=9.2.1-21 libuchardet0=0.0.6-3 libudev1=244-3 libunistring2=0.9.10-2 liburi-perl=1.76-1 libuuid1=2.34-0.1 libwebp6=0.6.1-2+b1 libwww-perl=6.43-1 libwww-robotrules-perl=6.02-1 libx11-6=2:1.6.8-1 libx11-data=2:1.6.8-1 libxau6=1:1.0.8-1+b2 libxcb-render0=1.13.1-2 libxcb-shm0=1.13.1-2 libxcb1=1.13.1-2 libxdmcp6=1:1.1.2-3 libxext6=2:1.3.3-1+b2 libxml-dom-perl=1.46-1 libxml-parser-perl=2.46-1+b1 libxml-perl=0.08-3 libxml-regexp-perl=0.04-1 libxml2=2.9.4+dfsg1-8 libxrender1=1:0.9.10-1 libzstd1=1.4.4+dfsg-1 linux-libc-dev=5.3.15-1 login=1:4.8-1 lsb-base=11.1.0 m4=1.4.18-4 make=4.2.1-1.2 man-db=2.9.0-2 mawk=1.3.3-17+b3 mono-4.0-gac=5.18.0.240+dfsg-5 mono-devel=5.18.0.240+dfsg-5 mono-gac=5.18.0.240+dfsg-5 mono-mcs=5.18.0.240+dfsg-5 mono-runtime=5.18.0.240+dfsg-5 mono-runtime-common=5.18.0.240+dfsg-5 mono-runtime-sgen=5.18.0.240+dfsg-5 mono-utils=5.18.0.240+dfsg-5 mono-xbuild=5.18.0.240+dfsg-5 ncurses-base=6.1+20191019-1 ncurses-bin=6.1+20191019-1 netbase=6.0 openssl=1.1.1d-2 patch=2.7.6-6 perl=5.30.0-9 perl-base=5.30.0-9 perl-modules-5.30=5.30.0-9 perl-openssl-defaults=3 pkg-config=0.29-6 po-debconf=1.0.21 sed=4.7-1 sensible-utils=0.0.12+nmu1 sysvinit-utils=2.96-1 tar=1.30+dfsg-6+b1 tzdata=2019c-3 ucf=3.0038+nmu1 util-linux=2.34-0.1 xz-utils=5.2.4-1+b1 zlib1g=1:1.2.11.dfsg-1+b1 --variant=apt --aptopt=Acquire::Check-Valid-Until "false" --aptopt=Acquire::http::Dl-Limit "1000"; --aptopt=Acquire::https::Dl-Limit "1000"; --aptopt=Acquire::Retries "5"; --aptopt=APT::Get::allow-downgrades "true"; --keyring=/usr/share/keyrings/ --essential-hook=chroot "$1" sh -c "apt-get --yes install fakeroot util-linux" --essential-hook=copy-in /usr/share/keyrings/debian-archive-bullseye-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-security-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-stable.gpg /usr/share/keyrings/debian-archive-buster-automatic.gpg /usr/share/keyrings/debian-archive-buster-security-automatic.gpg /usr/share/keyrings/debian-archive-buster-stable.gpg /usr/share/keyrings/debian-archive-keyring.gpg /usr/share/keyrings/debian-archive-removed-keys.gpg /usr/share/keyrings/debian-archive-stretch-automatic.gpg /usr/share/keyrings/debian-archive-stretch-security-automatic.gpg /usr/share/keyrings/debian-archive-stretch-stable.gpg /usr/share/keyrings/debian-ports-archive-keyring-removed.gpg /usr/share/keyrings/debian-ports-archive-keyring.gpg /usr/share/keyrings/debian-keyring.gpg /etc/apt/trusted.gpg.d/ --essential-hook=chroot "$1" sh -c "rm /etc/apt/sources.list && echo 'deb http://snapshot.notset.fr/archive/debian/20210814T212851Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20210814T212851Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20191227T155055Z/ unstable main' >> /etc/apt/sources.list && apt-get update" --customize-hook=chroot "$1" useradd --no-create-home -d /nonexistent -p "" builduser -s /bin/bash --customize-hook=chroot "$1" env sh -c "apt-get source --only-source -d boogie=2.4.1+dfsg-0.1 && mkdir -p /build/boogie-VWtJyQ && dpkg-source --no-check -x /*.dsc /build/boogie-VWtJyQ/boogie-2.4.1+dfsg && chown -R builduser:builduser /build/boogie-VWtJyQ" --customize-hook=chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/boogie-VWtJyQ/boogie-2.4.1+dfsg && env DEB_BUILD_OPTIONS="parallel=4" LANG="C.UTF-8" LC_ALL="C.UTF-8" SOURCE_DATE_EPOCH="1576502720" dpkg-buildpackage -uc -a amd64 --build=all" --customize-hook=sync-out /build/boogie-VWtJyQ /tmp/boogie-2.4.1+dfsg-0.1d27k1joe bullseye /dev/null deb http://snapshot.notset.fr/archive/debian/20191227T155055Z unstable main I: automatically chosen mode: root I: chroot architecture amd64 is equal to the host's architecture I: automatically chosen format: tar I: using /tmp/mmdebstrap.e11OzvtgvY as tempdir I: running apt-get update... I: downloading packages with apt... I: extracting archives... I: installing essential packages... I: running --essential-hook in shell: sh -c 'chroot "$1" sh -c "apt-get --yes install fakeroot util-linux"' exec /tmp/mmdebstrap.e11OzvtgvY Reading package lists... Building dependency tree... util-linux is already the newest version (2.34-0.1). The following NEW packages will be installed: fakeroot libfakeroot 0 upgraded, 2 newly installed, 0 to remove and 0 not upgraded. Need to get 132 kB of archives. After this operation, 393 kB of additional disk space will be used. Get:1 http://snapshot.notset.fr/archive/debian/20191227T155055Z unstable/main amd64 libfakeroot amd64 1.24-1 [45.7 kB] Get:2 http://snapshot.notset.fr/archive/debian/20191227T155055Z unstable/main amd64 fakeroot amd64 1.24-1 [85.9 kB] debconf: delaying package configuration, since apt-utils is not installed Fetched 132 kB in 0s (845 kB/s) Selecting previously unselected package libfakeroot:amd64. (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 ... 4508 files and directories currently installed.) Preparing to unpack .../libfakeroot_1.24-1_amd64.deb ... Unpacking libfakeroot:amd64 (1.24-1) ... Selecting previously unselected package fakeroot. Preparing to unpack .../fakeroot_1.24-1_amd64.deb ... Unpacking fakeroot (1.24-1) ... Setting up libfakeroot:amd64 (1.24-1) ... Setting up fakeroot (1.24-1) ... update-alternatives: using /usr/bin/fakeroot-sysv to provide /usr/bin/fakeroot (fakeroot) in auto mode Processing triggers for libc-bin (2.29-6) ... I: running special hook: copy-in /usr/share/keyrings/debian-archive-bullseye-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-security-automatic.gpg /usr/share/keyrings/debian-archive-bullseye-stable.gpg /usr/share/keyrings/debian-archive-buster-automatic.gpg /usr/share/keyrings/debian-archive-buster-security-automatic.gpg /usr/share/keyrings/debian-archive-buster-stable.gpg /usr/share/keyrings/debian-archive-keyring.gpg /usr/share/keyrings/debian-archive-removed-keys.gpg /usr/share/keyrings/debian-archive-stretch-automatic.gpg /usr/share/keyrings/debian-archive-stretch-security-automatic.gpg /usr/share/keyrings/debian-archive-stretch-stable.gpg /usr/share/keyrings/debian-ports-archive-keyring-removed.gpg /usr/share/keyrings/debian-ports-archive-keyring.gpg /usr/share/keyrings/debian-keyring.gpg /etc/apt/trusted.gpg.d/ I: running --essential-hook in shell: sh -c 'chroot "$1" sh -c "rm /etc/apt/sources.list && echo 'deb http://snapshot.notset.fr/archive/debian/20210814T212851Z/ bookworm main deb-src http://snapshot.notset.fr/archive/debian/20210814T212851Z/ bookworm main deb http://snapshot.notset.fr/archive/debian/20191227T155055Z/ unstable main' >> /etc/apt/sources.list && apt-get update"' exec /tmp/mmdebstrap.e11OzvtgvY Get:1 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm InRelease [81.6 kB] Hit:2 http://snapshot.notset.fr/archive/debian/20191227T155055Z unstable InRelease Ign:3 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main amd64 Packages Ign:3 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main Sources Ign:4 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main amd64 Packages Get:3 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main Sources [11.4 MB] Get:4 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main amd64 Packages [11.1 MB] Fetched 22.6 MB in 20s (1136 kB/s) Reading package lists... I: installing remaining packages inside the chroot... I: running --customize-hook in shell: sh -c 'chroot "$1" useradd --no-create-home -d /nonexistent -p "" builduser -s /bin/bash' exec /tmp/mmdebstrap.e11OzvtgvY I: running --customize-hook in shell: sh -c 'chroot "$1" env sh -c "apt-get source --only-source -d boogie=2.4.1+dfsg-0.1 && mkdir -p /build/boogie-VWtJyQ && dpkg-source --no-check -x /*.dsc /build/boogie-VWtJyQ/boogie-2.4.1+dfsg && chown -R builduser:builduser /build/boogie-VWtJyQ"' exec /tmp/mmdebstrap.e11OzvtgvY Reading package lists... NOTICE: 'boogie' packaging is maintained in the 'Git' version control system at: https://salsa.debian.org/debian/boogie.git Please use: git clone https://salsa.debian.org/debian/boogie.git to retrieve the latest (possibly unreleased) updates to the package. Need to get 1177 kB of source archives. Get:1 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main boogie 2.4.1+dfsg-0.1 (dsc) [1989 B] Get:2 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main boogie 2.4.1+dfsg-0.1 (tar) [1166 kB] Get:3 http://snapshot.notset.fr/archive/debian/20210814T212851Z bookworm/main boogie 2.4.1+dfsg-0.1 (diff) [9080 B] Fetched 1177 kB in 1s (1150 kB/s) Download complete and in download only mode W: Download is performed unsandboxed as root as file 'boogie_2.4.1+dfsg-0.1.dsc' couldn't be accessed by user '_apt'. - pkgAcquire::Run (13: Permission denied) dpkg-source: info: extracting boogie in /build/boogie-VWtJyQ/boogie-2.4.1+dfsg dpkg-source: info: unpacking boogie_2.4.1+dfsg.orig.tar.xz dpkg-source: info: unpacking boogie_2.4.1+dfsg-0.1.debian.tar.xz I: running --customize-hook in shell: sh -c 'chroot "$1" env --unset=TMPDIR runuser builduser -c "cd /build/boogie-VWtJyQ/boogie-2.4.1+dfsg && env DEB_BUILD_OPTIONS="parallel=4" LANG="C.UTF-8" LC_ALL="C.UTF-8" SOURCE_DATE_EPOCH="1576502720" dpkg-buildpackage -uc -a amd64 --build=all"' exec /tmp/mmdebstrap.e11OzvtgvY dpkg-buildpackage: info: source package boogie dpkg-buildpackage: info: source version 2.4.1+dfsg-0.1 dpkg-buildpackage: info: source distribution unstable dpkg-buildpackage: info: source changed by Fabian Wolff dpkg-source --before-build . fakeroot debian/rules clean dh clean --with cli dh_clean debian/rules build-indep dh build-indep --with cli dh_update_autotools_config -i dh_autoreconf -i debian/rules override_dh_auto_build make[1]: Entering directory '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg' # Apparently, the Mono C# compiler does not support pattern # matching yet. The proper thing to do here would be to patch # Witnesses.cs, but unfortunately, dpkg-source fails # spectacularly when it comes to patching files with DOS # (CRLF) line endings. Therefore, we need to do a "manual # patch" here: sed -i 's/is null/== null/g' Source/Concurrency/Witnesses.cs xbuild /p:TargetFrameworkVersion=v4.0 Source/Boogie.sln >>>> xbuild tool is deprecated and will be removed in future updates, use msbuild instead <<<< XBuild Engine Version 14.0 Mono, Version 5.18.0.240 Copyright (C) 2005-2013 Various Mono authors Build started 10/07/2021 12:10:20. __________________________________________________ Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Boogie.sln" (default target(s)): Target ValidateSolutionConfiguration: Building solution configuration "Checked|Mixed Platforms". Target Build: Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/CodeContractsExtender.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Created directory "bin/Checked/" Created directory "obj/Checked/" Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Checked/BoogieCodeContractsExtender.dll ../version.cs cce.cs obj/Checked/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /platform:AnyCPU /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Xml.Linq.dll /reference:/usr/lib/mono/4.0-api/System.Data.DataSetExtensions.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/obj/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/obj/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/CodeContractsExtender.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Model/Model.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Created directory "obj/Checked/" Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Checked/BoogieModel.dll Model.cs ModelParser.cs Properties/AssemblyInfo.cs ../version.cs obj/Checked/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /platform:AnyCPU /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Model/obj/Checked/BoogieModel.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieModel.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Model/obj/Checked/BoogieModel.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieModel.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Model/Model.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/Graph.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Created directory "bin/Checked/" Created directory "obj/Checked/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieCodeContractsExtender.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Checked/BoogieGraph.dll ../version.cs Graph.cs obj/Checked/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /platform:AnyCPU /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked//BoogieCodeContractsExtender.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/obj/Checked/BoogieGraph.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/obj/Checked/BoogieGraph.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/Graph.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/Basetypes.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Created directory "bin/Checked/" Created directory "obj/Checked/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieCodeContractsExtender.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Checked/BoogieBasetypes.dll ../version.cs BigDec.cs RoundingMode.cs BigNum.cs BigFloat.cs Rational.cs Set.cs obj/Checked/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /platform:AnyCPU /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Numerics.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked//BoogieCodeContractsExtender.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/obj/Checked/BoogieBasetypes.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/obj/Checked/BoogieBasetypes.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/Basetypes.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/ParserHelper.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Created directory "bin/Checked/" Created directory "obj/Checked/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieCodeContractsExtender.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Checked/BoogieParserHelper.dll ../version.cs ParserHelper.cs obj/Checked/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"TRACE;DEBUG" /nostdlib /platform:AnyCPU /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Xml.Linq.dll /reference:/usr/lib/mono/4.0-api/System.Data.DataSetExtensions.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked//BoogieCodeContractsExtender.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/obj/Checked/BoogieParserHelper.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/obj/Checked/BoogieParserHelper.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/ParserHelper.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ModelViewer/ModelViewer.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: x86 Created directory "obj/x86/Checked/" Target GenerateResources: Tool /usr/lib/mono/4.5/resgen.exe execution started with arguments: /useSourcePath /compile "Main.resx,obj/x86/Checked/Microsoft.Boogie.ModelViewer.Main.resources" Tool /usr/lib/mono/4.5/resgen.exe execution started with arguments: /useSourcePath /compile "Properties/Resources.resx,obj/x86/Checked/Microsoft.Boogie.ModelViewer.Properties.Resources.resources" Tool /usr/lib/mono/4.5/resgen.exe execution started with arguments: /useSourcePath /compile "SourceView.resx,obj/x86/Checked/Microsoft.Boogie.ModelViewer.SourceView.resources" Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/x86/Checked/BoogieModelViewer.dll /resource:obj/x86/Checked/Microsoft.Boogie.ModelViewer.Main.resources /resource:obj/x86/Checked/Microsoft.Boogie.ModelViewer.Properties.Resources.resources /resource:obj/x86/Checked/Microsoft.Boogie.ModelViewer.SourceView.resources BaseProvider.cs BCTProvider.cs DafnyProvider.cs DataModel.cs Main.cs Main.Designer.cs Namer.cs Properties/AssemblyInfo.cs SourceView.cs SourceView.Designer.cs TreeSkeleton.cs VccProvider.cs Properties/Resources.Designer.cs Properties/Settings.Designer.cs ../version.cs obj/x86/Checked/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /win32icon:bvdicon.ico /define:"DEBUG;TRACE" /nostdlib /platform:AnyCPU /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Numerics.dll /reference:/usr/lib/mono/4.0-api/System.Drawing.dll /reference:/usr/lib/mono/4.0-api/System.Windows.Forms.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries//BoogieModel.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 VccProvider.cs(811,13): warning CS0219: The variable `model' is assigned but its value is never used VccProvider.cs(952,15): warning CS0219: The variable `basePtr' is assigned but its value is never used BaseProvider.cs(46,25): warning CS0414: The private field `Microsoft.Boogie.ModelViewer.Base.BaseState.st' is assigned but its value is never used BCTProvider.cs(29,39): warning CS0414: The private field `Microsoft.Boogie.ModelViewer.BCT.BCTModel.typeName' is assigned but its value is never used DafnyProvider.cs(37,39): warning CS0414: The private field `Microsoft.Boogie.ModelViewer.Dafny.DafnyModel.typeName' is assigned but its value is never used Main.cs(276,25): warning CS0414: The private field `Microsoft.Boogie.ModelViewer.Main.center' is assigned but its value is never used VccProvider.cs(294,14): warning CS0414: The private field `Microsoft.Boogie.ModelViewer.Vcc.VccModel.state_props' is assigned but its value is never used Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ModelViewer/obj/x86/Checked/BoogieModelViewer.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieModelViewer.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ModelViewer/obj/x86/Checked/BoogieModelViewer.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieModelViewer.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ModelViewer/ModelViewer.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/Core.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Created directory "bin/Checked/" Created directory "obj/Checked/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieBasetypes.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieBasetypes.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCodeContractsExtender.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieGraph.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieGraph.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieParserHelper.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieParserHelper.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Checked/BoogieCore.dll Absy.cs AbsyCmd.cs AbsyExpr.cs AbsyQuant.cs AbsyType.cs AlphaEquality.cs CivlAttributes.cs InterProceduralReachabilityGraph.cs CommandLineOptions.cs DeadVarElim.cs Duplicator.cs Inline.cs LambdaHelper.cs MaxHolesLambdaLifter.cs LambdaLiftingMaxHolesFiller.cs LambdaLiftingTemplate.cs LoopUnroll.cs OOLongUtil.cs Parser.cs ResolutionContext.cs Scanner.cs StandardVisitor.cs TypeAmbiguitySeeker.cs Util.cs VariableDependenceAnalyser.cs VCExp.cs ../version.cs Xml.cs obj/Checked/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /platform:AnyCPU /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Numerics.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked//BoogieBasetypes.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked//BoogieCodeContractsExtender.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked//BoogieGraph.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked//BoogieParserHelper.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 AbsyExpr.cs(2228,16): warning CS0659: `Microsoft.Boogie.TypeCoercion' overrides Object.Equals(object) but does not override Object.GetHashCode() AbsyQuant.cs(678,25): warning CS0659: `Microsoft.Boogie.QuantifierExpr' overrides Object.Equals(object) but does not override Object.GetHashCode() AbsyType.cs(870,16): warning CS0659: `Microsoft.Boogie.BasicType' overrides Object.Equals(object) but does not override Object.GetHashCode() AbsyType.cs(3133,16): warning CS0659: `Microsoft.Boogie.CtorType' overrides Object.Equals(object) but does not override Object.GetHashCode() Absy.cs(3181,38): warning CS0219: The variable `entry' is assigned but its value is never used Absy.cs(4076,20): warning CS0219: The variable `StateName' is assigned but its value is never used Parser.cs(569,25): warning CS0219: The variable `tyds' is assigned but its value is never used Absy.cs(3273,40): warning CS0414: The private field `Microsoft.Boogie.LoopProcedure.blockMap' is assigned but its value is never used Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/obj/Checked/BoogieCore.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/obj/Checked/BoogieCore.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/Core.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/BVD/BVD.csproj" (default target(s)): Target PrepareForBuild: Configuration: Debug Platform: AnyCPU Created directory "obj/Debug/" Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /optimize- /out:obj/Debug/BVD.exe Program.cs Properties/AssemblyInfo.cs obj/Debug/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:winexe /define:"DEBUG;TRACE" /nostdlib /platform:AnyCPU /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Drawing.dll /reference:/usr/lib/mono/4.0-api/System.Numerics.dll /reference:/usr/lib/mono/4.0-api/System.Windows.Forms.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries//BoogieModelViewer.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 Target _CopyAppConfigFile: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/BVD/App.config' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BVD.exe.config' Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/BVD/obj/Debug/BVD.exe.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BVD.exe.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/BVD/obj/Debug/BVD.exe' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BVD.exe' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/BVD/BVD.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/BasetypesTests/BasetypesTests.csproj" (default target(s)): Target PrepareForBuild: Configuration: Debug Platform: AnyCPU Created directory "bin/Debug/" Created directory "obj/Debug/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/BasetypesTests/bin/Debug/BoogieBasetypes.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/BasetypesTests/bin/Debug/BoogieBasetypes.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/BasetypesTests/bin/Debug/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/BasetypesTests/bin/Debug/BoogieCodeContractsExtender.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /optimize- /out:obj/Debug/BasetypesTests.dll BigDecTests.cs Properties/AssemblyInfo.cs obj/Debug/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /reference:/usr/lib/cli/nunit.framework-2.6.3/nunit.framework.dll /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Numerics.dll /reference:/usr/lib/mono/4.0-api/System.Xml.Linq.dll /reference:/usr/lib/mono/4.0-api/System.Data.DataSetExtensions.dll /reference:/usr/lib/mono/4.0-api/Microsoft.CSharp.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked//BoogieBasetypes.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/BasetypesTests/obj/Debug/BasetypesTests.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/BasetypesTests/bin/Debug/BasetypesTests.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/BasetypesTests/obj/Debug/BasetypesTests.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/BasetypesTests/bin/Debug/BasetypesTests.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/BasetypesTests/BasetypesTests.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/AbsInt.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Created directory "bin/Checked/" Created directory "obj/Checked/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked/BoogieBasetypes.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked/BoogieBasetypes.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked/BoogieCodeContractsExtender.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked/BoogieCore.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked/BoogieCore.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked/BoogieParserHelper.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked/BoogieParserHelper.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieGraph.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked/BoogieGraph.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieGraph.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked/BoogieGraph.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Checked/BoogieAbsInt.dll IntervalDomain.cs TrivialDomain.cs NativeLattice.cs Traverse.cs ../version.cs obj/Checked/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /platform:AnyCPU /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Numerics.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked//BoogieBasetypes.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked//BoogieCodeContractsExtender.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked//BoogieCore.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked//BoogieParserHelper.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 IntervalDomain.cs(230,11): warning CS0472: The result of comparing value type `System.Numerics.BigInteger' with null is always `false' IntervalDomain.cs(231,9): warning CS0162: Unreachable code detected NativeLattice.cs(287,13): warning CS0219: The variable `conjuncts' is assigned but its value is never used Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/obj/Checked/BoogieAbsInt.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked/BoogieAbsInt.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/obj/Checked/BoogieAbsInt.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked/BoogieAbsInt.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/AbsInt.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/VCExpr.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Created directory "bin/Checked/" Created directory "obj/Checked/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieBasetypes.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieBasetypes.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieCodeContractsExtender.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieCore.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieCore.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieParserHelper.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieParserHelper.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieGraph.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieGraph.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieGraph.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieGraph.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Checked/BoogieVCExpr.dll ../version.cs BigLiteralAbstracter.cs Boogie2VCExpr.cs Clustering.cs LetBindingSorter.cs NameClashResolver.cs SimplifyLikeLineariser.cs TermFormulaFlattening.cs TypeErasure.cs TypeErasureArguments.cs TypeErasurePremisses.cs VCExprAST.cs VCExprASTPrinter.cs VCExprASTVisitors.cs obj/Checked/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /platform:AnyCPU /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked//BoogieBasetypes.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked//BoogieCodeContractsExtender.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked//BoogieCore.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked//BoogieParserHelper.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 VCExprASTVisitors.cs(365,18): warning CS0219: The variable `op' is assigned but its value is never used Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/obj/Checked/BoogieVCExpr.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieVCExpr.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/obj/Checked/BoogieVCExpr.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieVCExpr.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/VCExpr.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/Concurrency.csproj" (default target(s)): Target PrepareForBuild: Configuration: Debug Platform: AnyCPU Created directory "bin/Debug/" Created directory "obj/Debug/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug/BoogieBasetypes.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug/BoogieBasetypes.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug/BoogieCore.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug/BoogieCore.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug/BoogieGraph.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug/BoogieGraph.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug/BoogieParserHelper.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug/BoogieParserHelper.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug/BoogieCodeContractsExtender.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Debug/BoogieConcurrency.dll GlobalSnapshotInstrumentation.cs YieldingProcInstrumentation.cs LinearTypeChecker.cs MoverCheck.cs YieldingProcChecker.cs CivlVCGeneration.cs Properties/AssemblyInfo.cs RefinementInstrumentation.cs SimulationRelation.cs CivlTypeChecker.cs TransitionRelationComputation.cs NoninterferenceInstrumentation.cs YieldingProcDuplicator.cs YieldTypeChecker.cs CivlUtil.cs Witnesses.cs obj/Debug/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"TRACE;DEBUG" /nostdlib /platform:AnyCPU /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Xml.Linq.dll /reference:/usr/lib/mono/4.0-api/System.Data.DataSetExtensions.dll /reference:/usr/lib/mono/4.0-api/Microsoft.CSharp.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked//BoogieBasetypes.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked//BoogieCore.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked//BoogieGraph.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked//BoogieParserHelper.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 Target _CopyAppConfigFile: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/App.config' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug/BoogieConcurrency.dll.config' Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/obj/Debug/BoogieConcurrency.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug/BoogieConcurrency.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/obj/Debug/BoogieConcurrency.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug/BoogieConcurrency.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/Concurrency.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/TestUtil.csproj" (default target(s)): Target PrepareForBuild: Configuration: Debug Platform: AnyCPU Created directory "bin/Debug/" Created directory "obj/Debug/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/bin/Debug/BoogieCore.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/bin/Debug/BoogieCore.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/bin/Debug/BoogieParserHelper.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/bin/Debug/BoogieParserHelper.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieGraph.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/bin/Debug/BoogieGraph.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieGraph.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/bin/Debug/BoogieGraph.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieBasetypes.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/bin/Debug/BoogieBasetypes.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieBasetypes.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/bin/Debug/BoogieBasetypes.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/bin/Debug/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/bin/Debug/BoogieCodeContractsExtender.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /optimize- /out:obj/Debug/TestUtil.dll AssertionTextWriterTraceListener.cs BoogieTestBase.cs ProgramLoader.cs Properties/AssemblyInfo.cs obj/Debug/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /reference:/usr/lib/cli/nunit.framework-2.6.3/nunit.framework.dll /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Xml.Linq.dll /reference:/usr/lib/mono/4.0-api/System.Data.DataSetExtensions.dll /reference:/usr/lib/mono/4.0-api/Microsoft.CSharp.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked//BoogieCore.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked//BoogieParserHelper.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/obj/Debug/TestUtil.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/bin/Debug/TestUtil.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/obj/Debug/TestUtil.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/bin/Debug/TestUtil.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/TestUtil.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/VCGeneration.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Created directory "bin/Checked/" Created directory "obj/Checked/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieBasetypes.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieBasetypes.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieCodeContractsExtender.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieCore.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieCore.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieGraph.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieGraph.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieModel.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieModel.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieModel.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieModel.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieParserHelper.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieParserHelper.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieVCExpr.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCExpr.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieVCExpr.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCExpr.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Checked/BoogieVCGeneration.dll Check.cs ConditionGeneration.cs Context.cs ExprExtensions.cs FixedpointVC.cs OrderingAxioms.cs RPFP.cs StratifiedVC.cs VC.cs ../version.cs Wlp.cs obj/Checked/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /platform:AnyCPU /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked//BoogieBasetypes.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked//BoogieCodeContractsExtender.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked//BoogieCore.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked//BoogieGraph.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries//BoogieModel.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked//BoogieParserHelper.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked//BoogieVCExpr.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 ConditionGeneration.cs(1589,15): warning CS0219: The variable `subsumption' is assigned but its value is never used Context.cs(149,21): warning CS0219: The variable `cmds' is assigned but its value is never used FixedpointVC.cs(279,17): warning CS0219: The variable `thing' is assigned but its value is never used FixedpointVC.cs(690,30): warning CS0219: The variable `freePostExpr' is assigned but its value is never used FixedpointVC.cs(748,32): warning CS0219: The variable `exprs' is assigned but its value is never used FixedpointVC.cs(1078,29): warning CS0219: The variable `r' is assigned but its value is never used FixedpointVC.cs(1664,21): warning CS0219: The variable `id' is assigned but its value is never used FixedpointVC.cs(2036,24): warning CS0219: The variable `implName' is assigned but its value is never used FixedpointVC.cs(2102,23): warning CS0219: The variable `vvar' is assigned but its value is never used RPFP.cs(459,18): warning CS0219: The variable `body' is assigned but its value is never used StratifiedVC.cs(121,25): warning CS0219: The variable `sortedNodes' is assigned but its value is never used VC.cs(166,41): warning CS0429: Unreachable expression code detected VC.cs(169,13): warning CS0162: Unreachable code detected VC.cs(1496,40): warning CS0219: The variable `gotoCmdOrigins' is assigned but its value is never used VC.cs(1604,17): warning CS0219: The variable `watch' is assigned but its value is never used FixedpointVC.cs(57,48): warning CS0414: The private field `Microsoft.Boogie.FixedpointVC.gen' is assigned but its value is never used StratifiedVC.cs(2093,20): warning CS0414: The private field `VC.StratifiedVCGen.StratifiedInliningErrorReporter.mainVC' is assigned but its value is never used VC.cs(522,20): warning CS0414: The private field `VC.VCGen.Split.id' is assigned but its value is never used Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/obj/Checked/BoogieVCGeneration.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCGeneration.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/obj/Checked/BoogieVCGeneration.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCGeneration.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/VCGeneration.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/CoreTests.csproj" (default target(s)): Target PrepareForBuild: Configuration: Debug Platform: AnyCPU Created directory "bin/Debug/" Created directory "obj/Debug/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/bin/Debug/BoogieBasetypes.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/bin/Debug/BoogieBasetypes.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/bin/Debug/BoogieCore.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/bin/Debug/BoogieCore.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/bin/Debug/BoogieParserHelper.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/bin/Debug/BoogieParserHelper.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/bin/Debug/TestUtil.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/bin/Debug/TestUtil.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/bin/Debug/TestUtil.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/bin/Debug/TestUtil.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/bin/Debug/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/bin/Debug/BoogieCodeContractsExtender.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieGraph.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/bin/Debug/BoogieGraph.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieGraph.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/bin/Debug/BoogieGraph.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /optimize- /out:obj/Debug/CoreTests.dll AbsyMetadata.cs Duplicator.cs ExprEquality.cs Properties/AssemblyInfo.cs ExprTypeChecking.cs ExprImmutability.cs obj/Debug/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /reference:/usr/lib/cli/nunit.framework-2.6.3/nunit.framework.dll /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Xml.Linq.dll /reference:/usr/lib/mono/4.0-api/System.Data.DataSetExtensions.dll /reference:/usr/lib/mono/4.0-api/Microsoft.CSharp.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked//BoogieBasetypes.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked//BoogieCore.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked//BoogieParserHelper.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/TestUtil/bin/Debug//TestUtil.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/obj/Debug/CoreTests.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/bin/Debug/CoreTests.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/obj/Debug/CoreTests.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/bin/Debug/CoreTests.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/UnitTests/CoreTests/CoreTests.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/SMTLib.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Created directory "bin/Checked/" Created directory "obj/Checked/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieBasetypes.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieBasetypes.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieCodeContractsExtender.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieCore.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieCore.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieGraph.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieGraph.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieModel.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieModel.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieModel.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieModel.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieParserHelper.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieParserHelper.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieVCExpr.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieVCExpr.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieVCExpr.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieVCExpr.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCGeneration.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieVCGeneration.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCGeneration.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/BoogieVCGeneration.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../../InterimKey.snk /publicsign /optimize- /out:obj/Checked/Provers.SMTLib.dll Inspector.cs SMTLibProverOptions.cs ProverInterface.cs SExpr.cs SMTLibLineariser.cs SMTLibNamer.cs SMTLibProcess.cs TypeDeclCollector.cs ../../version.cs Z3.cs CVC4.cs obj/Checked/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /platform:AnyCPU /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Numerics.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked//BoogieBasetypes.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked//BoogieCodeContractsExtender.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked//BoogieCore.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked//BoogieGraph.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries//BoogieModel.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked//BoogieParserHelper.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked//BoogieVCExpr.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked//BoogieVCGeneration.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 ProverInterface.cs(666,15): warning CS0219: The variable `gb' is assigned but its value is never used TypeDeclCollector.cs(22,42): warning CS0414: The private field `Microsoft.Boogie.SMTLib.TypeDeclCollector.Options' is assigned but its value is never used Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/obj/Checked/Provers.SMTLib.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/Provers.SMTLib.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/obj/Checked/Provers.SMTLib.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/Provers.SMTLib.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/SMTLib.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/Predication.csproj" (default target(s)): Target PrepareForBuild: Configuration: Debug Platform: AnyCPU Created directory "bin/Debug/" Created directory "obj/Debug/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieBasetypes.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieBasetypes.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieCore.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieCore.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieGraph.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieGraph.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieParserHelper.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieParserHelper.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCGeneration.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieVCGeneration.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCGeneration.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieVCGeneration.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieCodeContractsExtender.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCExpr.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieVCExpr.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCExpr.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieVCExpr.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieModel.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieModel.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieModel.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogieModel.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Debug/BoogiePredication.dll SmartBlockPredicator.cs UniformityAnalyser.cs obj/Debug/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Xml.Linq.dll /reference:/usr/lib/mono/4.0-api/System.Data.DataSetExtensions.dll /reference:/usr/lib/mono/4.0-api/Microsoft.CSharp.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked//BoogieBasetypes.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked//BoogieCore.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked//BoogieGraph.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked//BoogieParserHelper.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked//BoogieVCGeneration.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/obj/Debug/BoogiePredication.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogiePredication.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/obj/Debug/BoogiePredication.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogiePredication.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/Predication.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/Doomed.csproj" (default target(s)): Target PrepareForBuild: Configuration: Debug Platform: AnyCPU Created directory "bin/Debug/" Created directory "obj/Debug/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieBasetypes.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieBasetypes.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieCodeContractsExtender.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieCore.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieCore.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieGraph.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieGraph.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieModel.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieModel.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieModel.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieModel.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieParserHelper.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieParserHelper.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieVCExpr.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieVCExpr.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieVCExpr.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieVCExpr.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCGeneration.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieVCGeneration.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCGeneration.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieVCGeneration.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Debug/BoogieDoomed.dll DoomCheck.cs DoomedLoopUnrolling.cs DoomedStrategy.cs DoomErrorHandler.cs HasseDiagram.cs VCDoomed.cs obj/Debug/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Xml.Linq.dll /reference:/usr/lib/mono/4.0-api/System.Data.DataSetExtensions.dll /reference:/usr/lib/mono/4.0-api/Microsoft.CSharp.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked//BoogieBasetypes.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked//BoogieCodeContractsExtender.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked//BoogieCore.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked//BoogieGraph.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries//BoogieModel.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked//BoogieParserHelper.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked//BoogieVCExpr.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked//BoogieVCGeneration.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 DoomErrorHandler.cs(69,29): warning CS0219: The variable `assertNodes' is assigned but its value is never used VCDoomed.cs(736,19): warning CS0219: The variable `cs' is assigned but its value is never used DoomedStrategy.cs(305,21): warning CS0414: The private field `VC.PathCoverStrategy.m_Ignore' is assigned but its value is never used DoomedStrategy.cs(307,16): warning CS0414: The private field `VC.PathCoverStrategy.m_Random' is assigned but its value is never used DoomedStrategy.cs(310,29): warning CS0414: The private field `VC.PathCoverStrategy.m_foundBlock' is assigned but its value is never used DoomedStrategy.cs(413,21): warning CS0414: The private field `VC.PathCoverStrategyK.m_Ignore' is assigned but its value is never used DoomedStrategy.cs(415,16): warning CS0414: The private field `VC.PathCoverStrategyK.m_Random' is assigned but its value is never used DoomedStrategy.cs(418,29): warning CS0414: The private field `VC.PathCoverStrategyK.m_foundBlock' is assigned but its value is never used VCDoomed.cs(23,45): warning CS0414: The private field `VC.DCGen.m_copiedBlocks' is assigned but its value is never used VCDoomed.cs(25,25): warning CS0414: The private field `VC.DCGen.m_doomedCmds' is assigned but its value is never used Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/obj/Debug/BoogieDoomed.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieDoomed.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/obj/Debug/BoogieDoomed.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieDoomed.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/Doomed.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/Houdini.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Created directory "bin/Checked/" Created directory "obj/Checked/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieBasetypes.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieBasetypes.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieCodeContractsExtender.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieCore.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieCore.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieGraph.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieGraph.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieModel.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieModel.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieModel.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieModel.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieParserHelper.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieParserHelper.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/Provers.SMTLib.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/Provers.SMTLib.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/Provers.SMTLib.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/Provers.SMTLib.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieVCExpr.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieVCExpr.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked/BoogieVCExpr.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieVCExpr.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCGeneration.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieVCGeneration.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCGeneration.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieVCGeneration.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Checked/BoogieHoudini.dll ../version.cs AbstractHoudini.cs Checker.cs AnnotationDependenceAnalyser.cs Houdini.cs StagedHoudini.cs ConcurrentHoudini.cs obj/Checked/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /nostdlib /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Xml.Linq.dll /reference:/usr/lib/mono/4.0-api/System.Data.DataSetExtensions.dll /reference:/usr/lib/mono/4.0-api/Microsoft.CSharp.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked//BoogieBasetypes.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked//BoogieCodeContractsExtender.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked//BoogieCore.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked//BoogieGraph.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries//BoogieModel.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked//BoogieParserHelper.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked//Provers.SMTLib.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked//BoogieVCExpr.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked//BoogieVCGeneration.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 AbstractHoudini.cs(315,27): warning CS0219: The variable `failingProcedure' is assigned but its value is never used AbstractHoudini.cs(2110,25): warning CS0219: The variable `top' is assigned but its value is never used AbstractHoudini.cs(3388,25): warning CS0219: The variable `pos' is assigned but its value is never used AbstractHoudini.cs(2274,25): warning CS0414: The private field `Microsoft.Boogie.Houdini.AbstractHoudini.summaryClass' is assigned but its value is never used AbstractHoudini.cs(3110,17): warning CS0414: The private field `Microsoft.Boogie.Houdini.ConstantVal.program' is assigned but its value is never used AbstractHoudini.cs(3111,24): warning CS0414: The private field `Microsoft.Boogie.Houdini.ConstantVal.impl' is assigned but its value is never used AnnotationDependenceAnalyser.cs(764,21): warning CS0414: The private field `Microsoft.Boogie.Houdini.AnnotationReachabilityChecker.prog' is assigned but its value is never used AnnotationDependenceAnalyser.cs(765,33): warning CS0414: The private field `Microsoft.Boogie.Houdini.AnnotationReachabilityChecker.AnnotationIdentifiers' is assigned but its value is never used Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/obj/Checked/BoogieHoudini.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieHoudini.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/Houdini.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ExecutionEngine/ExecutionEngine.csproj" (default target(s)): Target PrepareForBuild: Configuration: Debug Platform: AnyCPU Created directory "obj/Debug/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked/BoogieAbsInt.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieAbsInt.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked/BoogieAbsInt.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieAbsInt.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieBasetypes.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked/BoogieBasetypes.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieBasetypes.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieCodeContractsExtender.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked/BoogieCodeContractsExtender.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieCodeContractsExtender.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieCore.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked/BoogieCore.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieCore.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieGraph.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked/BoogieGraph.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieGraph.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieHoudini.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieHoudini.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieParserHelper.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked/BoogieParserHelper.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieParserHelper.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCGeneration.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieVCGeneration.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked/BoogieVCGeneration.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieVCGeneration.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug/BoogieConcurrency.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieConcurrency.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug/BoogieConcurrency.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieConcurrency.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieDoomed.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieDoomed.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug/BoogieDoomed.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieDoomed.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogiePredication.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogiePredication.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug/BoogiePredication.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogiePredication.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieVCExpr.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieVCExpr.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked/BoogieVCExpr.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieVCExpr.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Debug/BoogieExecutionEngine.dll ExecutionEngine.cs Properties/AssemblyInfo.cs ThreadTaskScheduler.cs VerificationResultCache.cs obj/Debug/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:library /define:"DEBUG;TRACE" /nostdlib /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Runtime.Caching.dll /reference:/usr/lib/mono/4.0-api/System.Xml.Linq.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked//BoogieAbsInt.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked//BoogieBasetypes.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked//BoogieCodeContractsExtender.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked//BoogieCore.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked//BoogieGraph.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked//BoogieHoudini.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries//BoogieModel.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked//BoogieParserHelper.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked//BoogieVCGeneration.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Concurrency/bin/Debug//BoogieConcurrency.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug//BoogieDoomed.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug//BoogiePredication.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ExecutionEngine/obj/Debug/BoogieExecutionEngine.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieExecutionEngine.dll.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ExecutionEngine/obj/Debug/BoogieExecutionEngine.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/BoogieExecutionEngine.dll' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ExecutionEngine/ExecutionEngine.csproj". Project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/BoogieDriver/BoogieDriver.csproj" (default target(s)): Target PrepareForBuild: Configuration: Checked Platform: AnyCPU Created directory "obj/Checked/" Target CopyFilesMarkedCopyLocal: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/Provers.SMTLib.dll' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/Provers.SMTLib.dll' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked/Provers.SMTLib.dll.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/Provers.SMTLib.dll.mdb' Target GenerateSatelliteAssemblies: No input files were specified for target GenerateSatelliteAssemblies, skipping. Target CoreCompile: Tool /usr/lib/mono/4.5/mcs.exe execution started with arguments: /noconfig /debug:full /debug:portable /keyfile:../InterimKey.snk /publicsign /optimize- /out:obj/Checked/Boogie.exe BoogieDriver.cs ../version.cs obj/Checked/.NETFramework,Version=v4.0.AssemblyAttribute.cs /target:exe /define:"DEBUG;TRACE" /nostdlib /platform:AnyCPU /reference:/usr/lib/mono/4.0-api/System.dll /reference:/usr/lib/mono/4.0-api/System.Data.dll /reference:/usr/lib/mono/4.0-api/System.Xml.dll /reference:/usr/lib/mono/4.0-api/System.Core.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/bin/Checked//BoogieAbsInt.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Basetypes/bin/Checked//BoogieBasetypes.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/CodeContractsExtender/bin/Checked//BoogieCodeContractsExtender.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/bin/Checked//BoogieCore.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Graph/bin/Checked//BoogieGraph.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/bin/Checked//BoogieHoudini.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ParserHelper/bin/Checked//BoogieParserHelper.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/bin/Checked//Provers.SMTLib.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/bin/Checked//BoogieVCExpr.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/bin/Checked//BoogieVCGeneration.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/bin/Debug//BoogieDoomed.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries//BoogieExecutionEngine.dll /reference:/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Predication/bin/Debug//BoogiePredication.dll /reference:/usr/lib/mono/4.0-api//mscorlib.dll /warn:4 Target _CopyAppConfigFile: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/BoogieDriver/app.config' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/Boogie.exe.config' Target DeployOutputFiles: Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/BoogieDriver/obj/Checked/Boogie.exe.mdb' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/Boogie.exe.mdb' Copying file from '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/BoogieDriver/obj/Checked/Boogie.exe' to '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Binaries/Boogie.exe' Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/BoogieDriver/BoogieDriver.csproj". Done building project "/build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Boogie.sln". Build succeeded. Warnings: /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Boogie.sln (default targets) -> (Build target) -> /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/ModelViewer/ModelViewer.csproj (default targets) -> /usr/lib/mono/xbuild/14.0/bin/Microsoft.CSharp.targets (CoreCompile target) -> VccProvider.cs(811,13): warning CS0219: The variable `model' is assigned but its value is never used VccProvider.cs(952,15): warning CS0219: The variable `basePtr' is assigned but its value is never used BaseProvider.cs(46,25): warning CS0414: The private field `Microsoft.Boogie.ModelViewer.Base.BaseState.st' is assigned but its value is never used BCTProvider.cs(29,39): warning CS0414: The private field `Microsoft.Boogie.ModelViewer.BCT.BCTModel.typeName' is assigned but its value is never used DafnyProvider.cs(37,39): warning CS0414: The private field `Microsoft.Boogie.ModelViewer.Dafny.DafnyModel.typeName' is assigned but its value is never used Main.cs(276,25): warning CS0414: The private field `Microsoft.Boogie.ModelViewer.Main.center' is assigned but its value is never used VccProvider.cs(294,14): warning CS0414: The private field `Microsoft.Boogie.ModelViewer.Vcc.VccModel.state_props' is assigned but its value is never used /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Boogie.sln (default targets) -> (Build target) -> /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Core/Core.csproj (default targets) -> /usr/lib/mono/xbuild/14.0/bin/Microsoft.CSharp.targets (CoreCompile target) -> AbsyExpr.cs(2228,16): warning CS0659: `Microsoft.Boogie.TypeCoercion' overrides Object.Equals(object) but does not override Object.GetHashCode() AbsyQuant.cs(678,25): warning CS0659: `Microsoft.Boogie.QuantifierExpr' overrides Object.Equals(object) but does not override Object.GetHashCode() AbsyType.cs(870,16): warning CS0659: `Microsoft.Boogie.BasicType' overrides Object.Equals(object) but does not override Object.GetHashCode() AbsyType.cs(3133,16): warning CS0659: `Microsoft.Boogie.CtorType' overrides Object.Equals(object) but does not override Object.GetHashCode() Absy.cs(3181,38): warning CS0219: The variable `entry' is assigned but its value is never used Absy.cs(4076,20): warning CS0219: The variable `StateName' is assigned but its value is never used Parser.cs(569,25): warning CS0219: The variable `tyds' is assigned but its value is never used Absy.cs(3273,40): warning CS0414: The private field `Microsoft.Boogie.LoopProcedure.blockMap' is assigned but its value is never used /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Boogie.sln (default targets) -> (Build target) -> /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/AbsInt/AbsInt.csproj (default targets) -> /usr/lib/mono/xbuild/14.0/bin/Microsoft.CSharp.targets (CoreCompile target) -> IntervalDomain.cs(230,11): warning CS0472: The result of comparing value type `System.Numerics.BigInteger' with null is always `false' IntervalDomain.cs(231,9): warning CS0162: Unreachable code detected NativeLattice.cs(287,13): warning CS0219: The variable `conjuncts' is assigned but its value is never used /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Boogie.sln (default targets) -> (Build target) -> /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCExpr/VCExpr.csproj (default targets) -> /usr/lib/mono/xbuild/14.0/bin/Microsoft.CSharp.targets (CoreCompile target) -> VCExprASTVisitors.cs(365,18): warning CS0219: The variable `op' is assigned but its value is never used /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Boogie.sln (default targets) -> (Build target) -> /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/VCGeneration/VCGeneration.csproj (default targets) -> /usr/lib/mono/xbuild/14.0/bin/Microsoft.CSharp.targets (CoreCompile target) -> ConditionGeneration.cs(1589,15): warning CS0219: The variable `subsumption' is assigned but its value is never used Context.cs(149,21): warning CS0219: The variable `cmds' is assigned but its value is never used FixedpointVC.cs(279,17): warning CS0219: The variable `thing' is assigned but its value is never used FixedpointVC.cs(690,30): warning CS0219: The variable `freePostExpr' is assigned but its value is never used FixedpointVC.cs(748,32): warning CS0219: The variable `exprs' is assigned but its value is never used FixedpointVC.cs(1078,29): warning CS0219: The variable `r' is assigned but its value is never used FixedpointVC.cs(1664,21): warning CS0219: The variable `id' is assigned but its value is never used FixedpointVC.cs(2036,24): warning CS0219: The variable `implName' is assigned but its value is never used FixedpointVC.cs(2102,23): warning CS0219: The variable `vvar' is assigned but its value is never used RPFP.cs(459,18): warning CS0219: The variable `body' is assigned but its value is never used StratifiedVC.cs(121,25): warning CS0219: The variable `sortedNodes' is assigned but its value is never used VC.cs(166,41): warning CS0429: Unreachable expression code detected VC.cs(169,13): warning CS0162: Unreachable code detected VC.cs(1496,40): warning CS0219: The variable `gotoCmdOrigins' is assigned but its value is never used VC.cs(1604,17): warning CS0219: The variable `watch' is assigned but its value is never used FixedpointVC.cs(57,48): warning CS0414: The private field `Microsoft.Boogie.FixedpointVC.gen' is assigned but its value is never used StratifiedVC.cs(2093,20): warning CS0414: The private field `VC.StratifiedVCGen.StratifiedInliningErrorReporter.mainVC' is assigned but its value is never used VC.cs(522,20): warning CS0414: The private field `VC.VCGen.Split.id' is assigned but its value is never used /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Boogie.sln (default targets) -> (Build target) -> /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Provers/SMTLib/SMTLib.csproj (default targets) -> /usr/lib/mono/xbuild/14.0/bin/Microsoft.CSharp.targets (CoreCompile target) -> ProverInterface.cs(666,15): warning CS0219: The variable `gb' is assigned but its value is never used TypeDeclCollector.cs(22,42): warning CS0414: The private field `Microsoft.Boogie.SMTLib.TypeDeclCollector.Options' is assigned but its value is never used /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Boogie.sln (default targets) -> (Build target) -> /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Doomed/Doomed.csproj (default targets) -> /usr/lib/mono/xbuild/14.0/bin/Microsoft.CSharp.targets (CoreCompile target) -> DoomErrorHandler.cs(69,29): warning CS0219: The variable `assertNodes' is assigned but its value is never used VCDoomed.cs(736,19): warning CS0219: The variable `cs' is assigned but its value is never used DoomedStrategy.cs(305,21): warning CS0414: The private field `VC.PathCoverStrategy.m_Ignore' is assigned but its value is never used DoomedStrategy.cs(307,16): warning CS0414: The private field `VC.PathCoverStrategy.m_Random' is assigned but its value is never used DoomedStrategy.cs(310,29): warning CS0414: The private field `VC.PathCoverStrategy.m_foundBlock' is assigned but its value is never used DoomedStrategy.cs(413,21): warning CS0414: The private field `VC.PathCoverStrategyK.m_Ignore' is assigned but its value is never used DoomedStrategy.cs(415,16): warning CS0414: The private field `VC.PathCoverStrategyK.m_Random' is assigned but its value is never used DoomedStrategy.cs(418,29): warning CS0414: The private field `VC.PathCoverStrategyK.m_foundBlock' is assigned but its value is never used VCDoomed.cs(23,45): warning CS0414: The private field `VC.DCGen.m_copiedBlocks' is assigned but its value is never used VCDoomed.cs(25,25): warning CS0414: The private field `VC.DCGen.m_doomedCmds' is assigned but its value is never used /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Boogie.sln (default targets) -> (Build target) -> /build/boogie-VWtJyQ/boogie-2.4.1+dfsg/Source/Houdini/Houdini.csproj (default targets) -> /usr/lib/mono/xbuild/14.0/bin/Microsoft.CSharp.targets (CoreCompile target) -> AbstractHoudini.cs(315,27): warning CS0219: The variable `failingProcedure' is assigned but its value is never used AbstractHoudini.cs(2110,25): warning CS0219: The variable `top' is assigned but its value is never used AbstractHoudini.cs(3388,25): warning CS0219: The variable `pos' is assigned but its value is never used AbstractHoudini.cs(2274,25): warning CS0414: The private field `Microsoft.Boogie.Houdini.AbstractHoudini.summaryClass' is assigned but its value is never used AbstractHoudini.cs(3110,17): warning CS0414: The private field `Microsoft.Boogie.Houdini.ConstantVal.program' is assigned but its value is never used AbstractHoudini.cs(3111,24): warning CS0414: The private field `Microsoft.Boogie.Houdini.ConstantVal.impl' is assigned but its value is never used AnnotationDependenceAnalyser.cs(764,21): warning CS0414: The private field `Microsoft.Boogie.Houdini.AnnotationReachabilityChecker.prog' is assigned but its value is never used AnnotationDependenceAnalyser.cs(765,33): warning CS0414: The private field `Microsoft.Boogie.Houdini.AnnotationReachabilityChecker.AnnotationIdentifiers' is assigned but its value is never used 57 Warning(s) 0 Error(s) Time Elapsed 00:00:34.4980850 sed -i 's/is null/== null/g' Source/Concurrency/Witnesses.cs make[1]: Leaving directory '/build/boogie-VWtJyQ/boogie-2.4.1+dfsg' create-stamp debian/debhelper-build-stamp fakeroot debian/rules binary-indep dh binary-indep --with cli dh_testroot -i dh_prep -i dh_install -i dh_installdocs -i dh_installchangelogs -i dh_installman -i dh_perl -i dh_link -i dh_strip_nondeterminism -i dh_compress -i dh_fixperms -i dh_clifixperms -i dh_missing -i dh_clistrip -i dh_makeclilibs -i dh_clideps -i dh_installdeb -i dh_gencontrol -i dh_md5sums -i dh_builddeb -i dpkg-deb: building package 'libboogie-cil' in '../libboogie-cil_2.4.1+dfsg-0.1_all.deb'. dpkg-deb: building package 'boogie' in '../boogie_2.4.1+dfsg-0.1_all.deb'. dpkg-genbuildinfo --build=all dpkg-genchanges --build=all >../boogie_2.4.1+dfsg-0.1_all.changes dpkg-genchanges: info: binary-only arch-indep upload (source code and arch-specific packages not included) dpkg-source --after-build . dpkg-buildpackage: info: binary-only upload (no source included) I: running special hook: sync-out /build/boogie-VWtJyQ /tmp/boogie-2.4.1+dfsg-0.1d27k1joe I: cleaning package lists and apt cache... I: creating tarball... I: done I: removing tempdir /tmp/mmdebstrap.e11OzvtgvY... I: success in 402.8755 seconds md5: boogie_2.4.1+dfsg-0.1_all.deb: OK md5: Value of 'md5' differs for libboogie-cil_2.4.1+dfsg-0.1_all.deb md5: Size differs for libboogie-cil_2.4.1+dfsg-0.1_all.deb sha1: boogie_2.4.1+dfsg-0.1_all.deb: OK sha1: Value of 'sha1' differs for libboogie-cil_2.4.1+dfsg-0.1_all.deb sha1: Size differs for libboogie-cil_2.4.1+dfsg-0.1_all.deb sha256: boogie_2.4.1+dfsg-0.1_all.deb: OK sha256: Value of 'sha256' differs for libboogie-cil_2.4.1+dfsg-0.1_all.deb sha256: Size differs for libboogie-cil_2.4.1+dfsg-0.1_all.deb Checksums: FAIL diffoscope run passed