Error runnning stainless.

[NicolasRouquette]

See: https://github.com/NicolasRouquette/stainless-bundle-closure/tree/4d184817484de4e6e465b5edd56cfaef1a66b4d3

When building, I get this:

[info] welcome to sbt 1.3.13 (AdoptOpenJDK Java 11.0.7)
[info] loading settings for project global-plugins from dependency-graph.sbt,sbt-updates.sbt ...
[info] loading global plugins from /home/rouquette/.sbt/1.0/plugins
[info] loading settings for project bundle-closure-build from plugins.sbt,idea7.sbt ...
[info] loading project definition from /home/rouquette/Desktop/stainless/bundle-closure/project
[info] loading settings for project bundle-closure from build.sbt ...
[info] set current project to bundle-closure (in build file:/home/rouquette/Desktop/stainless/bundle-closure/)
[info] Defining Global / ideaPort
[info] The new value will be used by Compile / compile, Test / compile and 3 others.
[info]  Run `last` for details.
[info] Reapplying settings...
[info] set current project to bundle-closure (in build file:/home/rouquette/Desktop/stainless/bundle-closure/)
[IJ]sbt:bundle-closure> all {file:/home/rouquette/Desktop/stainless/bundle-closure/}bundle-closure/products {file:/home/rouquette/Desktop/stainless/bundle-closure/}bundle-closure/test:products {file:/home/rouquette/Desktop/stainless/bundle-closure/}core/products {file:/home/rouquette/Desktop/stainless/bundle-closure/}core/test:products {file:/home/rouquette/Desktop/stainless/bundle-closure/}verified/products {file:/home/rouquette/Desktop/stainless/bundle-closure/}verified/test:products
[info] Compiling 33 Scala sources to /home/rouquette/Desktop/stainless/bundle-closure/verified/target/scala-2.12/classes ...
[warn] The Z3 native interface is not available. Falling back onto princess.
[info] Generating VCs for those functions: complement$0, complement$1, complement$2, complement$3
[info] Checking Verification Conditions...
[info]  - Checking cache: 'precond. (call complement(@unchecked {   assert(this...)' VC for complement @5:7...
[info] Cache hit: 'precond. (call complement(@unchecked {   assert(this...)' VC for complement @5:7...
[info]  - Checking cache: 'precond. (call complement(@unchecked {   assert(this...)' VC for complement @5:7...
[info] Cache hit: 'precond. (call complement(@unchecked {   assert(this...)' VC for complement @5:7...
[info]  - Checking cache: 'precond. (call complement(@unchecked {   assert(this...)' VC for complement @5:7...
[info] Cache hit: 'precond. (call complement(@unchecked {   assert(this...)' VC for complement @5:7...
[info]   - Inferring measure for unique...
[info]  => Found measure for unique.
[info]   - Inferring measure for ++...
[info]  => Found measure for ++.
[info]   - Inferring measure for union...
[error] Stainless terminated with an error.
[error] Debug output is available in the file `stainless-stack-trace.txt`, you may report your issue on https://github.com/epfl-lara/stainless/issues
[error] You may use --debug=frontend to have the stack trace displayed in the output.
2020-11-08 21:58:15,451 shutdown-hooks-run-all ERROR No Log4j 2 configuration file found. Using default configuration (logging only errors to the console), or user programmatically provided configurations. Set system property 'log4j2.debug' to show Log4j 2 internal initialization logging. See https://logging.apache.org/log4j/2.x/manual/configuration.html for instructions on how to configure Log4j 2

And the attached stack trace. stainless-stack-trace.txt

[jad-hamza]

The princess solver is not very well supported by Stainless. Can you try downloading z3 4.8.6 (we have some known issues with later versions) and adding it to your path?

https://github.com/Z3Prover/z3/releases/tag/z3-4.8.6

Then your warning might become, and hopefully the errors go away.

[warn] The Z3 native interface is not available. Falling back onto smt-z3.

[NicolasRouquette]

Thanks! On my linux system, I just did sudo apt-get install z3 which gave me version z3/focal 4.8.7-4build1 amd64 Now, stainless is behaving as advertised.

However, I'm a bit perplexed here; the installation instructions say that stainless bundles z3: https://epfl-lara.github.io/stainless/installation.html

How is it then that I had to install z3 separately? I don't mind doing this, I'm just a bit confused.

[jad-hamza]

You're welcome, z3 4.8.7 should work mostly fine but it's possible that our test suite fails in one or two examples.

However, I'm a bit perplexed here; the installation instructions say that stainless bundles z3:

I think this refers to the binary release available here: https://github.com/epfl-lara/stainless/releases