search

Boolector / boolector

A Satisfiability Modulo Theories (SMT) solver for the theories of fixed-size bit-vectors, arrays and uninterpreted functions.
http://boolector.github.io
Other
335 stars 62 forks source link

Test failures on aarch64 linux #178

Closed risicle closed 2 years ago

risicle commented 2 years ago

Hi, this is half issue-report and half question.

Over at https://github.com/nixos/nixpkgs we're getting many test failures when building our boolector package for aarch64. Full log: https://hydra.nixos.org/log/hcc77cybwgnpypyhk8aq0xxvcimny65b-boolector-3.2.2.drv

This is using the same procedure as the x86_64 package which passes its tests flawlessly: https://hydra.nixos.org/log/hz01xqlc0gs1lvrggg9j3id38c3jaxs4-boolector-3.2.2.drv

The question - to what extent is boolector known to work on other architectures? Though there's no mention of ARM64/aarch64 in this repo, there's evidence of other projects building it under aarch64 (https://github.com/esbmc/esbmc/blob/0749b2e72197e62323387f423ceb1ad339c9ae94/.github/workflows/build.yml#L59), but nothing about them running the tests.

mpreiner commented 2 years ago

Most of the tests fail because of Lingeling, but I can't reproduce it on an arm64 Ubuntu docker image. It seems that the Lingeling version that is used is pretty outdated (from 2018). Boolector currently uses arminbiere/lingeling@7d5db72420b95ab356c98ca7f7a4681ed2c59c70. There are two other errors related to parsing that we'll investigate.

Thanks for the heads-up!

mpreiner commented 2 years ago

Parser issues are fixed with cc3a709. The Lingeling errors should be gone when using a newer version.

risicle commented 2 years ago

Amazing! Bumping lingeling and applying the patch indeed solves it all. Aarch64 users will have a boolector this nixos release (and the 10 packages that depend on it). Many thanks.