Potential bug with race condition

Hi, this might be a user error, but I got the examples working and got correct bug reports.

But the following code:

[Fact]
public async Task Test()
{
    long counter = 17;

    var task1 = Task.Run(() =>
    {
        var val = counter;
        counter -= val;
    });
    var task2 = Task.Run(() =>
    {
        var val = counter;
        counter -= val;
    });

    await Task.WhenAll(task1, task2);

    Assert.Equal(0, counter);
}

[Fact]
[Microsoft.Coyote.SystematicTesting.Test]
public void CoyoteTest()
{
    var configuration = Configuration.Create().WithTestingIterations(10);
    var engine = TestingEngine.Create(configuration, Test);
    engine.Run();
}

Does not produce any bugs. in some cases this can return -17 instead of 0, but I cant get coyote to produce that result.

Changing to this:

[Fact]
public async Task Test()
{
    long counter = 17;

    var task1 = Task.Run(async () =>
    {
        var val = counter;
        await Task.Delay(1);
        counter -= val;
    });
    var task2 = Task.Run(async () =>
    {
        var val = counter;
        await Task.Delay(1);
        counter -= val;
    });

    await Task.WhenAll(task1, task2);

    Assert.Equal(0, counter);
}

produces the bug report correctly, is this expected behaviour or should the first example also produce a bug?

Start with the two C# examples in the issue and run the CoyoteTest method using Configuration.Create().WithTestingIterations(10). Compare the behavior of the immediate counter updates with the version containing Task.Delay(1). Done should establish whether the difference is expected and identify the relevant Coyote behavior or missing coverage.