search

epfl-lara / stainless

Verification framework and tool for higher-order Scala programs
https://epfl-lara.github.io/stainless/
Apache License 2.0
349 stars 50 forks source link

CVC4 built from source with the attached modification (to build on arm64) makes Stainless freeze #1419

Open samuelchassot opened 1 year ago

samuelchassot commented 1 year ago

CVC4 is not available on arm64 architecture so I built it from source. For the build process to go through, I had to make some modifications to a file of the project (see .patch attached). The compilation produces an executable that is in my PATH and that I can invoke from my terminal. However, when I try to use smt-cvc4 option with Stainless, it freezes at the 1st VC. For the same project without smt-cvc4 everything works well.

to_build_arm.patch

samuelchassot commented 1 year ago

This can be reproduced with https://github.com/epfl-lara/bolts/tree/master/WIP/SLOW/longmap for example, with or without smt-cvc4 in the config: stainless-dotty --config-file=stainless.conf StrictlyOrderedLongListMap.scala