SMTChecker test failure: "SMTChecker/division": Multiple errors found

[livnev]

Description

When I build 0.5.11 from https://github.com/ethereum/solidity/releases/download/v0.5.11/solidity_0.5.11.tar.gz, upon running the tests I get:

--- SKIPPING ALL SEMANTICS TESTS ---

Running 2879 test cases...

0%   10   20   30   40   50   60   70   80   90   100%
|----|----|----|----|----|----|----|----|----|----|
*******/build/source/test/libsolidity/AnalysisFramework.cpp(65): fatal error: in "SMTChecker/division": Multiple errors found: :9:17: Warning: Overflow (resulting value larger than 2**256 - 1) might happen here.
                                uint256 c = a * b;
                                            ^---^

:10:13: Warning: Division by zero happens here
                                require(c / a == b);
                                        ^---^
  for:
   = 0
  <result> = 0
  a = 0
  b = 0
  c = 0

Callstack:


********************************************

*** 1 failure is detected in the test module "SolidityTests"

Environment

• Compiler version: the 0.5.11 release
• Target EVM version (as per compiler settings): -
• Framework/IDE (e.g. Truffle or Remix): -
• EVM execution environment / backend / blockchain client: -
• Operating system: linux

$ z3 --version
Z3 version 4.8.4 - 64 bit

Steps to Reproduce

I am building solc with nix from this version of nixpkgs. 0.5.10 builds and tests without problems. Could my z3 version be responsible?

cc @leonardoalt

[leonardoalt]

Yeah we've seen queries that Z3 4.8.5 can solve whereas 4.8.4 can't, this could be one of those. It's hard to set test expectations for hard queries (nonlinear arithmetics in this case), also because using CVC4 instead of Z3 might be more/less powerful depending on the theory. That's why we decided to set the test expectations according to the solvers latest releases.

[livnev]

Yeah we've seen queries that Z3 4.8.5 can solve whereas 4.8.4 can't, this could be one of those. It's hard to set test expectations for hard queries (nonlinear arithmetics in this case), also because using CVC4 instead of Z3 might be more/less powerful depending on the theory. That's why we decided to set the test expectations according to the solvers latest releases.

I see, though I think it didn't work for me with 4.8.5 either, but I can check again.

[livnev]

Can confirm that I am getting the same failure with:

$ z3 --version
Z3 version 4.8.5 - 64 bit

[leonardoalt]

Let me run that locally with Z3 only, maybe CVC4 is the responsible for solving it in the tests.

[leonardoalt]

I can reproduce it with Z3 4.8.5 and no CVC4. This means we also need to adjust this test such that it can succeed or return unknown.

[livnev]

I can confirm that:

(a) building with CVC4 resolves the issue
(b) your patch in #7298 resolves the issue

I decided to add CVC4 support to the nix derivation.

[leonardoalt]

Thanks @livnev !