Using `--standard-libraries` causes verification timeouts

[alexporter8013]

Dafny version

4.4.0+707b18acee078b3aa4d84c0590a980966bf22428

Code to produce this issue

method GoodDouble(x: int) returns (r: int)
{
    r := x + x;
    assert r == 2 * x;
}

method BadDouble(x: int) returns (r: int)
{
    r := x + x;
    assert r == 2 * x + 1;
}

Command to run and resulting output

> dafny verify .\bad_standard_lib.dfy --standard-libraries --verification-time-limit=30 --log-format text
bad_standard_lib.dfy(8,0): Verification of 'BadDouble (correctness)' timed out after 30 seconds
  |
8 | method BadDouble(x: int) returns (r: int)
  |        ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^

Dafny program verifier finished with 1 verified, 0 errors, 1 time out

Results for GoodDouble (correctness)
  Overall outcome: Correct
  Overall time: 00:00:00.2391828
  Overall resource count: 6558
  Maximum assertion batch time: 00:00:00.0874553
  Maximum assertion batch resource count: 6558

  Assertion batch 0:
    Outcome: Valid
    Duration: 00:00:00.0874553
    Resource count: 6558

    Assertions:
      bad_standard_lib.dfy(4,12): variable 'r', which is subject to definite-assignment rules, is always initialized here
      bad_standard_lib.dfy(4,14): assertion always holds
      bad_standard_lib.dfy(5,1): out-parameter 'r', which is subject to definite-assignment rules, is always initialized at this return point

Results for BadDouble (correctness)
  Overall outcome: TimedOut
  Overall time: 00:00:30.3462355
  Overall resource count: 6821342
  Maximum assertion batch time: 00:00:30.0877105
  Maximum assertion batch resource count: 6821342

  Assertion batch 0:
    Outcome: TimeOut
    Duration: 00:00:30.0877105
    Resource count: 6821342

    Assertions:
      bad_standard_lib.dfy(11,12): variable 'r', which is subject to definite-assignment rules, is always initialized here
      bad_standard_lib.dfy(11,14): assertion always holds
      bad_standard_lib.dfy(12,1): out-parameter 'r', which is subject to definite-assignment rules, is always initialized at this return point

What happened?

When running the above command, I would expect something closer to the output of not including --standard-libraries, given below:

> dafny verify .\bad_standard_lib.dfy --verification-time-limit=30 --log-format text
bad_standard_lib.dfy(11,11): Error: assertion might not hold
   |
11 |     assert r == 2 * x + 1;
   |              ^^^^^^^^^^^^

Dafny program verifier finished with 1 verified, 1 error

Results for GoodDouble (correctness)
  Overall outcome: Correct
  Overall time: 00:00:00.2280506
  Overall resource count: 3451
  Maximum assertion batch time: 00:00:00.0894618
  Maximum assertion batch resource count: 3451

  Assertion batch 0:
    Outcome: Valid
    Duration: 00:00:00.0894618
    Resource count: 3451

    Assertions:
      bad_standard_lib.dfy(4,12): variable 'r', which is subject to definite-assignment rules, is always initialized here
      bad_standard_lib.dfy(4,14): assertion always holds
      bad_standard_lib.dfy(5,1): out-parameter 'r', which is subject to definite-assignment rules, is always initialized at this return point

Results for BadDouble (correctness)
  Overall outcome: Errors
  Overall time: 00:00:00.2182016
  Overall resource count: 3636
  Maximum assertion batch time: 00:00:00.0967902
  Maximum assertion batch resource count: 3636

  Assertion batch 0:
    Outcome: Invalid
    Duration: 00:00:00.0967902
    Resource count: 3636

    Assertions:
      bad_standard_lib.dfy(11,12): variable 'r', which is subject to definite-assignment rules, is always initialized here
      bad_standard_lib.dfy(11,14): assertion always holds
      bad_standard_lib.dfy(12,1): out-parameter 'r', which is subject to definite-assignment rules, is always initialized at this return point

What type of operating system are you experiencing the problem on?

Windows

[keyboardDrummer]

The usage of --standard-libraries should have absolutely no effect since you are not even importing any of the modules from that library, so the generated SMT should be exactly the same.

[franck44]

I also experience the same issue (all the proofs in the file that includes Std.Arithmetic time out). Running 4.4.0.0, VsCode, MacOS.