search

VSharp-team / VSharp

Symbolic execution engine for .NET Core
Apache License 2.0
50 stars 32 forks source link

[followup] Test generation incomplete for switch statement #320

Closed smhmhmd closed 5 months ago

smhmhmd commented 6 months ago

This is a followup of https://github.com/VSharp-team/VSharp/issues/318. The following uses the latest VSharp after 'git pull'. Do you see the same issue ? Am I running this right ?

Here is input

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

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

        public bool SimpleSwitchWithAdditionAndMultiplication()
        {

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

                case 512: return false;

                case 1024: return false;
            }

            return false;

        }

    }
}

Only one test-case was generated, it does not include the "true" branch in the code i.e "case 256: return true":

  [Test, Category("Generated")]^M
    public void SimpleSwitchWithAdditionAndMultiplicationTest()^M
    {^M
        // arrange
        SwitchStatement thisArg = new Allocator<SwitchStatement>{
            ["X"] = 4096,
            ["Y"] = 4096,
            ["Z"] = 0
        }.Object;^M

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

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

The value should be [z = -7, x = -20, y = 2]:

$ cat test.py
from z3 import *

x = Int('x')
y = Int('y')
z = Int('z')
s = Solver()
s.add(x + y + z + x*y*z + 1 == 256)
print(s.check())
print(s.model())

$ python3 test.py
sat
[z = -7, x = -20, y = 2]
MchKosticyn commented 6 months ago

Checked on #317, it works and finds path with "return true". Try it on current 'master'.

smhmhmd commented 6 months ago

Hi @MchKosticyn

Test-case for 'return true' is not created. I am using current master branch at this git hash

commit 7a70925b1898bd7ce303cdfd0053333b6883c7b9 (HEAD -> master, origin/master, origin/HEAD)
Merge: f2f93b50 f33d60e9
Author: Mikhail Kosticyn <mishakosticyn@yandex.ru>
Date:   Tue Mar 26 13:51:42 2024 +0300

    Merge pull request #317 from MchKosticyn/master

    Fixes and ASP.NET exploration

Here is the dll I built today. I did a 'git pull' , 'git clean -fdx' and built the release dll using Visual Studio 2022:

D:\Users\samiull\Documents\2023\cymbal-testgen\Cymbal-TestGen\csharp\branches-quickstart>dir ..\..\..\Cymbal-TestGen\upstream\VSharp\VSharp.Runner\bin\Release\net7.0\VSharp.Runner.dll
 Volume in drive D is UserProfile
 Volume Serial Number is 3E5C-67FD

 Directory of D:\Users\samiull\Documents\2023\cymbal-testgen\Cymbal-TestGen\upstream\VSharp\VSharp.Runner\bin\Release\net7.0

04/10/2024  01:49 PM            17,920 VSharp.Runner.dll
               1 File(s)         17,920 bytes
               0 Dir(s)  117,816,336,384 bytes free

Testgen bat script in Windows 10

>type testgen.bat
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

Tests are created in the out directory (I will file issues for the other failing tests after this one is resolved)

D:\Users\samiull\Documents\2023\cymbal-testgen\Cymbal-TestGen\csharp\out>dir BranchesAndLoops.tests\
dir BranchesAndLoops.tests\
 Volume in drive D is UserProfile
 Volume Serial Number is 3E5C-67FD

 Directory of D:\Users\samiull\Documents\2023\cymbal-testgen\Cymbal-TestGen\csharp\out\BranchesAndLoops.tests

04/10/2024  02:05 PM    <DIR>          .
04/10/2024  02:05 PM    <DIR>          ..
04/10/2024  01:57 PM             1,912 BranchesAndLoops.Tests.csproj
04/10/2024  01:57 PM             1,707 ChallengeAnswerTests.cs
04/10/2024  01:57 PM             4,024 EightQueensTests.cs
04/10/2024  01:57 PM             8,404 ExploreIfTests.cs
04/10/2024  01:57 PM             4,462 ExploreLoopsTests.cs
04/10/2024  01:57 PM    <DIR>          Extensions
04/10/2024  01:57 PM             3,584 LinearEquationsTests.cs
04/10/2024  01:57 PM    <DIR>          obj
04/10/2024  01:57 PM                99 SudokuTests.cs
04/10/2024  01:57 PM               577 SwitchStatementTests.cs
               8 File(s)         24,769 bytes
               4 Dir(s)  117,815,783,424 bytes free

Here is the resulting SwitchStatementTests.cs that was created:

using NUnit.Framework;^M
using VSharp.TestExtensions;^M
^M
namespace BranchesAndLoops.Tests;

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

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

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

If there are any debug logs you would like to see, please let me know what I need to turn on in the VSharp source code.

MchKosticyn commented 6 months ago

Hi, @smhmhmd. Tested on Windows 10, 'return true' is covered. Can you please add '-v Trace' option to V# starting cmd command and post the result?

smhmhmd commented 6 months ago

Hi @MchKosticyn

Here is the log with '-v Trace'

dotnet ..\..\..\Test\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 -v Trace

log.txt

MchKosticyn commented 6 months ago

Hi, @smhmhmd. Your coverage zone (methods, which SE is trying to cover with tests) is 'all public methods'. Maybe SE engine has not enough time to cover all methods' branches. Try to use '--method SimpleSwitchWithAdditionAndMultiplication' option instead. This will lead to only this method exploration.

smhmhmd commented 5 months ago

Hi @MchKosticyn

Still not seeing the branch. As suggested, I removed '--all-public-methods' and added '--method SimpleSwitchWithAdditionAndMultiplication'

Looking at the log, there is an overflow exception: log.txt

[Info] [4/23/2024 11:11:14 AM] System.OverflowException! Stack trace: System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)^M [Info] [4/23/2024 11:11:14 AM] Invoking method System.Void VSharp.CSharpUtils.Exceptions.CreateOverflowException()^M [Trace] [4/23/2024 11:11:14 AM] Exception thrown (HeapRef 2 to System.OverflowException), StackTrace: [method = System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this) offset = 37]^M

MchKosticyn commented 5 months ago

Hi, @smhmhmd

"Overflow exception" message in the log means, that V# found branch with overflow exception.

Reason why branch 'return true' is uncovered is 'UNKNOWN' result from SMT solver.

But in my logs I have different SMT requests. This may happen due to randomness inside Searcher (it's system, which determines, what branch to explore). Let's use BFS searcher for determinism. Could you add '--strat BFS' option to use it and post the log again?

smhmhmd commented 5 months ago

Thanks @MchKosticyn , '--strat BFS' worked. Could you explain how the constraints were computed, thanks again.

log.txt

   [Test, Category("Generated")]^M
    public void SimpleSwitchWithAdditionAndMultiplicationTest3()^M
    {^M
        // arrange
        SwitchStatement thisArg = new Allocator<SwitchStatement>{
            ["X"] = 4,
            ["Y"] = 50,
            ["Z"] = 1
        }.Object;^M

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

        // assert
        Assert.AreEqual(true, result);^M
    }^M
MchKosticyn commented 5 months ago

Hi, @smhmhmd It seems you posted an old log, because it has no '--strat' option in starting command. Could you post new log, please? Also, it's kind of strange, that '--strat BFS' option helped, because searcher doesn't change SE process very much. Could you also use '--strat DFS' option and post second log?

Speaking about constraints, it's computed during symbolic execution: at very beginning initial symbolic state is created, it contains the initial symbolic memory and the initial path conditions. The initial symbolic memory contains symbolic function arguments -- symbols (for example, int x = 'X'). In your example symbolic memory will contain object of class 'SwitchStatement', it means, that each field of that class is symbolic. Initial path constraints are 'true'. After initial state is created, symbolic interpreter executes instruction by instruction, arguments and result of instruction may be symbolic expressions. For example, if instruction is 'x + y' and 'x' variable equals 'X' symbol, 'y' equals 'Y' symbol, than result of expression will be 'X + Y'. When 'if (c) then t else e' statement is executed, symbolic machine uses SMT solver to check if 'c' is satisfiable (it means, that there are any concrete arguments substitution for symbols, which will eval formula 'c' to 'true'). If 'c' is satisfiable, interpreter goes to 'then' branch. After 'c' condition checked, it checks '!c' condition: if it's satisfiable, then interpreter creates another symbolic state, which goes to 'else' branch. As result SMT solver may return: (1) 'SAT' (formula is satisfiable) and model (model is variables substitution), (2) 'UNSAT' (formula is unsatisfiable), (3) 'UNKNOWN' -- in general SMT solver problem is unsolvable, but on practice it rarely happens. When all program branches are executed, symbolic machine will contain 'N' symbolic states. Each state can be transformed to unit test. Arguments for test obtained via model from SMT solver. Function result is computed via evaluation of symbolic result expression with substituted symbolic variables from model. For example, if function result is 'X + Y X Z - 1' and SMT model declares 'X' = 1, 'Y' = 2, 'Z' = 3, then result is 1 + 2 1 3 - 1 = 6.

I omitted a lot of details, you can read about them in the article https://arxiv.org/pdf/1610.00502.

smhmhmd commented 5 months ago

Hi @MchKosticyn

Here is the log with the "--strat BFS" option.

samiull@DESKTOP-OS5I16B MINGW64 /d/Users/samiull/Documents/2023/testgen/testgen/csharp/branches-quickstart (mainline)
$ ./testgen.bat | tee log.txt

D:\Users\samiull\Documents\2023\testgen\testgen\csharp\branches-quickstart>dotnet ..\..\..\testGen\upstream\VSharp\VSharp.Runner\bin\Release\net7.0\VSharp.Runner.dll  --method SimpleSwitchWithAdditionAndMultiplication bin\Debug\net6.0\BranchesAndLoops.dll --strat BFS -t 90 -o ..\out --render-tests --run-tests -v Trace 
[Info] [4/28/2024 8:28:31 PM] Starting to explore method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
[Trace] [4/28/2024 8:28:31 PM] Add CFG for System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this).
[Trace] [4/28/2024 8:28:31 PM] Add CFG for System.Int32 BranchesAndLoops.SwitchStatement.get_X(this).
[Info] [4/28/2024 8:28:31 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_X(this)
[Info] [4/28/2024 8:28:31 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_X(this)
[Trace] [4/28/2024 8:28:31 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:28:31 PM] !(null == this) & this.<X>k__BackingField > 0
[Trace] [4/28/2024 8:28:31 PM] SATISFIABLE
[Trace] [4/28/2024 8:28:31 PM] Add CFG for System.Int32 BranchesAndLoops.SwitchStatement.get_Y(this).
[Info] [4/28/2024 8:28:31 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_Y(this)
[Info] [4/28/2024 8:28:31 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_Y(this)
[Trace] [4/28/2024 8:28:31 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:28:31 PM] !(null == this) & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0
[Trace] [4/28/2024 8:28:31 PM] SATISFIABLE
[Trace] [4/28/2024 8:28:31 PM] Add CFG for System.Int32 BranchesAndLoops.SwitchStatement.get_Z(this).
[Info] [4/28/2024 8:28:31 PM] Result of method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this) is False
[Info] [4/28/2024 8:28:31 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_Z(this)
[Info] [4/28/2024 8:28:31 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_Z(this)
[Info] [4/28/2024 8:28:31 PM] Result of method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this) is False
[Trace] [4/28/2024 8:28:32 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:28:32 PM] !(null == this) & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:28:32 PM] SATISFIABLE
[Info] [4/28/2024 8:28:32 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_X(this)
[Info] [4/28/2024 8:28:32 PM] Result of method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this) is False
[Info] [4/28/2024 8:28:32 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_X(this)
[Info] [4/28/2024 8:28:32 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_Y(this)
[Info] [4/28/2024 8:28:32 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_Y(this)
[Trace] [4/28/2024 8:28:32 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:28:32 PM] !(null == this) & !(this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField) & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:28:32 PM] SATISFIABLE
[Info] [4/28/2024 8:28:32 PM] System.OverflowException!
Stack trace:
System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
[Info] [4/28/2024 8:28:32 PM] Invoking method System.Void VSharp.CSharpUtils.Exceptions.CreateOverflowException()
[Trace] [4/28/2024 8:28:32 PM] Exception thrown (HeapRef 2 to System.OverflowException), StackTrace:
[method = System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
offset = 37]
[Info] [4/28/2024 8:28:32 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_Z(this)
[Info] [4/28/2024 8:28:32 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_Z(this)
[Trace] [4/28/2024 8:28:32 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:28:32 PM] !(null == this) & !(this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField) & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:28:32 PM] SATISFIABLE
[Info] [4/28/2024 8:28:32 PM] System.OverflowException!
Stack trace:
System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
[Info] [4/28/2024 8:28:32 PM] Invoking method System.Void VSharp.CSharpUtils.Exceptions.CreateOverflowException()
[Trace] [4/28/2024 8:28:32 PM] Exception thrown (HeapRef 2 to System.OverflowException), StackTrace:
[method = System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
offset = 3E]
[Info] [4/28/2024 8:28:32 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_X(this)
[Info] [4/28/2024 8:28:32 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_X(this)
[Info] [4/28/2024 8:28:32 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_Y(this)
[Info] [4/28/2024 8:28:32 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_Y(this)
[Trace] [4/28/2024 8:28:32 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:28:32 PM] !(null == this) & !(this.<X>k__BackingField * (no ovf) this.<Y>k__BackingField) & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:28:32 PM] SATISFIABLE
[Info] [4/28/2024 8:28:32 PM] System.OverflowException!
Stack trace:
System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
[Info] [4/28/2024 8:28:32 PM] Invoking method System.Void VSharp.CSharpUtils.Exceptions.CreateOverflowException()
[Trace] [4/28/2024 8:28:32 PM] Exception thrown (HeapRef 2 to System.OverflowException), StackTrace:
[method = System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
offset = 4B]
[Info] [4/28/2024 8:28:32 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_Z(this)
[Info] [4/28/2024 8:28:32 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_Z(this)
[Trace] [4/28/2024 8:28:32 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:28:32 PM] !(null == this) & !(this.<X>k__BackingField * this.<Y>k__BackingField * (no ovf) this.<Z>k__BackingField) & this.<X>k__BackingField * (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:28:32 PM] SATISFIABLE
[Info] [4/28/2024 8:28:32 PM] System.OverflowException!
Stack trace:
System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
[Info] [4/28/2024 8:28:32 PM] Invoking method System.Void VSharp.CSharpUtils.Exceptions.CreateOverflowException()
[Trace] [4/28/2024 8:28:32 PM] Exception thrown (HeapRef 2 to System.OverflowException), StackTrace:
[method = System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
offset = 52]
[Trace] [4/28/2024 8:28:32 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:28:32 PM] !(null == this) & !(this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + (no ovf) this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField) & this.<X>k__BackingField * (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:28:32 PM] SATISFIABLE
[Info] [4/28/2024 8:28:32 PM] System.OverflowException!
Stack trace:
System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
[Info] [4/28/2024 8:28:32 PM] Invoking method System.Void VSharp.CSharpUtils.Exceptions.CreateOverflowException()
[Trace] [4/28/2024 8:28:32 PM] Exception thrown (HeapRef 2 to System.OverflowException), StackTrace:
[method = System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
offset = 53]
[Trace] [4/28/2024 8:28:32 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:28:32 PM] !(1 + (no ovf) this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField) & !(null == this) & this.<X>k__BackingField * (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + (no ovf) this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:28:36 PM] SATISFIABLE
[Info] [4/28/2024 8:28:36 PM] System.OverflowException!
Stack trace:
System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
[Info] [4/28/2024 8:28:36 PM] Invoking method System.Void VSharp.CSharpUtils.Exceptions.CreateOverflowException()
[Trace] [4/28/2024 8:28:36 PM] Exception thrown (HeapRef 2 to System.OverflowException), StackTrace:
[method = System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
offset = 55]
[Trace] [4/28/2024 8:28:36 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:28:36 PM] !(null == this) & 1 + (no ovf) this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField & 1 + this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField == 256 & this.<X>k__BackingField * (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + (no ovf) this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:28:37 PM] SATISFIABLE
[Trace] [4/28/2024 8:28:37 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:28:37 PM] !(1 + this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField == 256) & !(null == this) & 1 + (no ovf) this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField & 1 + this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField == 512 & this.<X>k__BackingField * (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + (no ovf) this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Error] [4/28/2024 8:29:22 PM] Solver returned Status.UNKNOWN. Reason: canceled
Expression: [(bvsle this #x00000000); (let ((a!1 (bvadd (bvadd (select |this.<X>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<X>k__BackingField, |
                                 this)
                         (select |this.<Y>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Y>k__BackingField, |
                                 this))
                  (select |this.<Z>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Z>k__BackingField, |
                          this)))
      (a!2 (bvmul (bvmul (select |this.<X>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<X>k__BackingField, |
                                 this)
                         (select |this.<Y>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Y>k__BackingField, |
                                 this))
                  (select |this.<Z>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Z>k__BackingField, |
                          this)))
      (a!6 (=> (and (bvslt (select |this.<X>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<X>k__BackingField, |
                                   this)
                           #x00000000)
                    (bvslt (select |this.<Y>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Y>k__BackingField, |
                                   this)
                           #x00000000))
               (bvslt (bvadd (select |this.<X>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<X>k__BackingField, |
                                     this)
                             (select |this.<Y>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Y>k__BackingField, |
                                     this))
                      #x00000000)))
      (a!7 (=> (and (bvslt #x00000000
                           (select |this.<X>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<X>k__BackingField, |
                                   this))
                    (bvslt #x00000000
                           (select |this.<Y>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Y>k__BackingField, |
                                   this)))
               (bvslt #x00000000
                      (bvadd (select |this.<X>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<X>k__BackingField, |
                                     this)
                             (select |this.<Y>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Y>k__BackingField, |
                                     this)))))
      (a!8 (and (bvslt (bvadd (select |this.<X>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<X>k__BackingField, |
                                      this)
                              (select |this.<Y>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Y>k__BackingField, |
                                      this))
                       #x00000000)
                (bvslt (select |this.<Z>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Z>k__BackingField, |
                               this)
                       #x00000000)))
      (a!9 (and (bvslt #x00000000
                       (bvadd (select |this.<X>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<X>k__BackingField, |
                                      this)
                              (select |this.<Y>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Y>k__BackingField, |
                                      this)))
                (bvslt #x00000000
                       (select |this.<Z>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Z>k__BackingField, |
                               this)))))
(let ((a!3 (=> (and (bvslt (bvadd a!1 a!2) #x00000000)
                    (bvslt #x00000001 #x00000000))
               (bvslt (bvadd (bvadd a!1 a!2) #x00000001) #x00000000)))
      (a!4 (=> (and (bvslt #x00000000 (bvadd a!1 a!2))
                    (bvslt #x00000000 #x00000001))
               (bvslt #x00000000 (bvadd (bvadd a!1 a!2) #x00000001))))
      (a!5 (not (= (bvadd #x00000001 (bvadd a!1 a!2)) #x00000100))))
  (and a!3
       a!4
       (= (bvadd #x00000001 (bvadd a!1 a!2)) #x00000200)
       a!5
       (bvsmul_noudfl (select |this.<X>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<X>k__BackingField, |
                              this)
                      (select |this.<Y>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Y>k__BackingField, |
                              this))
       (bvsmul_noovfl (select |this.<X>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<X>k__BackingField, |
                              this)
                      (select |this.<Y>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Y>k__BackingField, |
                              this))
       (=> (and (bvslt a!1 #x00000000) (bvslt a!2 #x00000000))
           (bvslt (bvadd a!1 a!2) #x00000000))
       (=> (and (bvslt #x00000000 a!1) (bvslt #x00000000 a!2))
           (bvslt #x00000000 (bvadd a!1 a!2)))
       (bvsmul_noudfl (bvmul (select |this.<X>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<X>k__BackingField, |
                                     this)
                             (select |this.<Y>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Y>k__BackingField, |
                                     this))
                      (select |this.<Z>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Z>k__BackingField, |
                              this))
       (bvsmul_noovfl (bvmul (select |this.<X>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<X>k__BackingField, |
                                     this)
                             (select |this.<Y>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Y>k__BackingField, |
                                     this))
                      (select |this.<Z>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Z>k__BackingField, |
                              this))
       a!6
       a!7
       (bvsgt (select |this.<X>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<X>k__BackingField, |
                      this)
              #x00000000)
       (not (= this #x00000000))
       (bvsgt (select |this.<Y>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Y>k__BackingField, |
                      this)
              #x00000000)
       (=> a!8 (bvslt a!1 #x00000000))
       (=> a!9 (bvslt #x00000000 a!1))
       (bvsgt (select |this.<Z>k__BackingField of HeapField (System.Int32)BranchesAndLoops.SwitchStatement.<Z>k__BackingField, |
                      this)
              #x00000000))))]
[Trace] [4/28/2024 8:29:22 PM] UNKNOWN
[Info] [4/28/2024 8:29:22 PM] Result of method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this) is True
[Trace] [4/28/2024 8:29:22 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:29:22 PM] !(1 + this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField == 256) & !(1 + this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField == 512) & !(null == this) & 1 + (no ovf) this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField & 1 + this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField == 1024 & this.<X>k__BackingField * (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + (no ovf) this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:29:44 PM] SATISFIABLE
The template "NUnit 3 Test Project" was created successfully.

Processing post-creation actions...
Restoring D:\Users\samiull\Documents\2023\testgen\testgen\csharp\out\BranchesAndLoops.Tests\BranchesAndLoops.Tests.csproj:
  Determining projects to restore...
  Restored D:\Users\samiull\Documents\2023\testgen\testgen\csharp\out\BranchesAndLoops.Tests\BranchesAndLoops.Tests.csproj (in 443 ms).
Restore succeeded.

Starting reproducing error1.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
Test error1.vst throws the expected exception System.OverflowException!
error1.vst passed!
Starting reproducing error2.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
Test error2.vst throws the expected exception System.OverflowException!
error2.vst passed!
Starting reproducing error3.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
Test error3.vst throws the expected exception System.OverflowException!
error3.vst passed!
Starting reproducing error4.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
Test error4.vst throws the expected exception System.OverflowException!
error4.vst passed!
Starting reproducing error5.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
Test error5.vst throws the expected exception System.OverflowException!
error5.vst passed!
Starting reproducing error6.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
Test error6.vst throws the expected exception System.OverflowException!
error6.vst passed!
Starting reproducing test1.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
test1.vst passed!
Starting reproducing test2.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
test2.vst passed!
Starting reproducing test3.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
test3.vst passed!
Starting reproducing test4.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
test4.vst passed!
Total time: 00:01:12.880.
Approximate coverage: 75
Test results written to D:\Users\samiull\Documents\2023\testgen\testgen\csharp\out\VSharp.tests.0
Tests generated: 4
Errors generated: 6

samiull@DESKTOP-OS5I16B MINGW64 /d/Users/samiull/Documents/2023/testgen/testgen/csharp/branches-quickstart (mainline)
smhmhmd commented 5 months ago

The "--strat DFS" option also creates a "true branch" testcase, but both runs have overflow exception. I will try one without specifying "--strat" next.

samiull@DESKTOP-OS5I16B MINGW64 /d/Users/samiull/Documents/2023/testgen/testgen/csharp/branches-quickstart (mainline)
$ ./testgen.bat | tee log.txt

D:\Users\samiull\Documents\2023\testgen\testgen\csharp\branches-quickstart>dotnet ..\..\..\testGen\upstream\VSharp\VSharp.Runner\bin\Release\net7.0\VSharp.Runner.dll  --method SimpleSwitchWithAdditionAndMultiplication bin\Debug\net6.0\BranchesAndLoops.dll --strat DFS -t 90 -o ..\out --render-tests --run-tests -v Trace 
[Info] [4/28/2024 8:34:05 PM] Starting to explore method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
[Trace] [4/28/2024 8:34:05 PM] Add CFG for System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this).
[Trace] [4/28/2024 8:34:05 PM] Add CFG for System.Int32 BranchesAndLoops.SwitchStatement.get_X(this).
[Info] [4/28/2024 8:34:05 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_X(this)
[Info] [4/28/2024 8:34:05 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_X(this)
[Trace] [4/28/2024 8:34:05 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:34:05 PM] !(null == this) & this.<X>k__BackingField > 0
[Trace] [4/28/2024 8:34:05 PM] SATISFIABLE
[Trace] [4/28/2024 8:34:05 PM] Add CFG for System.Int32 BranchesAndLoops.SwitchStatement.get_Y(this).
[Info] [4/28/2024 8:34:05 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_Y(this)
[Info] [4/28/2024 8:34:05 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_Y(this)
[Trace] [4/28/2024 8:34:05 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:34:05 PM] !(null == this) & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0
[Trace] [4/28/2024 8:34:05 PM] SATISFIABLE
[Trace] [4/28/2024 8:34:05 PM] Add CFG for System.Int32 BranchesAndLoops.SwitchStatement.get_Z(this).
[Info] [4/28/2024 8:34:05 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_Z(this)
[Info] [4/28/2024 8:34:05 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_Z(this)
[Trace] [4/28/2024 8:34:05 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:34:05 PM] !(null == this) & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:34:05 PM] SATISFIABLE
[Info] [4/28/2024 8:34:05 PM] Result of method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this) is False
[Info] [4/28/2024 8:34:05 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_X(this)
[Info] [4/28/2024 8:34:05 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_X(this)
[Info] [4/28/2024 8:34:05 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_Y(this)
[Info] [4/28/2024 8:34:05 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_Y(this)
[Trace] [4/28/2024 8:34:05 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:34:05 PM] !(null == this) & !(this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField) & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:34:05 PM] SATISFIABLE
[Info] [4/28/2024 8:34:05 PM] System.OverflowException!
Stack trace:
System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
[Info] [4/28/2024 8:34:05 PM] Invoking method System.Void VSharp.CSharpUtils.Exceptions.CreateOverflowException()
[Trace] [4/28/2024 8:34:05 PM] Exception thrown (HeapRef 2 to System.OverflowException), StackTrace:
[method = System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
offset = 37]
[Info] [4/28/2024 8:34:05 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_Z(this)
[Info] [4/28/2024 8:34:05 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_Z(this)
[Trace] [4/28/2024 8:34:05 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:34:05 PM] !(null == this) & !(this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField) & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:34:05 PM] SATISFIABLE
[Info] [4/28/2024 8:34:05 PM] System.OverflowException!
Stack trace:
System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
[Info] [4/28/2024 8:34:05 PM] Invoking method System.Void VSharp.CSharpUtils.Exceptions.CreateOverflowException()
[Trace] [4/28/2024 8:34:05 PM] Exception thrown (HeapRef 2 to System.OverflowException), StackTrace:
[method = System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
offset = 3E]
[Info] [4/28/2024 8:34:05 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_X(this)
[Info] [4/28/2024 8:34:05 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_X(this)
[Info] [4/28/2024 8:34:05 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_Y(this)
[Info] [4/28/2024 8:34:05 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_Y(this)
[Trace] [4/28/2024 8:34:05 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:34:05 PM] !(null == this) & !(this.<X>k__BackingField * (no ovf) this.<Y>k__BackingField) & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:34:05 PM] SATISFIABLE
[Info] [4/28/2024 8:34:06 PM] System.OverflowException!
Stack trace:
System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
[Info] [4/28/2024 8:34:06 PM] Invoking method System.Void VSharp.CSharpUtils.Exceptions.CreateOverflowException()
[Trace] [4/28/2024 8:34:06 PM] Exception thrown (HeapRef 2 to System.OverflowException), StackTrace:
[method = System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
offset = 4B]
[Info] [4/28/2024 8:34:06 PM] Starting to explore method System.Int32 BranchesAndLoops.SwitchStatement.get_Z(this)
[Info] [4/28/2024 8:34:06 PM] Done with method System.Int32 BranchesAndLoops.SwitchStatement.get_Z(this)
[Trace] [4/28/2024 8:34:06 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:34:06 PM] !(null == this) & !(this.<X>k__BackingField * this.<Y>k__BackingField * (no ovf) this.<Z>k__BackingField) & this.<X>k__BackingField * (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:34:06 PM] SATISFIABLE
[Info] [4/28/2024 8:34:06 PM] System.OverflowException!
Stack trace:
System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
[Info] [4/28/2024 8:34:06 PM] Invoking method System.Void VSharp.CSharpUtils.Exceptions.CreateOverflowException()
[Trace] [4/28/2024 8:34:06 PM] Exception thrown (HeapRef 2 to System.OverflowException), StackTrace:
[method = System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
offset = 52]
[Trace] [4/28/2024 8:34:06 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:34:06 PM] !(null == this) & !(this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + (no ovf) this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField) & this.<X>k__BackingField * (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:34:06 PM] SATISFIABLE
[Info] [4/28/2024 8:34:06 PM] System.OverflowException!
Stack trace:
System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
[Info] [4/28/2024 8:34:06 PM] Invoking method System.Void VSharp.CSharpUtils.Exceptions.CreateOverflowException()
[Trace] [4/28/2024 8:34:06 PM] Exception thrown (HeapRef 2 to System.OverflowException), StackTrace:
[method = System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
offset = 53]
[Trace] [4/28/2024 8:34:06 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:34:06 PM] !(1 + (no ovf) this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField) & !(null == this) & this.<X>k__BackingField * (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + (no ovf) this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:34:08 PM] SATISFIABLE
[Info] [4/28/2024 8:34:08 PM] System.OverflowException!
Stack trace:
System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
[Info] [4/28/2024 8:34:08 PM] Invoking method System.Void VSharp.CSharpUtils.Exceptions.CreateOverflowException()
[Trace] [4/28/2024 8:34:08 PM] Exception thrown (HeapRef 2 to System.OverflowException), StackTrace:
[method = System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
offset = 55]
[Trace] [4/28/2024 8:34:08 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:34:08 PM] !(null == this) & 1 + (no ovf) this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField & 1 + this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField == 256 & this.<X>k__BackingField * (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + (no ovf) this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:34:09 PM] SATISFIABLE
[Trace] [4/28/2024 8:34:09 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:34:09 PM] !(1 + this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField == 256) & !(null == this) & 1 + (no ovf) this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField & 1 + this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField == 512 & this.<X>k__BackingField * (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + (no ovf) this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:34:19 PM] SATISFIABLE
[Trace] [4/28/2024 8:34:19 PM] SOLVER: trying to solve constraints...
[Trace] [4/28/2024 8:34:19 PM] !(1 + this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField == 256) & !(1 + this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField == 512) & !(null == this) & 1 + (no ovf) this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField & 1 + this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField == 1024 & this.<X>k__BackingField * (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField * this.<Y>k__BackingField * this.<Z>k__BackingField + (no ovf) this.<X>k__BackingField + this.<Y>k__BackingField + this.<Z>k__BackingField & this.<X>k__BackingField + (no ovf) this.<Y>k__BackingField & this.<X>k__BackingField + this.<Y>k__BackingField + (no ovf) this.<Z>k__BackingField & this.<X>k__BackingField > 0 & this.<Y>k__BackingField > 0 & this.<Z>k__BackingField > 0
[Trace] [4/28/2024 8:34:25 PM] SATISFIABLE
[Info] [4/28/2024 8:34:25 PM] Result of method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this) is False
[Info] [4/28/2024 8:34:25 PM] Result of method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this) is False
[Info] [4/28/2024 8:34:25 PM] Result of method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this) is False
[Info] [4/28/2024 8:34:25 PM] Result of method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this) is True
[Info] [4/28/2024 8:34:25 PM] Result of method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this) is False
The template "NUnit 3 Test Project" was created successfully.

Processing post-creation actions...
Restoring D:\Users\samiull\Documents\2023\testgen\testgen\csharp\out\BranchesAndLoops.Tests\BranchesAndLoops.Tests.csproj:
  Determining projects to restore...
  Restored D:\Users\samiull\Documents\2023\testgen\testgen\csharp\out\BranchesAndLoops.Tests\BranchesAndLoops.Tests.csproj (in 439 ms).
Restore succeeded.

Starting reproducing error1.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
Test error1.vst throws the expected exception System.OverflowException!
error1.vst passed!
Starting reproducing error2.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
Test error2.vst throws the expected exception System.OverflowException!
error2.vst passed!
Starting reproducing error3.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
Test error3.vst throws the expected exception System.OverflowException!
error3.vst passed!
Starting reproducing error4.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
Test error4.vst throws the expected exception System.OverflowException!
error4.vst passed!
Starting reproducing error5.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
Test error5.vst throws the expected exception System.OverflowException!
error5.vst passed!
Starting reproducing error6.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
Test error6.vst throws the expected exception System.OverflowException!
error6.vst passed!
Starting reproducing test1.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
test1.vst passed!
Starting reproducing test2.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
test2.vst passed!
Starting reproducing test3.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
test3.vst passed!
Starting reproducing test4.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
test4.vst passed!
Starting reproducing test5.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
test5.vst passed!
Starting reproducing test6.vst for method System.Boolean BranchesAndLoops.SwitchStatement.SimpleSwitchWithAdditionAndMultiplication(this)
test6.vst passed!
Total time: 00:00:20.534.
Approximate coverage: 100
Test results written to D:\Users\samiull\Documents\2023\testgen\testgen\csharp\out\VSharp.tests.0
Tests generated: 6
Errors generated: 6

samiull@DESKTOP-OS5I16B MINGW64 /d/Users/samiull/Documents/2023/testgen/testgen/csharp/branches-quickstart (mainline)
smhmhmd commented 5 months ago

Hi @MchKosticyn Thank you for the reference https://arxiv.org/pdf/1610.00502

It works without "--strat" option as well. The issue was probably due to other tests, "--method " option made this work.

Thanks again, I will check and file for other issues, if needed.