Trying to use generate-tests

[seebees]

Dafny version

4.9.0

Code to produce this issue

No response

Command to run and resulting output

No response

What happened?

I am running

dafny generate-tests \
Block \
AwsCryptographyPrimitives/src/KDF/KdfCtr.dfy \
--cores 4 \
--coverage-report dafny-cov.html \
--print-bpl asdf.bpl \
--function-syntax 3 

For this code: https://github.com/aws/aws-cryptographic-material-providers-library/blob/main/AwsCryptographyPrimitives/src/KDF/KdfCtr.dfy.

I added
method {:testEntry} KdfCounterMode(input: Types.KdfCtrInput)
method {:testInline} RawDerive(
function method {:testInline} Increment(

and to Wrappers.dfy
function {:testInline} Need

I get

(77418,174): Error: arithmetic comparisons are not allowed in triggers
(77418,185): Error: arithmetic comparisons are not allowed in triggers
(77418,215): Error: arithmetic comparisons are not allowed in triggers
(77418,230): Error: arithmetic comparisons are not allowed in triggers
(77418,265): Error: arithmetic comparisons are not allowed in triggers
(77418,280): Error: arithmetic comparisons are not allowed in triggers
(77418,303): Error: arithmetic comparisons are not allowed in triggers
(77418,323): Error: arithmetic comparisons are not allowed in triggers
(66521,174): Error: arithmetic comparisons are not allowed in triggers
(66521,185): Error: arithmetic comparisons are not allowed in triggers
(66521,215): Error: arithmetic comparisons are not allowed in triggers
(66521,230): Error: arithmetic comparisons are not allowed in triggers
(66521,265): Error: arithmetic comparisons are not allowed in triggers
(66521,280): Error: arithmetic comparisons are not allowed in triggers
(66521,303): Error: arithmetic comparisons are not allowed in triggers
(66521,323): Error: arithmetic comparisons are not allowed in triggers
(66521,174): Error: arithmetic comparisons are not allowed in triggers
(66521,185): Error: arithmetic comparisons are not allowed in triggers
(66521,215): Error: arithmetic comparisons are not allowed in triggers
(66521,230): Error: arithmetic comparisons are not allowed in triggers
(66521,265): Error: arithmetic comparisons are not allowed in triggers
(66521,280): Error: arithmetic comparisons are not allowed in triggers
(66521,303): Error: arithmetic comparisons are not allowed in triggers
(66521,323): Error: arithmetic comparisons are not allowed in triggers

Pulling out the boogie, I find 66521 for you

implementation {:smt_option "smt.arith.solver", "2"}
{:verboseName "Mul.LemmaMulStrictUpperBoundAuto (correctness)"}
Impl$$Mul.__default.LemmaMulStrictUpperBoundAuto() returns ($_reverifyPost: bool)
{

...

  anon12_Else:
    assume (forall x#0_1: int, XBound#0_1: int, y#0_1: int, YBound#0_1: int :: 
    { Mul(XBound#0_1 - 1, YBound#0_1 - 1), Mul(x#0_1, y#0_1) } 
    { YBound#0_1 - 1, XBound#0_1 - 1, 0 < y#0_1, 0 < x#0_1 }
    { YBound#0_1 - 1, 0 < y#0_1, x#0_1 < XBound#0_1 }
    { XBound#0_1 - 1, 0 < x#0_1, y#0_1 < YBound#0_1 }
    { y#0_1 < YBound#0_1, x#0_1 < XBound#0_1 }
    x#0_1 < XBound#0_1 && y#0_1 < YBound#0_1 && 0 < x#0_1 && 0 < y#0_1 ==> Mul(x#0_1, y#0_1) <= Mul(XBound#0_1 - 1, YBound#0_1 - 1));
    goto anon11;

Here is the Dafny:

  lemma LemmaMulStrictUpperBoundAuto()
    ensures forall x: int, XBound: int, y: int, YBound: int {:trigger x * y, (XBound - 1) * (YBound - 1)}
              :: x < XBound && y < YBound && 0 < x && 0 < y ==> x * y <= (XBound - 1) * (YBound - 1)
  {
    forall (x: int, XBound: int, y: int, YBound: int | x < XBound && y < YBound && 0 < x && 0 < y)
      ensures x * y <= (XBound - 1) * (YBound - 1)
    {
      LemmaMulStrictUpperBound(x, XBound, y, YBound);
    }
  }

Additionally, I only get a single test. Not many tests as I would expect.

asdf.bpl.zip

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

Mac