Gentoo Websites Logo
Go to: Gentoo Home Documentation Forums Lists Bugs Planet Store Wiki Get Gentoo!

Bug 921948

Summary: dev-lang/boogie-3.0.8: fails prover/z3-hard-timeout.bpl test
Product: Gentoo Linux Reporter: Sam James <sam>
Component: Current packagesAssignee: dotnet project <dotnet>
Status: RESOLVED FIXED    
Severity: normal    
Priority: Normal    
Version: unspecified   
Hardware: All   
OS: Linux   
Whiteboard:
Package list:
Runtime testing required: ---
Bug Depends on:    
Bug Blocks: 921420    
Attachments: build.log

Description Sam James archtester Gentoo Infrastructure gentoo-dev Security 2024-01-12 17:54:51 UTC 
Created attachment 882120 [details]
build.log

Failed Tests (1):
  Boogie :: prover/z3-hard-timeout.bpl


Testing Time: 106.27s
  Unsupported      :  13
  Passed           : 575
  Expectedly Failed:   2
  Failed           :   1
 [ !! ]
 * ERROR: dev-lang/boogie-3.0.8::gentoo failed (test phase):
 *   Failed to run command: lit --order=lexical --time-tests --verbose --workers=4 /var/tmp/portage/dev-lang/boogie-3.0.8/work/boogie-3.0.8/Test
 *

----

# emerge --info
Portage 3.0.59 (python 3.11.7-final-0, default/linux/amd64/17.1/systemd, gcc-13, glibc-2.38-r9, 6.6.11 x86_64)
=================================================================
System uname: Linux-6.6.11-x86_64-AMD_Ryzen_9_3950X_16-Core_Processor-with-glibc2.38
KiB Mem:    65758036 total,   4800500 free
KiB Swap:   16662520 total,    472056 free
Timestamp of repository gentoo: Fri, 12 Jan 2024 17:20:16 +0000
sh bash 5.1_p16-r6
ld GNU ld (Gentoo 2.41 p2) 2.41.0
app-misc/pax-utils:        1.3.5::gentoo
app-shells/bash:           5.1_p16-r6::gentoo
dev-java/java-config:      2.3.3-r1::gentoo
dev-lang/perl:             5.38.2-r1::gentoo
dev-lang/python:           3.11.7::gentoo, 3.12.1::gentoo
dev-lang/rust-bin:         1.74.1::gentoo
dev-util/cmake:            3.27.9::gentoo
dev-util/meson:            1.3.0-r2::gentoo
sys-apps/baselayout:       2.14-r1::gentoo
sys-apps/sandbox:          2.37::gentoo
sys-apps/systemd:          254.7::gentoo
sys-devel/autoconf:        2.71-r6::gentoo
sys-devel/automake:        1.16.5-r1::gentoo
sys-devel/binutils:        2.41-r2::gentoo
sys-devel/binutils-config: 5.5::gentoo
sys-devel/gcc:             13.2.1_p20230826::gentoo
sys-devel/gcc-config:      2.11::gentoo
sys-devel/libtool:         2.4.7-r1::gentoo
sys-devel/llvm:            16.0.6::gentoo
sys-devel/make:            4.4.1-r1::gentoo
sys-kernel/linux-headers:  6.1::gentoo (virtual/os-headers)
sys-libs/glibc:            2.38-r9::gentoo
Repositories:

gentoo
    location: /var/db/repos/gentoo
    sync-type: rsync
    sync-uri: rsync://rsync.gentoo.org/gentoo-portage
    priority: -1000
    volatile: False
    sync-rsync-verify-jobs: 1
    sync-rsync-extra-opts: 
    sync-rsync-verify-max-age: 3
    sync-rsync-verify-metamanifest: yes

ACCEPT_KEYWORDS="amd64"
ACCEPT_LICENSE="@FREE"
CBUILD="x86_64-pc-linux-gnu"
CFLAGS="-O2 -pipe"
CHOST="x86_64-pc-linux-gnu"
CONFIG_PROTECT="/etc /usr/share/config /usr/share/gnupg/qualified.txt"
CONFIG_PROTECT_MASK="/etc/ca-certificates.conf /etc/dconf /etc/env.d /etc/fonts/fonts.conf /etc/gconf /etc/gentoo-release /etc/revdep-rebuild /etc/sandbox.d /etc/terminfo /etc/texmf/language.dat.d /etc/texmf/language.def.d /etc/texmf/updmap.d /etc/texmf/web2c"
CXXFLAGS="-O2 -pipe"
DISTDIR="/var/cache/distfiles"
EMERGE_DEFAULT_OPTS="--keep-going --complete-graph --usepkg=y"
ENV_UNSET="CARGO_HOME DBUS_SESSION_BUS_ADDRESS DISPLAY GDK_PIXBUF_MODULE_FILE GOBIN GOPATH PERL5LIB PERL5OPT PERLPREFIX PERL_CORE PERL_MB_OPT PERL_MM_OPT XAUTHORITY XDG_CACHE_HOME XDG_CONFIG_HOME XDG_DATA_HOME XDG_RUNTIME_DIR XDG_STATE_HOME"
FCFLAGS="-O2 -pipe"
FEATURES="assume-digests binpkg-docompress binpkg-dostrip binpkg-logs binpkg-multi-instance buildpkg buildpkg-live clean-logs config-protect-if-modified distlocks fixlafiles ipc-sandbox multilib-strict network-sandbox news parallel-fetch parallel-install pid-sandbox pkgdir-index-trusted preserve-libs protect-owned qa-unresolved-soname-deps sandbox sfperms split-elog split-log strict unknown-features-warn unmerge-logs unmerge-orphans userfetch userpriv usersandbox usersync xattr"
FFLAGS="-O2 -pipe"
GENTOO_MIRRORS="https://mirrors.gethosted.online/gentoo/ https://www.mirrorservice.org/sites/distfiles.gentoo.org/ https://mirror.bytemark.co.uk/gentoo/ https://mirrors.soeasyto.com/distfiles.gentoo.org/"
LANG="C.UTF8"
LDFLAGS="-Wl,-O1 -Wl,--as-needed"
LEX="flex"
MAKEOPTS="-j4 -l4"
PKGDIR="/var/cache/binpkgs"
PORTAGE_COMPRESS="xz"
PORTAGE_CONFIGROOT="/"
PORTAGE_RSYNC_OPTS="--recursive --links --safe-links --perms --times --omit-dir-times --compress --force --whole-file --delete --stats --human-readable --timeout=180 --exclude=/distfiles --exclude=/local --exclude=/packages --exclude=/.git"
PORTAGE_TMPDIR="/var/tmp"
SHELL="/bin/bash"
USE="acl amd64 bzip2 cli crypt dri fortran gdbm iconv ipv6 libtirpc multilib ncurses nls openmp pam pcre readline seccomp split-usr ssl systemd test-rust udev unicode xattr zlib" ABI_X86="64" ADA_TARGET="gnat_2021" APACHE2_MODULES="authn_core authz_core socache_shmcb unixd actions alias auth_basic authn_anon authn_dbm authn_file authz_dbm authz_groupfile authz_host authz_owner authz_user autoindex cache cgi cgid dav dav_fs dav_lock deflate dir env expires ext_filter file_cache filter headers include info log_config logio mime mime_magic negotiation rewrite setenvif speling status unique_id userdir usertrack vhost_alias" CALLIGRA_FEATURES="karbon sheets words" COLLECTD_PLUGINS="df interface irq load memory rrdtool swap syslog" CPU_FLAGS_X86="mmx mmxext sse sse2" ELIBC="glibc" GPSD_PROTOCOLS="ashtech aivdm earthmate evermore fv18 garmin garmintxt gpsclock greis isync itrax mtk3301 ntrip navcom oceanserver oncore rtcm104v2 rtcm104v3 sirf skytraq superstar2 tsip tripmate tnt ublox" INPUT_DEVICES="libinput" KERNEL="linux" LCD_DEVICES="bayrad cfontz glk hd44780 lb216 lcdm001 mtxorb text" LUA_SINGLE_TARGET="lua5-1" LUA_TARGETS="lua5-1" OFFICE_IMPLEMENTATION="libreoffice" PHP_TARGETS="php8-1" POSTGRES_TARGETS="postgres15" PYTHON_SINGLE_TARGET="python3_11" PYTHON_TARGETS="python3_11" RUBY_TARGETS="ruby31" VIDEO_CARDS="amdgpu fbdev intel nouveau radeon radeonsi vesa dummy" XTABLES_ADDONS="quota2 psd pknock lscan length2 ipv4options ipp2p iface geoip fuzzy condition tarpit sysrq proto logmark ipmark dhcpmac delude chaos account"
Unset:  ADDR2LINE, AR, ARFLAGS, AS, ASFLAGS, CC, CCLD, CONFIG_SHELL, CPP, CPPFLAGS, CTARGET, CXX, CXXFILT, ELFEDIT, EXTRA_ECONF, F77FLAGS, FC, GCOV, GPROF, INSTALL_MASK, LC_ALL, LD, LFLAGS, LIBTOOL, LINGUAS, MAKE, MAKEFLAGS, NM, OBJCOPY, OBJDUMP, PORTAGE_BINHOST, PORTAGE_BUNZIP2_COMMAND, PORTAGE_COMPRESS_FLAGS, PORTAGE_RSYNC_EXTRA_OPTS, PYTHONPATH, RANLIB, READELF, RUSTFLAGS, SIZE, STRINGS, STRIP, YACC, YFLAGS
Comment 1 Sam James archtester Gentoo Infrastructure gentoo-dev Security 2024-01-12 17:55:18 UTC 
I've not looked at what the test does but if it's a timeout or something as the name implies, maybe just skip it, as I thinnk the box was loaded.
Comment 2 Maciej Barć gentoo-dev 2024-01-12 18:05:55 UTC 
A lot of Z3 tests in Dafny and Boogie could be outdated, so yes, this is safe to skip probably, there is definitely a fair amount of tests using z3 already.
Comment 3 Larry the Git Cow gentoo-dev 2024-01-12 23:22:06 UTC 
The bug has been closed via the following commit(s):

https://gitweb.gentoo.org/repo/gentoo.git/commit/?id=c4294764f72a31de0fd5a013151a2fd8807ad0af

commit c4294764f72a31de0fd5a013151a2fd8807ad0af
Author:     Maciej Barć <xgqt@gentoo.org>
AuthorDate: 2024-01-12 19:54:41 +0000
Commit:     Maciej Barć <xgqt@gentoo.org>
CommitDate: 2024-01-12 23:21:58 +0000

    dev-lang/boogie: disable the z3-hard-timeout test
    
    Closes: https://bugs.gentoo.org/921948
    Signed-off-by: Maciej Barć <xgqt@gentoo.org>

 dev-lang/boogie/boogie-3.0.6.ebuild | 3 ++-
 dev-lang/boogie/boogie-3.0.8.ebuild | 3 ++-
 dev-lang/boogie/boogie-3.0.9.ebuild | 3 ++-
 3 files changed, 6 insertions(+), 3 deletions(-)