Test generation incomplete for switch statement

Hi,

The test code generated does not exercise the path with the "true" return statement - "case 256: return true;"

Here is the generated code:

using NUnit.Framework;
using VSharp.TestExtensions;

namespace BranchesAndLoops.Tests;

[TestFixture]
class SwitchStatementTests
{
    [Test, Category("Generated")]
    public void SimpleSwitchWithAdditionAndMultiplicationTest()
    {
        // arrange
        SwitchStatement thisArg = new Allocator<SwitchStatement>{
            ["X"] = 8,
            ["Y"] = 0
        }.Object;

        // act
        var result = thisArg.SimpleSwitchWithAdditionAndMultiplication();

        // assert
        Assert.AreEqual(false, result);
    }
}

This is the input:

namespace BranchesAndLoops
{
    public class SwitchStatement
    {
        public SwitchStatement(int x, int y)
        {
            this.X = x;
            this.Y = y;
        }

        int X { get; }
        int Y { get;  }

        public bool SimpleSwitchWithAdditionAndMultiplication()
        {
            if (X <= 0 || Y <= 0)
            {
                return false;
            }

            switch (checked(X + Y + X*Y + 1))
            {
                case 256: return true;

                case 512: return false;

                case 1024: return false;
            }

            return false;

        }

    }
}

Script to execute:

dotnet ..\..\..\Cymbal-TestGen\upstream\VSharp\VSharp.Runner\bin\Release\net7.0\VSharp.Runner.dll --all-public-methods  bin\Debug\net6.0\BranchesAndLoops.dll -t 30 -o ..\out --render-tests --run-tests

VSharp-team / VSharp

Test generation incomplete for switch statement #318