private void PrintCounterexampleHelper()

in Sources/VeriSol/VeriSolExecuter.cs [287:366]
73 lines of code
15 McCabe index (conditional complexity)

        private void PrintCounterexampleHelper(List<Tuple<string, string>> trace)
        {
            Stack<string> callStack = new Stack<string>();
            string currentArgs = "";
            bool collectArgs = false;
            List<string> resultArray = new List<string>();

            // this is a list of (line#, element)
            // element \in {CALL foo, RETURN from foo, x = e, ASSERTION FAILS, ...}
            for (int i = 0; i < trace.Count(); i++)
            {
                var elem = trace[i].Item2;
                if (elem.StartsWith("CALL CorralChoice_"))
                {
                    continue;
                }
                else if (elem.StartsWith("RETURN from CorralChoice_"))
                {
                    continue;
                }
                else if (elem.StartsWith("CALL "))
                {
                    var func = elem.Substring("CALL ".Length);
                    callStack.Push(func);
                    currentArgs = "";
                }
                else if (elem.StartsWith("RETURN from "))
                {
                    var func = elem.Substring("RETURN from ".Length);
                    Debug.Assert(callStack.Count > 0, "Call stack cannot be empty");
                    Debug.Assert(func.TrimEnd().Equals(callStack.Peek().TrimEnd()), $"Top of stack {callStack.Peek()} does not match with return {func}");
                    callStack.Pop();
                }
                else if (elem.StartsWith("_verisolFirstArg"))
                {
                    collectArgs = true;
                }
                else if (elem.StartsWith("_verisolLastArg"))
                {
                    Debug.Assert(callStack.Count > 0, "callstack cannot be empty");
                    collectArgs = false;
                    if (callStack.Count == 1)
                    {
                        resultArray.Add($"{trace[i].Item1}: {ConvertFunctionName(callStack.Peek())} ({currentArgs.Substring(", ".Length)})");
                    }
                }
                else if (elem.StartsWith("(ASSERTION FAILS"))
                {
                    resultArray.Add($"{trace[i].Item1}: ASSERTION FAILS!");
                }
                else if (elem.Contains("=") && !elem.Contains("=="))
                {

                    if (collectArgs)
                    {
                        // Replace "T@Ref!val!0" with "address!0"
                        string[] splitElem = elem.Split(" = ");
                        Debug.Assert(splitElem.Count() == 2);
                        string[] rhsSplit = splitElem[1].Split("!");
                        if (rhsSplit.Count() > 0 && rhsSplit[0].Equals("T@Ref"))
                        {
                            currentArgs += ", " + elem.Replace("T@Ref!val", "address");
                        }
                        else
                        {
                            currentArgs += ", " + elem;
                        }                       
                    }
                }
                else
                {
                    Debug.Assert(false, $"This should be unreachable, found a new class of statement {elem}");
                }
            }

            resultArray.ForEach(x => Console.WriteLine(x));
            // Only printing counterexample on the command line:
            File.WriteAllLines(counterexampleFileName, resultArray);
            return;
        }