diff --git a/RELEASE_NOTES.md b/RELEASE_NOTES.md
index bfeaf217307..6a6855ee00e 100644
--- a/RELEASE_NOTES.md
+++ b/RELEASE_NOTES.md
@@ -6,6 +6,7 @@
   (https://github.com/dafny-lang/dafny/pull/2416)
 - feat: Dafny now supports disjunctive (“or”) patterns in match statements and expressions.  Cases are separated by `|` characters.  Disjunctive patterns may not appear within other patterns and may not bind variables.
   (https://github.com/dafny-lang/dafny/pull/2448)
+- fix: Counterexamples - fix an integer parsing bug and correctly extract datatype and field names (https://github.com/dafny-lang/dafny/pull/2461)
 - feat: New option `-diagnosticsFormat:json` to print Dafny error messages as JSON objects (one per line).
   (https://github.com/dafny-lang/dafny/pull/2363)
 - fix: No more exceptions when hovering over variables without type, and types of local variabled kept under match statements (https://github.com/dafny-lang/dafny/pull/2437)
diff --git a/Source/DafnyDriver/DafnyDriver.cs b/Source/DafnyDriver/DafnyDriver.cs
index 12703e1c088..81559534927 100644
--- a/Source/DafnyDriver/DafnyDriver.cs
+++ b/Source/DafnyDriver/DafnyDriver.cs
@@ -349,7 +349,7 @@ private static void PrintCounterexample(string modelViewFile) {
         var vars = state.ExpandedVariableSet(-1);
         foreach (var variable in vars) {
           Console.WriteLine($"\t{variable.ShortName} : " +
-                            $"{variable.Type.InDafnyFormat()} = " +
+                            $"{DafnyModelTypeUtils.GetInDafnyFormat(variable.Type)} = " +
                             $"{variable.Value}");
         }
       }
diff --git a/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs b/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs
index 8aecbcf41ad..11219b9410c 100644
--- a/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs
+++ b/Source/DafnyLanguageServer.Test/Various/CounterExampleTest.cs
@@ -863,8 +863,8 @@ method test() {
       var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
       Assert.AreEqual(2, counterExamples.Length);
       Assert.AreEqual(1, counterExamples[1].Variables.Count);
-      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int,bool>"));
-      StringAssert.Matches(counterExamples[1].Variables["m:map<int,bool>"], new Regex("\\(.*3 := false.*"));
+      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int, bool>"));
+      StringAssert.Matches(counterExamples[1].Variables["m:map<int, bool>"], new Regex("\\(.*3 := false.*"));
     }
 
     [TestMethod]
@@ -881,15 +881,15 @@ method test(value:int) {
       var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
       Assert.AreEqual(4, counterExamples.Length);
       Assert.AreEqual(2, counterExamples[1].Variables.Count);
-      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int,int>"));
-      StringAssert.Matches(counterExamples[1].Variables["m:map<int,int>"], new Regex("\\(.*3 := -1.*"));
+      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int, int>"));
+      StringAssert.Matches(counterExamples[1].Variables["m:map<int, int>"], new Regex("\\(.*3 := -1.*"));
       Assert.AreEqual(3, counterExamples[3].Variables.Count);
-      Assert.IsTrue(counterExamples[3].Variables.ContainsKey("m:map<int,int>"));
+      Assert.IsTrue(counterExamples[3].Variables.ContainsKey("m:map<int, int>"));
       Assert.IsTrue(counterExamples[3].Variables.ContainsKey("value:int"));
       Assert.IsTrue(counterExamples[3].Variables.ContainsKey("b:bool"));
       Assert.AreEqual("true", counterExamples[3].Variables["b:bool"]);
       StringAssert.Matches(counterExamples[3].Variables["value:int"], new Regex("[1-9][0-9]*"));
-      StringAssert.Matches(counterExamples[3].Variables["m:map<int,int>"], new Regex("\\(.*3 := [1-9].*"));
+      StringAssert.Matches(counterExamples[3].Variables["m:map<int, int>"], new Regex("\\(.*3 := [1-9].*"));
     }
 
     [TestMethod]
@@ -907,13 +907,13 @@ requires key in m.Keys
       var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
       Assert.AreEqual(3, counterExamples.Length);
       Assert.AreEqual(4, counterExamples[2].Variables.Count);
-      Assert.IsTrue(counterExamples[2].Variables.ContainsKey("m:map<int,int>"));
-      Assert.IsTrue(counterExamples[2].Variables.ContainsKey("m':map<int,int>"));
+      Assert.IsTrue(counterExamples[2].Variables.ContainsKey("m:map<int, int>"));
+      Assert.IsTrue(counterExamples[2].Variables.ContainsKey("m':map<int, int>"));
       Assert.IsTrue(counterExamples[2].Variables.ContainsKey("val:int"));
       Assert.IsTrue(counterExamples[2].Variables.ContainsKey("key:int"));
       var key = counterExamples[2].Variables["key:int"];
       var val = counterExamples[2].Variables["val:int"];
-      StringAssert.Matches(counterExamples[2].Variables["m':map<int,int>"], new Regex("\\(.*" + key + " := " + val + ".*"));
+      StringAssert.Matches(counterExamples[2].Variables["m':map<int, int>"], new Regex("\\(.*" + key + " := " + val + ".*"));
     }
 
     [TestMethod]
@@ -930,15 +930,15 @@ method T_map0(m:map<int,int>, key:int, val:int)
       var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
       Assert.AreEqual(2, counterExamples.Length);
       Assert.AreEqual(4, counterExamples[1].Variables.Count);
-      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int,int>"));
-      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m':map<int,int>"));
+      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int, int>"));
+      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m':map<int, int>"));
       Assert.IsTrue(counterExamples[1].Variables.ContainsKey("val:int"));
       Assert.IsTrue(counterExamples[1].Variables.ContainsKey("key:int"));
       var key = counterExamples[1].Variables["key:int"];
       var val = counterExamples[1].Variables["val:int"];
       var mapRegex = new Regex("\\(.*" + key + " := " + val + ".*");
-      Assert.IsTrue(mapRegex.IsMatch(counterExamples[1].Variables["m':map<int,int>"]) ||
-                    mapRegex.IsMatch(counterExamples[1].Variables["m:map<int,int>"]));
+      Assert.IsTrue(mapRegex.IsMatch(counterExamples[1].Variables["m':map<int, int>"]) ||
+                    mapRegex.IsMatch(counterExamples[1].Variables["m:map<int, int>"]));
 
     }
 
@@ -954,9 +954,9 @@ method test(m:map<int,char>) {
       var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
       Assert.AreEqual(2, counterExamples.Length);
       Assert.AreEqual(2, counterExamples[1].Variables.Count);
-      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int,char>"));
+      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int, char>"));
       Assert.IsTrue(counterExamples[1].Variables.ContainsKey("keys:set<int>"));
-      StringAssert.Matches(counterExamples[1].Variables["m:map<int,char>"], new Regex("\\(.*25 := .*"));
+      StringAssert.Matches(counterExamples[1].Variables["m:map<int, char>"], new Regex("\\(.*25 := .*"));
       StringAssert.Matches(counterExamples[1].Variables["keys:set<int>"], new Regex("\\{.*25 := true.*"));
     }
 
@@ -972,9 +972,9 @@ method test(m:map<int,char>) {
       var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
       Assert.AreEqual(2, counterExamples.Length);
       Assert.AreEqual(2, counterExamples[1].Variables.Count);
-      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int,char>"));
+      Assert.IsTrue(counterExamples[1].Variables.ContainsKey("m:map<int, char>"));
       Assert.IsTrue(counterExamples[1].Variables.ContainsKey("values:set<char>"));
-      StringAssert.Matches(counterExamples[1].Variables["m:map<int,char>"], new Regex("\\(.* := 'c'.*"));
+      StringAssert.Matches(counterExamples[1].Variables["m:map<int, char>"], new Regex("\\(.* := 'c'.*"));
       StringAssert.Matches(counterExamples[1].Variables["values:set<char>"], new Regex("\\{.*'c' := true.*"));
     }
 
@@ -992,8 +992,8 @@ method test(m:map<bv2,bv3>) {
       var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
       Assert.AreEqual(1, counterExamples.Length);
       Assert.AreEqual(1, counterExamples[0].Variables.Count);
-      Assert.IsTrue(counterExamples[0].Variables.ContainsKey("m:map<bv2,bv3>"));
-      StringAssert.Matches(counterExamples[0].Variables["m:map<bv2,bv3>"], new Regex("\\(.*[0-9]+ := [0-9]+.*"));
+      Assert.IsTrue(counterExamples[0].Variables.ContainsKey("m:map<bv2, bv3>"));
+      StringAssert.Matches(counterExamples[0].Variables["m:map<bv2, bv3>"], new Regex("\\(.*[0-9]+ := [0-9]+.*"));
     }
 
     [TestMethod]
@@ -1019,61 +1019,73 @@ method test() {
     }
 
     [TestMethod]
-    public void DafnyModelTypeMultipleArguments() {
-      var type = DafnyModelType.FromString("seq<int, char>");
-      Assert.AreEqual("seq", type.Name);
-      Assert.AreEqual(2, type.TypeArgs.Count);
-      Assert.AreEqual("int", type.TypeArgs[0].Name);
-      Assert.AreEqual("char", type.TypeArgs[1].Name);
-      Assert.AreEqual(0, type.TypeArgs[0].TypeArgs.Count);
-      Assert.AreEqual(0, type.TypeArgs[1].TypeArgs.Count);
-    }
+    public async Task UnboundedIntegers() {
+      var source = @"
+      ghost const NAT64_MAX := 0x7fff_ffff_ffff_ffff
 
+      newtype nat64 = x | 0 <= x <= NAT64_MAX
+
+      function method plus(a: nat64, b: nat64): nat64 {
+        a + b
+      }".TrimStart();
+      var documentItem = CreateTestDocument(source);
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
+      Assert.AreEqual(1, counterExamples.Length);
+      Assert.IsTrue(counterExamples[0].Variables.ContainsKey("a:int"));
+      Assert.IsTrue(counterExamples[0].Variables.ContainsKey("b:int"));
+      var a = long.Parse(counterExamples[0].Variables["a:int"]);
+      var b = long.Parse(counterExamples[0].Variables["b:int"]);
+      Assert.IsTrue(a + b < a || a + b < b);
+    }
 
     [TestMethod]
-    public void DafnyModelTypeNestedArguments() {
-      var type = DafnyModelType.FromString("seq<map<char, int>>");
-      Assert.AreEqual("seq", type.Name);
-      Assert.AreEqual(1, type.TypeArgs.Count);
-      Assert.AreEqual("map", type.TypeArgs[0].Name);
-      Assert.AreEqual(2, type.TypeArgs[0].TypeArgs.Count);
-      Assert.AreEqual("char", type.TypeArgs[0].TypeArgs[0].Name);
-      Assert.AreEqual("int", type.TypeArgs[0].TypeArgs[1].Name);
-      Assert.AreEqual(0, type.TypeArgs[0].TypeArgs[0].TypeArgs.Count);
-      Assert.AreEqual(0, type.TypeArgs[0].TypeArgs[1].TypeArgs.Count);
+    public async Task DatatypeWithPredicate() {
+      var source = @"
+      module M {
+        datatype D = C(i:int) {
+          predicate p() {true}
+        }
+
+        method test(d: D) {
+          if (d.p()) {
+            assert d.i != 123;
+          }
+        }
+      }".TrimStart();
+      var documentItem = CreateTestDocument(source);
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
+      Assert.AreEqual(1, counterExamples.Length);
+      Assert.IsTrue(counterExamples[0].Variables.ContainsKey("d:M.D"));
+      Assert.AreEqual("C(i := 123)", counterExamples[0].Variables["d:M.D"]);
     }
 
+    /// <summary>
+    /// Test a situation in which two fields of an object are equal
+    /// (the value is represented by one Element in the Model)
+    /// </summary>
     [TestMethod]
-    public void DafnyModelTypeComplexCase() {
-      var type = DafnyModelType.FromString("Custom<Value<set<map<bv6, real>>>, map<char, int>, array<bool>>");
-      Assert.AreEqual("Custom", type.Name);
-      Assert.AreEqual(3, type.TypeArgs.Count);
-      var arg = type.TypeArgs[0];
-      Assert.AreEqual("Value", arg.Name);
-      Assert.AreEqual(1, arg.TypeArgs.Count);
-      arg = arg.TypeArgs[0];
-      Assert.AreEqual("set", arg.Name);
-      Assert.AreEqual(1, arg.TypeArgs.Count);
-      arg = arg.TypeArgs[0];
-      Assert.AreEqual("map", arg.Name);
-      Assert.AreEqual(2, arg.TypeArgs.Count);
-      Assert.AreEqual("bv6", arg.TypeArgs[0].Name);
-      Assert.AreEqual("real", arg.TypeArgs[1].Name);
-      Assert.AreEqual(0, arg.TypeArgs[0].TypeArgs.Count);
-      Assert.AreEqual(0, arg.TypeArgs[1].TypeArgs.Count);
-      arg = type.TypeArgs[1];
-      Assert.AreEqual("map", arg.Name);
-      Assert.AreEqual(2, arg.TypeArgs.Count);
-      Assert.AreEqual("char", arg.TypeArgs[0].Name);
-      Assert.AreEqual("int", arg.TypeArgs[1].Name);
-      Assert.AreEqual(0, arg.TypeArgs[0].TypeArgs.Count);
-      Assert.AreEqual(0, arg.TypeArgs[1].TypeArgs.Count);
-      arg = type.TypeArgs[2];
-      Assert.AreEqual("array", arg.Name);
-      Assert.AreEqual(1, arg.TypeArgs.Count);
-      arg = arg.TypeArgs[0];
-      Assert.AreEqual("bool", arg.Name);
-      Assert.AreEqual(0, arg.TypeArgs.Count);
+    public async Task EqualFields() {
+      var source = @"
+      module M {
+        class C { 
+          var c1:char;
+          var c2:char;
+        }
+
+        method test(c: C?) {
+          assert c == null || c.c1 != c.c2 || c.c1 != '\u1023';
+        }
+      }".TrimStart();
+      var documentItem = CreateTestDocument(source);
+      await client.OpenDocumentAndWaitAsync(documentItem, CancellationToken);
+      var counterExamples = (await RequestCounterExamples(documentItem.Uri)).ToArray();
+      Assert.AreEqual(1, counterExamples.Length);
+      Assert.IsTrue(counterExamples[0].Variables.ContainsKey("c:M.C?"));
+      Assert.IsTrue(counterExamples[0].Variables["c:M.C?"] is
+        "(c1 := '\\u1023', c2 := '\\u1023')" or
+        "(c2 := '\\u1023', c1 := '\\u1023')");
     }
   }
 }
diff --git a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs
index 16d6f4b1e2e..a05f51f0067 100644
--- a/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs
+++ b/Source/DafnyLanguageServer/Handlers/Custom/DafnyCounterExampleHandler.cs
@@ -99,7 +99,7 @@ private CounterExampleItem GetCounterExample(DafnyModelState state) {
         return new(
           new Position(state.GetLineId() - 1, state.GetCharId()),
           vars.WithCancellation(cancellationToken).ToDictionary(
-            variable => variable.ShortName + ":" + variable.Type.InDafnyFormat(),
+            variable => variable.ShortName + ":" + DafnyModelTypeUtils.GetInDafnyFormat(variable.Type),
             variable => variable.Value
           )
         );
diff --git a/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs b/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs
index 914d05856b3..a944e0d1394 100644
--- a/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs
+++ b/Source/DafnyServer/CounterExampleGeneration/DafnyModel.cs
@@ -9,13 +9,13 @@
 using System.Text.RegularExpressions;
 using Microsoft.Boogie;
 using Microsoft.Dafny;
+using Token = Microsoft.Dafny.Token;
 using Type = Microsoft.Dafny.Type;
 
 namespace DafnyServer.CounterexampleGeneration {
 
   /// <summary>
-  /// a wrapper around Boogie's Model class that
-  /// defines Dafny specific functions and provides functionality for extracting
+  /// A wrapper around Boogie's Model class that allows extracting
   /// types and values of Elements representing Dafny variables. The three core
   /// methods are: GetDafnyType, CanonicalName, and GetExpansion
   /// </summary>
@@ -23,6 +23,8 @@ public class DafnyModel {
 
     public readonly Model Model;
     public readonly List<DafnyModelState> States = new();
+    public static readonly UserDefinedType UnknownType =
+      new(new Token(), "?", null);
     private readonly Model.Func fSetSelect, fSeqLength, fSeqIndex, fBox,
       fDim, fIndexField, fMultiIndexField, fDtype, fCharToInt, fTag, fBv, fType,
       fChar, fNull, fSetUnion, fSetIntersection, fSetDifference, fSetUnionOne,
@@ -31,22 +33,22 @@ public class DafnyModel {
       fMapDomain, fMapElements, fMapBuild, fIs, fIsBox;
     private readonly Dictionary<Model.Element, Model.Element[]> arrayLengths = new();
     private readonly Dictionary<Model.Element, Model.FuncTuple> datatypeValues = new();
-    private readonly Dictionary<Model.Element, string> localValue = new();
 
     // maps a numeric type (int, real, bv4, etc.) to the set of integer
     // values of that type that appear in the model. 
     private readonly Dictionary<Type, HashSet<int>> reservedNumerals = new();
-    // set of all characters values that appear in the model
-    private readonly HashSet<char> reservedChars = new();
-    private bool isTrueReserved = false; // True if "true" appears anywhere in the model
-    // maps an element representing a primitive value to the string representation of that value
+    // set of all UTF values for characters that appear in the model
+    private readonly HashSet<int> reservedChars = new();
+    private bool isTrueReserved; // True if "true" appears anywhere in the model
+    // maps an element representing a primitive to its string representation
     private readonly Dictionary<Model.Element, string> reservedValuesMap = new();
-    // ensures that a given bitvectorType is created only once for a given base
+    // maps width to a unique object representing bitvector type of such width 
     private readonly Dictionary<int, BitvectorType> bitvectorTypes = new();
 
     // the model will begin assigning characters starting from this utf value
-    private static readonly int firstCharacterUtfValue = 65; // 'A'
-    private static readonly Regex bvTypeRegex = new Regex("^bv[0-9]+Type$");
+    private const int FirstCharacterUtfValue = 65; // 'A'
+    private static readonly Regex BvTypeRegex = new("^bv[0-9]+Type$");
+    private static readonly Regex UnderscoreRemovalRegex = new("__");
 
 
     public DafnyModel(Model model) {
@@ -137,7 +139,7 @@ private void InitArraysAndDataTypes() {
         } else if (fn.Name.StartsWith("#") && fn.Name.IndexOf('.') != -1 && fn.Name[1] != '#') {
           foreach (var tpl in fn.Apps) {
             var elt = tpl.Result;
-            datatypeValues.Add(elt, tpl);
+            datatypeValues[elt] = tpl;
           }
         }
       }
@@ -175,11 +177,43 @@ private Model.Func MergeMapSelectFunctions(int arity) {
       return result;
     }
 
-    /// <summary> Registered all char values specified by the model </summary>
+    /// <summary> Register all char values specified by the model </summary>
     private void RegisterReservedChars() {
       foreach (var app in fCharToInt.Apps) {
-        int UTFCode = int.Parse(((Model.Integer)app.Result).Numeral);
-        reservedChars.Add(Convert.ToChar(UTFCode));
+        if (int.TryParse(((Model.Integer)app.Result).Numeral,
+              out var UTFCode) && UTFCode is <= char.MaxValue and >= 0) {
+          reservedChars.Add(UTFCode);
+        }
+      }
+    }
+
+    /// <summary>
+    /// Return the character representation of a UTF code understood by Dafny
+    /// This is either the character itself, if it is a parsable ASCII,
+    /// Escaped character, for the cases specified in Dafny manual,
+    /// Or escaped UTF code otherwise
+    /// </summary>
+    private string PrettyPrintChar(int UTFCode) {
+      switch (UTFCode) {
+        case 0:
+          return "'\\0'";
+        case 9:
+          return "'\\t'";
+        case 10:
+          return "'\\n'";
+        case 13:
+          return "'\\r'";
+        case 34:
+          return "'\\\"'";
+        case 39:
+          return "'\\\''";
+        case 92:
+          return "'\\\\'";
+        default:
+          if ((UTFCode >= 32) && (UTFCode <= 126)) {
+            return $"'{Convert.ToChar(UTFCode)}'";
+          }
+          return $"'\\u{UTFCode:X4}'";
       }
     }
 
@@ -187,8 +221,8 @@ private void RegisterReservedChars() {
     private void RegisterReservedInts() {
       reservedNumerals[Type.Int] = new();
       foreach (var app in fU2Int.Apps) {
-        if (app.Result is Model.Integer integer) {
-          reservedNumerals[Type.Int].Add(integer.AsInt());
+        if (app.Result is Model.Integer integer && int.TryParse(integer.Numeral, out int value)) {
+          reservedNumerals[Type.Int].Add(value);
         }
       }
     }
@@ -231,7 +265,10 @@ private void RegisterReservedBitVectors() {
         }
 
         foreach (var app in func.Apps) {
-          reservedNumerals[type].Add((app.Result as Model.BitVector).AsInt());
+          if (int.TryParse((app.Result as Model.BitVector).Numeral,
+                out var value)) {
+            reservedNumerals[type].Add(value);
+          }
         }
       }
     }
@@ -248,7 +285,7 @@ public static bool IsUserVariableName(string name) =>
     /// instance of Model.BitVector, which is a BitVector value)
     /// </summary>
     private static bool IsBitVectorObject(Model.Element element, DafnyModel model) =>
-      bvTypeRegex.IsMatch(GetTrueName(model.fType.OptEval(element)) ?? "");
+      BvTypeRegex.IsMatch(GetTrueName(model.fType.OptEval(element)) ?? "");
 
     /// <summary>
     /// Return True iff the given element has primitive type in Dafny or is null
@@ -279,9 +316,9 @@ private static string GetTrueName(Model.Element element) {
         if (funcTuple.Func.Arity != 0) {
           continue;
         }
-        if (name == null) {
+        if ((name == null) || name.Contains("$")) { // 2nd case is type param
           name = funcTuple.Func.Name;
-        } else {
+        } else if (!funcTuple.Func.Name.Contains("$")) {
           return null;
         }
       }
@@ -311,16 +348,16 @@ private string GetBoogieType(Model.Element element) {
     }
 
     /// <summary> Get the Dafny type of an element </summary>
-    internal DafnyModelType GetDafnyType(Model.Element element) {
+    internal Type GetDafnyType(Model.Element element) {
       switch (element.Kind) {
         case Model.ElementKind.Boolean:
-          return new DafnyModelType("bool");
+          return Type.Bool;
         case Model.ElementKind.Integer:
-          return new DafnyModelType("int");
+          return Type.Int;
         case Model.ElementKind.Real:
-          return new DafnyModelType("real");
+          return Type.Real;
         case Model.ElementKind.BitVector:
-          return new DafnyModelType("bv" + ((Model.BitVector)element).Size);
+          return new BitvectorType(((Model.BitVector)element).Size);
         case Model.ElementKind.Uninterpreted:
           return GetDafnyType(element as Model.Uninterpreted);
         case Model.ElementKind.DataValue:
@@ -328,9 +365,9 @@ internal DafnyModelType GetDafnyType(Model.Element element) {
             return GetDafnyType(
               ((Model.DatatypeValue)element).Arguments.First());
           }
-          return new DafnyModelType("?"); // This shouldn't be reachable.
+          return UnknownType; // This shouldn't be reachable.
         default:
-          return new DafnyModelType("?");
+          return UnknownType;
       }
     }
 
@@ -348,16 +385,19 @@ internal DafnyModelType GetDafnyType(Model.Element element) {
     }
 
     /// <summary> Get the Dafny type of an Uninterpreted element </summary>
-    private DafnyModelType GetDafnyType(Model.Uninterpreted element) {
+    private Type GetDafnyType(Model.Uninterpreted element) {
       var boogieType = GetBoogieType(element);
       List<Model.Element> isOfType;
-      List<DafnyModelType> typeArgs = new();
+      List<Type> typeArgs = new();
       switch (boogieType) {
         case "intType":
+          return Type.Int;
         case "realType":
+          return Type.Real;
         case "charType":
+          return Type.Char;
         case "boolType":
-          return new DafnyModelType(boogieType.Substring(0, boogieType.Length - 4));
+          return Type.Bool;
         case "SeqType":
           isOfType = GetIsResults(element);
           foreach (var isType in isOfType) {
@@ -379,17 +419,14 @@ private DafnyModelType GetDafnyType(Model.Uninterpreted element) {
           }
           seqOperation = fSeqBuild.AppWithResult(element);
           if (seqOperation != null) {
-            typeArgs.Add(GetDafnyType(Unbox(seqOperation.Args[1])));
-            return new DafnyModelType("seq", typeArgs);
+            return new SeqType(GetDafnyType(Unbox(seqOperation.Args[1])));
           }
           seqOperation = fSeqCreate.AppWithResult(element);
           seqOperation ??= fSeqEmpty.AppWithResult(element);
           if (seqOperation != null) {
-            typeArgs.Add(ReconstructType(seqOperation.Args.First()));
-            return new DafnyModelType("seq", typeArgs);
+            return new SeqType(ReconstructType(seqOperation.Args.First()));
           }
-          typeArgs.Add(new("?"));
-          return new DafnyModelType("seq", typeArgs);
+          return new SeqType(UnknownType);
         case "SetType":
           isOfType = GetIsResults(element);
           foreach (var isType in isOfType) {
@@ -410,22 +447,20 @@ private DafnyModelType GetDafnyType(Model.Uninterpreted element) {
           }
           setOperation = fSetUnionOne.AppWithResult(element);
           if (setOperation != null) {
-            typeArgs.Add(GetDafnyType(Unbox(setOperation.Args[1])));
-            return new DafnyModelType("set", typeArgs);
+            return new SetType(true, GetDafnyType(Unbox(setOperation.Args[1])));
           }
           setOperation = fSetEmpty.AppWithResult(element);
           if (setOperation != null) {
-            typeArgs.Add(ReconstructType(setOperation.Args.First()));
-            return new DafnyModelType("set", typeArgs);
+            return new SetType(true, ReconstructType(setOperation.Args.First()));
           }
-          typeArgs.Add(new("?"));
-          return new DafnyModelType("set", typeArgs);
+          return new SetType(true, UnknownType);
         case "DatatypeTypeType":
           isOfType = GetIsResults(element);
           if (isOfType.Count > 0) {
-            return ReconstructType(isOfType[0]);
+            return new DafnyModelTypeUtils.DatatypeType(
+              (ReconstructType(isOfType[0]) as UserDefinedType) ?? UnknownType);
           }
-          return new DafnyModelType("?");
+          return new DafnyModelTypeUtils.DatatypeType(UnknownType);
         case "MapType":
           isOfType = GetIsResults(element);
           foreach (var isType in isOfType) {
@@ -437,13 +472,22 @@ private DafnyModelType GetDafnyType(Model.Uninterpreted element) {
           if (mapOperation != null) {
             return GetDafnyType(mapOperation.Args.First());
           }
-          return new DafnyModelType("map", new List<DafnyModelType> { new("?"), new("?") });
+          return new Microsoft.Dafny.MapType(true, UnknownType, UnknownType);
         case "refType":
-          return ReconstructType(fDtype.OptEval(element));
+          var typeElement = fDtype.OptEval(element);
+          if (typeElement != null) {
+            return ReconstructType(typeElement);
+          }
+          // if typeElement == null, this object has a null value
+          isOfType = GetIsResults(element);
+          if (isOfType.Count > 0) {
+            return ReconstructType(isOfType[0]);
+          }
+          return UnknownType;
         case null:
-          return new DafnyModelType("?");
-        case var bv when bvTypeRegex.IsMatch(bv):
-          return new DafnyModelType(bv.Substring(0, bv.Length - 4));
+          return UnknownType;
+        case var bv when BvTypeRegex.IsMatch(bv):
+          return new BitvectorType(int.Parse(bv[2..^4]));
         case "BoxType":
           var unboxedTypes = fIsBox.AppsWithArg(0, element)
             .Where(tuple => ((Model.Boolean)tuple.Result).Value)
@@ -451,56 +495,85 @@ private DafnyModelType GetDafnyType(Model.Uninterpreted element) {
           if (unboxedTypes.Count == 1) {
             return ReconstructType(unboxedTypes[0]);
           }
-          return new DafnyModelType("?");
+          return UnknownType;
+        case "HandleTypeType":
+          isOfType = GetIsResults(element);
+          if (isOfType.Count > 0) {
+            return ReconstructType(isOfType[0]);
+          }
+          return UnknownType;
         default:
-          return new DafnyModelType("?");
+          return UnknownType;
       }
     }
 
     /// <summary>
     /// Reconstruct Dafny type from an element that represents a type in Z3
     /// </summary>
-    private DafnyModelType ReconstructType(Model.Element typeElement) {
+    private Type ReconstructType(Model.Element typeElement) {
       if (typeElement == null) {
-        return new DafnyModelType("?");
+        return UnknownType;
       }
       var fullName = GetTrueName(typeElement);
-      if (fullName != null && fullName.Length > 7 && fullName.Substring(0, 7).Equals("Tclass.")) {
-        return new DafnyModelType(fullName.Substring(7));
-      }
-      if (fullName is "TInt" or "TReal" or "TChar" or "TBool") {
-        return new DafnyModelType(fullName.Substring(1).ToLower());
+      if (fullName != null && fullName.Length > 7 && fullName[..7].Equals("Tclass.")) {
+        return new UserDefinedType(new Token(), fullName[7..], null);
+      }
+      switch (fullName) {
+        case "TInt":
+          return Type.Int;
+        case "TBool":
+          return Type.Bool;
+        case "TReal":
+          return Type.Real;
+        case "TChar":
+          return Type.Char;
       }
       if (fBv.AppWithResult(typeElement) != null) {
-        return new DafnyModelType("bv" + ((Model.Integer)fBv.AppWithResult(typeElement).Args[0]).AsInt());
+        return new BitvectorType(((Model.Integer)fBv.AppWithResult(typeElement).Args[0]).AsInt());
       }
+
+      Type fallBackType = UnknownType; // to be returned in the event all else fails
       if (fullName != null) { // this means this is a type variable
-        return new DafnyModelType(fullName);
+        fallBackType = new UserDefinedType(new Token(), fullName, null);
       }
       var tagElement = fTag.OptEval(typeElement);
       if (tagElement == null) {
-        return new DafnyModelType("?");
+        return fallBackType;
       }
       var tagName = GetTrueName(tagElement);
       if (tagName == null || (tagName.Length < 10 && tagName != "TagSeq" &&
                               tagName != "TagSet" &&
                               tagName != "TagBitVector" &&
                               tagName != "TagMap")) {
-        return new DafnyModelType("?");
+        return fallBackType;
       }
       var typeArgs = Model.GetFunc("T" + tagName.Substring(3))?.
         AppWithResult(typeElement)?.
-        Args.ToList();
-      tagName = tagName switch {
-        "TagSeq" => "seq",
-        "TagMap" => "map",
-        "TagSet" => "set",
-        _ => tagName.Substring(9)
-      };
+        Args.Select(e =>
+          GetBoogieType(e) == "DatatypeTypeType" ?
+          new DafnyModelTypeUtils.DatatypeType((ReconstructType(e) as UserDefinedType) ?? UnknownType) :
+          ReconstructType(e)).ToList();
       if (typeArgs == null) {
-        return new DafnyModelType(tagName);
+        return new UserDefinedType(new Token(), tagName.Substring(9), null);
+      }
+
+      switch (tagName) {
+        case "TagSeq":
+          return new SeqType(typeArgs.First());
+        case "TagMap":
+          return new Microsoft.Dafny.MapType(true, typeArgs[0], typeArgs[1]);
+        case "TagSet":
+          return new SetType(true, typeArgs.First());
+        default:
+          tagName = tagName.Substring(9);
+          if (tagName.StartsWith("_System.___hFunc") ||
+              tagName.StartsWith("_System.___hTotalFunc") ||
+              tagName.StartsWith("_System.___hPartialFunc")) {
+            return new ArrowType(new Token(), typeArgs.SkipLast(1).ToList(),
+              typeArgs.Last());
+          }
+          return new UserDefinedType(new Token(), tagName, typeArgs);
       }
-      return new DafnyModelType(tagName, typeArgs.ConvertAll(ReconstructType));
     }
 
     /// <summary>
@@ -519,7 +592,7 @@ public string CanonicalName(Model.Element elt) {
         return elt.ToString();
       }
       if (elt is Model.BitVector vector) {
-        return vector.AsInt().ToString();
+        return vector.Numeral;
       }
       if (IsBitVectorObject(elt, this)) {
         var typeName = GetTrueName(fType.OptEval(elt));
@@ -533,7 +606,7 @@ public string CanonicalName(Model.Element elt) {
           return GetUnreservedNumericValue(elt, bitvectorTypes[width]);
         }
         if (Model.GetFunc(funcName).OptEval(elt) != null) {
-          return Model.GetFunc(funcName).OptEval(elt).AsInt().ToString();
+          return (Model.GetFunc(funcName).OptEval(elt) as Model.Number)?.Numeral;
         }
         return GetUnreservedNumericValue(elt, bitvectorTypes[width]);
       }
@@ -550,10 +623,11 @@ public string CanonicalName(Model.Element elt) {
         return fnTuple.Func.Name.Split(".").Last();
       }
       if (fType.OptEval(elt) == fChar.GetConstant()) {
-        int utfCode;
         if (fCharToInt.OptEval(elt) != null) {
-          utfCode = ((Model.Integer)fCharToInt.OptEval(elt)).AsInt();
-          return "'" + char.ConvertFromUtf32(utfCode) + "'";
+          if (int.TryParse(((Model.Integer)fCharToInt.OptEval(elt)).Numeral,
+                out var UTFCode) && UTFCode is <= char.MaxValue and >= 0) {
+            return PrettyPrintChar(UTFCode);
+          }
         }
         return GetUnreservedCharValue(elt);
       }
@@ -586,12 +660,12 @@ private string GetUnreservedCharValue(Model.Element element) {
       if (reservedValuesMap.TryGetValue(element, out var reservedValue)) {
         return reservedValue;
       }
-      int i = firstCharacterUtfValue;
-      while (reservedChars.Contains(Convert.ToChar(i))) {
+      int i = FirstCharacterUtfValue;
+      while (reservedChars.Contains(i)) {
         i++;
       }
-      reservedValuesMap[element] = $"'{Convert.ToChar(i)}'";
-      reservedChars.Add(Convert.ToChar(i));
+      reservedValuesMap[element] = PrettyPrintChar(i);
+      reservedChars.Add(i);
       return reservedValuesMap[element];
     }
 
@@ -648,7 +722,14 @@ public IEnumerable<DafnyModelVariable> GetExpansion(DafnyModelState state, Dafny
 
       if (datatypeValues.TryGetValue(var.Element, out var fnTuple)) {
         // Elt is a datatype value
-        var destructors = GetDestructorFunctions(var.Element, var.Type.Name).OrderBy(f => f.Name).ToList();
+        var destructors = GetDestructorFunctions(var.Element).OrderBy(f => f.Name).ToList();
+        if (destructors.Count > fnTuple.Args.Length) {
+          // Try to filter out predicate functions
+          // (that follow a format very similar to that of destructor names)
+          destructors = destructors.Where(destructor =>
+              fnTuple.Args.Any(arg => destructor.OptEval(var.Element) == arg))
+            .ToList();
+        }
         if (destructors.Count == fnTuple.Args.Length) {
           // we know all destructor names
           foreach (var func in destructors) {
@@ -679,7 +760,7 @@ public IEnumerable<DafnyModelVariable> GetExpansion(DafnyModelState state, Dafny
         for (int i = 0; i < elements.Count; i++) {
           var e = DafnyModelVariableFactory.Get(state, Unbox(elements[i]), "[" + i + "]", var);
           result.Add(e);
-          (var as SeqVariable)?.AddAtIndex(e, i);
+          (var as SeqVariable)?.AddAtIndex(e, i.ToString());
         }
         if (elements.Count > 0) {
           return result;
@@ -689,7 +770,7 @@ public IEnumerable<DafnyModelVariable> GetExpansion(DafnyModelState state, Dafny
           var e = DafnyModelVariableFactory.Get(state, Unbox(tpl.Result),
             "[" + tpl.Args[1] + "]", var);
           result.Add(e);
-          (var as SeqVariable)?.AddAtIndex(e, (tpl.Args[1] as Model.Integer)?.AsInt());
+          (var as SeqVariable)?.AddAtIndex(e, tpl.Args[1].ToString());
         }
         return result;
       }
@@ -710,8 +791,9 @@ public IEnumerable<DafnyModelVariable> GetExpansion(DafnyModelState state, Dafny
       var mapElements = fMapElements.OptEval(var.Element);
       var mapBuild = fMapBuild.AppWithResult(var.Element);
       while (mapBuild != null) {
-        var key = DafnyModelVariableFactory.Get(state, Unbox(mapBuild.Args[1]), "", var);
-        var value = DafnyModelVariableFactory.Get(state, Unbox(mapBuild.Args[2]), "", var);
+        var pairId = var.Children.Count.ToString();
+        var key = DafnyModelVariableFactory.Get(state, Unbox(mapBuild.Args[1]), pairId, var);
+        var value = DafnyModelVariableFactory.Get(state, Unbox(mapBuild.Args[2]), pairId, var);
         result.Add(key);
         result.Add(value);
         ((MapVariable)var).AddMapping(key, value);
@@ -727,13 +809,14 @@ public IEnumerable<DafnyModelVariable> GetExpansion(DafnyModelState state, Dafny
           if (!((Model.Boolean)app.Result).Value) {
             continue;
           }
-          var key = DafnyModelVariableFactory.Get(state, Unbox(app.Args[1]), "", var);
+          var pairId = var.Children.Count.ToString();
+          var key = DafnyModelVariableFactory.Get(state, Unbox(app.Args[1]), pairId, var);
           result.Add(key);
           var valueElement = fSetSelect.OptEval(mapElements, app.Args[1]);
           if (valueElement == null) {
             ((MapVariable)var).AddMapping(key, null);
           } else {
-            var value = DafnyModelVariableFactory.Get(state, Unbox(valueElement), "", var);
+            var value = DafnyModelVariableFactory.Get(state, Unbox(valueElement), pairId, var);
             result.Add(value);
             ((MapVariable)var).AddMapping(key, value);
           }
@@ -759,9 +842,10 @@ public IEnumerable<DafnyModelVariable> GetExpansion(DafnyModelState state, Dafny
         return result;
       }
       foreach (var tpl in fSetSelect.AppsWithArg(0, instances.ToList()[0].Result)) {
-        var fieldName = GetFieldName(tpl.Args[1]);
-        if (fieldName != "alloc") {
-          result.Add(DafnyModelVariableFactory.Get(state, Unbox(tpl.Result), fieldName, var));
+        foreach (var fieldName in GetFieldNames(tpl.Args[1])) {
+          if (fieldName != "alloc") {
+            result.Add(DafnyModelVariableFactory.Get(state, Unbox(tpl.Result), fieldName, var));
+          }
         }
       }
       return result;
@@ -771,12 +855,14 @@ public IEnumerable<DafnyModelVariable> GetExpansion(DafnyModelState state, Dafny
     /// Return all functions that map the datatype object to a particular
     /// destructor value.
     /// </summary>
-    private static List<Model.Func> GetDestructorFunctions(Model.Element datatype, string type) {
+    private List<Model.Func> GetDestructorFunctions(Model.Element datatypeElement) {
+      var types = GetIsResults(datatypeElement).Select(isResult =>
+        new DafnyModelTypeUtils.DatatypeType(ReconstructType(isResult) as UserDefinedType ?? UnknownType).Name);
       List<Model.Func> result = new();
       var builtInDatatypeDestructor = new Regex("^.*[^_](__)*_q$");
-      foreach (var app in datatype.References) {
-        if (app.Func.Arity != 1 || app.Args[0] != datatype ||
-            !app.Func.Name.StartsWith(type + ".") ||
+      foreach (var app in datatypeElement.References) {
+        if (app.Func.Arity != 1 || app.Args[0] != datatypeElement ||
+            !types.Any(type => app.Func.Name.StartsWith(type + ".")) ||
             builtInDatatypeDestructor.IsMatch(app.Func.Name.Split(".").Last())) {
           continue;
         }
@@ -789,14 +875,17 @@ public IEnumerable<DafnyModelVariable> GetExpansion(DafnyModelState state, Dafny
     /// Return the name of the field represented by the given element.
     /// Special care is required if the element represents an array index
     /// </summary>
-    private string GetFieldName(Model.Element elt) {
-      int? dims = fDim.OptEval(elt)?.AsInt();
+    private List<string> GetFieldNames(Model.Element elt) {
+      if (elt == null) {
+        return new List<string>();
+      }
+      var dims = fDim.OptEval(elt)?.AsInt();
       if (dims is null or 0) { // meaning elt is not an array index
-        var fieldName = GetTrueName(elt);
-        if (fieldName == null) {
-          return elt.ToString();
-        }
-        return fieldName.Split(".").Last();
+        return elt.Names.Where(tuple =>
+          tuple.Func.Arity == 0 && !tuple.Func.Name.Contains("$"))
+          .Select(tuple => UnderscoreRemovalRegex
+            .Replace(tuple.Func.Name.Split(".").Last(), "_"))
+          .ToList();
       }
       // Reaching this code means elt is an index into an array
       var indices = new Model.Element[(int)dims];
@@ -811,8 +900,10 @@ private string GetFieldName(Model.Element elt) {
           elt = dimTuple.Args[0];
         }
       }
-      return "[" + string.Join(",", indices.ToList().
-        ConvertAll(element => element.ToString())) + "]";
+      return new List<string>() {
+        "[" + string.Join(",",
+          indices.ToList().ConvertAll(element => element.ToString())) + "]"
+      };
     }
 
     /// <summary> Unboxes an element, if possible </summary>
@@ -820,53 +911,5 @@ private Model.Element Unbox(Model.Element elt) {
       var unboxed = fBox.AppWithResult(elt);
       return unboxed != null ? unboxed.Args[0] : elt;
     }
-
-    public void RegisterLocalValue(string name, Model.Element elt) {
-      if (localValue.TryGetValue(elt, out var curr) &&
-          CompareFieldNames(name, curr) >= 0) {
-        return;
-      }
-      localValue[elt] = name;
-    }
-
-    private static ulong GetNumber(string s, int beg) {
-      ulong res = 0;
-      while (beg < s.Length) {
-        char c = s[beg];
-        if ('0' <= c && c <= '9') {
-          res *= 10;
-          res += (uint)c - '0';
-        }
-        beg++;
-      }
-      return res;
-    }
-
-    private static int CompareFieldNames(string f1, string f2) {
-      int len = Math.Min(f1.Length, f2.Length);
-      int numberPos = -1;
-      for (int i = 0; i < len; ++i) {
-        char c1 = f1[i];
-        char c2 = f2[i];
-        if ('0' <= c1 && c1 <= '9' && '0' <= c2 && c2 <= '9') {
-          numberPos = i;
-          break;
-        }
-        if (c1 != c2) {
-          break;
-        }
-      }
-      if (numberPos >= 0) {
-        ulong v1 = GetNumber(f1, numberPos);
-        ulong v2 = GetNumber(f2, numberPos);
-        if (v1 < v2) {
-          return -1;
-        }
-        if (v1 > v2) {
-          return 1;
-        }
-      }
-      return string.CompareOrdinal(f1, f2);
-    }
   }
 }
diff --git a/Source/DafnyServer/CounterExampleGeneration/DafnyModelState.cs b/Source/DafnyServer/CounterExampleGeneration/DafnyModelState.cs
index 12b5f1bef0e..4775c7c741c 100644
--- a/Source/DafnyServer/CounterExampleGeneration/DafnyModelState.cs
+++ b/Source/DafnyServer/CounterExampleGeneration/DafnyModelState.cs
@@ -10,8 +10,7 @@
 namespace DafnyServer.CounterexampleGeneration {
 
   /// <summary>
-  /// Represents a state in a `DafnyModel` and captures the values of all
-  /// variables at a particular point in the code.
+  /// Represents a program state in a DafnyModel
   /// </summary>
   public class DafnyModelState {
 
@@ -19,31 +18,34 @@ public class DafnyModelState {
     internal readonly Model.CapturedState State;
     internal int VarIndex; // used to assign unique indices to variables
     private readonly List<DafnyModelVariable> vars;
-    private readonly List<DafnyModelVariable> skolems;
-    // The following map helps to avoid the creation of multiple variables for
-    // the same element.
+    private readonly List<DafnyModelVariable> boundVars;
+    // varMap prevents the creation of multiple variables for the same element.
     private readonly Dictionary<Model.Element, DafnyModelVariable> varMap;
-    private readonly Dictionary<string, int> varNamesMap;
+    // varNameCount keeps track of the number of variables with the same name.
+    // Name collision can happen in the presence of an old expression,
+    // for instance, in which case the it is important to distinguish between
+    // two variables that have the same name using an index provided by Boogie
+    private readonly Dictionary<string, int> varNameCount;
 
     private const string InitialStateName = "<initial>";
-    private static Regex statePositionRegex = new(
+    private static readonly Regex StatePositionRegex = new(
       @".*\((?<line>\d+),(?<character>\d+)\)",
       RegexOptions.IgnoreCase | RegexOptions.Singleline
     );
 
-    public DafnyModelState(DafnyModel model, Model.CapturedState state) {
+    internal DafnyModelState(DafnyModel model, Model.CapturedState state) {
       Model = model;
       State = state;
       VarIndex = 0;
       vars = new();
       varMap = new();
-      varNamesMap = new();
-      skolems = new List<DafnyModelVariable>(SkolemVars());
+      varNameCount = new();
+      boundVars = new(BoundVars());
       SetupVars();
     }
 
     /// <summary>
-    /// Start with the union of vars and skolems and expand it by adding the
+    /// Start with the union of vars and boundVars and expand the set by adding 
     /// variables that represent fields of any object in the original set or
     /// elements of any sequence in the original set, etc. This is done
     /// recursively in breadth-first order and only up to a certain maximum
@@ -52,13 +54,13 @@ public DafnyModelState(DafnyModel model, Model.CapturedState state) {
     /// <param name="maxDepth">The maximum depth up to which to expand the
     /// variable set. Can be null to indicate that there is no limit</param>
     /// <returns>List of variables</returns>
-    public HashSet<DafnyModelVariable> ExpandedVariableSet(int? maxDepth) {
+    public HashSet<DafnyModelVariable> ExpandedVariableSet(int maxDepth) {
       HashSet<DafnyModelVariable> expandedSet = new();
       // The following is the queue for elements to be added to the set. The 2nd
       // element of a tuple is the depth of the variable w.r.t. the original set
       List<Tuple<DafnyModelVariable, int>> varsToAdd = new();
-      vars.ForEach(variable => varsToAdd.Add(new Tuple<DafnyModelVariable, int>(variable, 0)));
-      skolems.ForEach(variable => varsToAdd.Add(new Tuple<DafnyModelVariable, int>(variable, 0)));
+      vars.ForEach(variable => varsToAdd.Add(new(variable, 0)));
+      boundVars.ForEach(variable => varsToAdd.Add(new(variable, 0)));
       while (varsToAdd.Count != 0) {
         var (next, depth) = varsToAdd[0];
         varsToAdd.RemoveAt(0);
@@ -72,59 +74,61 @@ public HashSet<DafnyModelVariable> ExpandedVariableSet(int? maxDepth) {
         // fields of primitive types are skipped:
         foreach (var v in next.GetExpansion().
             Where(variable => !expandedSet.Contains(variable) && !variable.IsPrimitive)) {
-          varsToAdd.Add(new Tuple<DafnyModelVariable, int>(v, depth + 1));
+          varsToAdd.Add(new(v, depth + 1));
         }
       }
       return expandedSet;
     }
 
-    public bool ExistsVar(Model.Element element) {
+    internal bool ExistsVar(Model.Element element) {
       return varMap.ContainsKey(element);
     }
 
-    public void AddVar(Model.Element element, DafnyModelVariable var) {
+    internal void AddVar(Model.Element element, DafnyModelVariable var) {
       if (!ExistsVar(element)) {
         varMap[element] = var;
       }
     }
 
-    public DafnyModelVariable GetVar(Model.Element element) {
+    internal DafnyModelVariable GetVar(Model.Element element) {
       return varMap[element];
     }
 
-    public void AddVarName(string name) {
-      varNamesMap[name] = varNamesMap.GetValueOrDefault(name, 0) + 1;
+    internal void AddVarName(string name) {
+      varNameCount[name] = varNameCount.GetValueOrDefault(name, 0) + 1;
     }
 
-    public bool VarNameIsShared(string name) {
-      return varNamesMap.GetValueOrDefault(name, 0) > 1;
+    internal bool VarNameIsShared(string name) {
+      return varNameCount.GetValueOrDefault(name, 0) > 1;
     }
 
     public string FullStateName => State.Name;
 
-    public string ShortenedStateName => ShortenName(State.Name, 20);
+    private string ShortenedStateName => ShortenName(State.Name, 20);
 
     public bool IsInitialState => FullStateName.Equals(InitialStateName);
 
     public int GetLineId() {
-      var match = statePositionRegex.Match(ShortenedStateName);
+      var match = StatePositionRegex.Match(ShortenedStateName);
       if (!match.Success) {
-        throw new ArgumentException($"state does not contain position: {ShortenedStateName}");
+        throw new ArgumentException(
+          $"state does not contain position: {ShortenedStateName}");
       }
       return int.Parse(match.Groups["line"].Value);
     }
 
     public int GetCharId() {
-      var match = statePositionRegex.Match(ShortenedStateName);
+      var match = StatePositionRegex.Match(ShortenedStateName);
       if (!match.Success) {
-        throw new ArgumentException($"state does not contain position: {ShortenedStateName}");
+        throw new ArgumentException(
+          $"state does not contain position: {ShortenedStateName}");
       }
       return int.Parse(match.Groups["character"].Value);
     }
 
     /// <summary>
     /// Initialize the vars list, which stores all variables relevant to
-    /// the counterexample except for Skolem constants
+    /// the counterexample except for the bound variables
     /// </summary>
     private void SetupVars() {
       var names = Enumerable.Empty<string>();
@@ -133,7 +137,6 @@ private void SetupVars() {
         names = prev.vars.ConvertAll(variable => variable.Name);
       }
       names = names.Concat(State.Variables).Distinct();
-      var curVars = State.Variables.ToDictionary(x => x);
       foreach (var v in names) {
         if (!DafnyModel.IsUserVariableName(v)) {
           continue;
@@ -142,18 +145,16 @@ private void SetupVars() {
         if (val == null) {
           continue; // This variable has no value in the model, so ignore it.
         }
+
         var vn = DafnyModelVariableFactory.Get(this, val, v, duplicate: true);
-        if (curVars.ContainsKey(v)) {
-          Model.RegisterLocalValue(vn.Name, val);
-        }
         vars.Add(vn);
       }
     }
 
     /// <summary>
-    /// Return list of variables associated with Skolem constants
+    /// Return list of bound variables
     /// </summary>
-    private IEnumerable<DafnyModelVariable> SkolemVars() {
+    private IEnumerable<DafnyModelVariable> BoundVars() {
       foreach (var f in Model.Model.Functions) {
         if (f.Arity != 0) {
           continue;
@@ -166,6 +167,7 @@ private IEnumerable<DafnyModelVariable> SkolemVars() {
         if (!name.Contains('#')) {
           continue;
         }
+
         yield return DafnyModelVariableFactory.Get(this, f.GetConstant(), name,
           null, true);
       }
diff --git a/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs b/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs
deleted file mode 100644
index 7c7ff374908..00000000000
--- a/Source/DafnyServer/CounterExampleGeneration/DafnyModelType.cs
+++ /dev/null
@@ -1,113 +0,0 @@
-using System;
-using System.Collections.Generic;
-using System.Text.RegularExpressions;
-
-namespace DafnyServer.CounterexampleGeneration {
-  /// <summary>
-  /// Represents the type of a DafnyModelVariable.
-  /// </summary>
-  public class DafnyModelType {
-
-    public readonly string Name;
-    public readonly List<DafnyModelType> TypeArgs;
-
-    private static readonly Regex ModuleSeparatorRegex = new("(?<=[^_](__)*)_m");
-    private static readonly Regex UnderscoreRemovalRegex = new("__");
-
-    public DafnyModelType(string name, IEnumerable<DafnyModelType> typeArgs) {
-      Name = name;
-      TypeArgs = new List<DafnyModelType>(typeArgs);
-    }
-
-    public DafnyModelType(string name) :
-      this(name, new List<DafnyModelType>()) {
-    }
-
-    public override string ToString() {
-      if (TypeArgs.Count == 0) {
-        return Name;
-      }
-      return Name + "<" + string.Join(",", TypeArgs) + ">";
-    }
-
-    /// <summary>
-    /// Recursively convert this type's name and the names of its type arguments
-    /// to the Dafny format. So, for instance,
-    /// Mo__dule___mModule2__.Cla____ss is converted to
-    /// Mo_dule_.Module2_.Cla__ss
-    /// </summary>
-    public DafnyModelType InDafnyFormat() {
-      // The line below converts "_m" used in boogie to separate modules to ".":
-      var newName = ModuleSeparatorRegex.Replace(Name, ".");
-      // strip everything after @, this is done for type variables:
-      newName = newName.Split("@")[0];
-      // The code below converts every "__" to "_":
-      newName = UnderscoreRemovalRegex.Replace(newName, "_");
-      return new(newName, TypeArgs.ConvertAll(type => type.InDafnyFormat()));
-    }
-
-    public DafnyModelType GetNonNullable() {
-      var newName = Name.Trim('?');
-      return new DafnyModelType(newName, TypeArgs);
-    }
-
-    public DafnyModelType ReplaceTypeVariables(DafnyModelType with) {
-      // Assigns the given value to all type variables
-      if (Name.Contains("$")) {
-        return with;
-      }
-      return new(Name, TypeArgs.ConvertAll(type =>
-        type.ReplaceTypeVariables(with)));
-    }
-
-    public override int GetHashCode() {
-      int hash = Name.GetHashCode();
-      foreach (var typ in TypeArgs) {
-        hash = 31 * typ.GetHashCode();
-      }
-      return hash;
-    }
-
-    public override bool Equals(object other) {
-      if (other is not DafnyModelType typ) {
-        return false;
-      }
-      return typ.ToString() == ToString();
-    }
-
-    /// <summary>
-    /// Parse a string into a type.
-    /// </summary>
-    public static DafnyModelType FromString(string type) {
-      type = Regex.Replace(type, " ", "");
-      if (!type.Contains("<")) {
-        return new DafnyModelType(type);
-      }
-      List<DafnyModelType> typeArgs = new();
-      int id = type.IndexOf("<", StringComparison.Ordinal);
-      var name = type[..id];
-      id++; // skip the first '<' since it opens the argument list
-      int lastId = id;
-      int openBrackets = 0;
-      while (id < type.Length) {
-        switch (type[id]) {
-          case '<':
-            openBrackets += 1;
-            break;
-          case '>':
-            openBrackets -= 1;
-            break;
-          case ',':
-            if (openBrackets == 0) { // Skip ',' belonging to nested types
-              typeArgs.Add(FromString(type.Substring(lastId, id - lastId)));
-              lastId = id + 1;
-            }
-            break;
-        }
-        id++;
-      }
-      typeArgs.Add(FromString(type.Substring(lastId, id - lastId - 1)));
-      return new DafnyModelType(name, typeArgs);
-    }
-  }
-}
\ No newline at end of file
diff --git a/Source/DafnyServer/CounterExampleGeneration/DafnyModelTypeUtils.cs b/Source/DafnyServer/CounterExampleGeneration/DafnyModelTypeUtils.cs
new file mode 100644
index 00000000000..ee5ad4c60a5
--- /dev/null
+++ b/Source/DafnyServer/CounterExampleGeneration/DafnyModelTypeUtils.cs
@@ -0,0 +1,117 @@
+// Copyright by the contributors to the Dafny Project
+// SPDX-License-Identifier: MIT
+
+using System;
+using System.Linq;
+using System.Text.RegularExpressions;
+using Microsoft.Dafny;
+using MapType = Microsoft.Dafny.MapType;
+using Token = Microsoft.Dafny.Token;
+using Type = Microsoft.Dafny.Type;
+
+namespace DafnyServer.CounterexampleGeneration {
+
+  /// <summary>
+  /// This class stores various transformations that could be useful to perform
+  /// on types extracted from DafnyModel (e.g. to convert Boogie type names
+  /// back to the original Dafny names)
+  /// </summary>
+  public static class DafnyModelTypeUtils {
+
+    private static readonly Regex ModuleSeparatorRegex = new("(?<=[^_](__)*)_m");
+    private static readonly Regex UnderscoreRemovalRegex = new("__");
+
+    // Used to distinguish between class types and algebraic datatypes
+    public class DatatypeType : UserDefinedType {
+      public DatatypeType(UserDefinedType type)
+        : base(new Token(), type.Name, type.TypeArgs) { }
+    }
+
+    public static Type GetNonNullable(Type type) {
+      if (type is not UserDefinedType userType) {
+        return type;
+      }
+
+      var newType = new UserDefinedType(new Token(),
+        userType.Name.TrimEnd('?'), userType.TypeArgs);
+      if (type is DatatypeType) {
+        return new DatatypeType(newType);
+      }
+      return newType;
+    }
+
+    public static Type ReplaceTypeVariables(Type type, Type with) {
+      return ReplaceType(type, t => t.Name.Contains('$'), _ => with);
+    }
+
+    /// <summary>
+    /// Recursively replace all types within <param>type</param> that satisfy
+    /// <param>condition</param>
+    /// </summary>
+    public static Type ReplaceType(Type type, Func<UserDefinedType, Boolean> condition,
+      Func<UserDefinedType, Type> replacement) {
+      if ((type is not UserDefinedType userType) || (type is ArrowType)) {
+        return TransformType(type, t => ReplaceType(t, condition, replacement));
+      }
+      var newType = condition(userType) ? replacement(userType) : type;
+      newType.TypeArgs = newType.TypeArgs.ConvertAll(t =>
+        TransformType(t, t => ReplaceType(t, condition, replacement)));
+      if (newType is not UserDefinedType newUserType) {
+        return newType;
+      }
+      // The copying above is required to update the NamePath so it takes into
+      // account the changes to TypeArgs made above
+      newUserType = new UserDefinedType(newUserType.tok, newUserType.Name,
+        newUserType.TypeArgs);
+      if (newType is DatatypeType) {
+        return new DatatypeType(newUserType);
+      }
+      return newUserType;
+    }
+
+    public static Type GetInDafnyFormat(Type type) {
+      if ((type is not UserDefinedType userType) || (type is ArrowType)) {
+        return TransformType(type, GetInDafnyFormat);
+      }
+      // The line below converts "_m" used in boogie to separate modules to ".":
+      var newName = ModuleSeparatorRegex.Replace(userType.Name, ".");
+      // strip everything after @, this is done for type variables:
+      newName = newName.Split("@")[0];
+      // The code below converts every "__" to "_":
+      newName = UnderscoreRemovalRegex.Replace(newName, "_");
+      var newType = new UserDefinedType(new Token(), newName,
+        type.TypeArgs.ConvertAll(t => TransformType(t, GetInDafnyFormat)));
+      if (type is DatatypeType) {
+        return new DatatypeType(newType);
+      }
+      return newType;
+    }
+
+    /// <summary>
+    /// Recursively transform all UserDefinedType objects within a given type
+    /// </summary>
+    public static Type TransformType(Type type, Func<UserDefinedType, Type> transform) {
+      switch (type) {
+        case Microsoft.Dafny.BasicType:
+          return type;
+        case MapType mapType:
+          return new MapType(mapType.Finite,
+            TransformType(mapType.Domain, transform),
+            TransformType(mapType.Range, transform));
+        case SeqType seqType:
+          return new SeqType(TransformType(seqType.Arg, transform));
+        case SetType setType:
+          return new SetType(setType.Finite, TransformType(setType.Arg, transform));
+        case MultiSetType multiSetType:
+          return new MultiSetType(TransformType(multiSetType, transform));
+        case ArrowType arrowType:
+          return new ArrowType(new Token(),
+            arrowType.Args.Select(t => TransformType(t, transform)).ToList(),
+            TransformType(arrowType.Result, transform));
+        case UserDefinedType userDefinedType:
+          return transform(userDefinedType);
+      }
+      return type;
+    }
+  }
+}
\ No newline at end of file
diff --git a/Source/DafnyServer/CounterExampleGeneration/DafnyModelVariable.cs b/Source/DafnyServer/CounterExampleGeneration/DafnyModelVariable.cs
index 7d241b91ad7..8d6594e6ef8 100644
--- a/Source/DafnyServer/CounterExampleGeneration/DafnyModelVariable.cs
+++ b/Source/DafnyServer/CounterExampleGeneration/DafnyModelVariable.cs
@@ -6,6 +6,8 @@
 using System.Linq;
 using System.Text.RegularExpressions;
 using Microsoft.Boogie;
+using Microsoft.Dafny;
+using MapType = Microsoft.Dafny.MapType;
 
 namespace DafnyServer.CounterexampleGeneration {
 
@@ -42,13 +44,12 @@ public static DafnyModelVariable Get(DafnyModelState state,
         }
         return new DuplicateVariable(state, state.GetVar(element), name, parent);
       }
-      if (state.Model.GetDafnyType(element).Name == "seq") {
-        return new SeqVariable(state, element, name, parent);
-      }
-      if (state.Model.GetDafnyType(element).Name == "map") {
-        return new MapVariable(state, element, name, parent);
-      }
-      return new DafnyModelVariable(state, element, name, parent);
+
+      return state.Model.GetDafnyType(element) switch {
+        SeqType _ => new SeqVariable(state, element, name, parent),
+        MapType _ => new MapVariable(state, element, name, parent),
+        _ => new DafnyModelVariable(state, element, name, parent)
+      };
     }
   }
 
@@ -60,27 +61,24 @@ public static DafnyModelVariable Get(DafnyModelState state,
   public class DafnyModelVariable {
 
     public readonly string Name; // name given to the variable at creation
-    public readonly DafnyModelType Type; // Dafny type of the variable
+    public readonly Microsoft.Dafny.Type Type; // Dafny type of the variable
     public readonly Model.Element Element;
+    // Maps a field name, sequence index, or some other identifier to
+    // a list of DafnyModelVariables that represent the corresponding value
+    private readonly Dictionary<string, List<DafnyModelVariable>> children;
     private readonly DafnyModelState state; // the associated captured state
-    // A child is a field or a value at a given index of an array, etc.
-    // This dictionary associates a child name with resp. variable:
-    // several children can have same names (particularly, sets can have
-    // many children called true and falls)
-    public readonly Dictionary<string, HashSet<DafnyModelVariable>> children;
+    public virtual Dictionary<string, List<DafnyModelVariable>> Children => children;
 
     internal DafnyModelVariable(DafnyModelState state, Model.Element element,
       string name, DafnyModelVariable parent) {
       this.state = state;
       Element = element;
       Type = state.Model.GetDafnyType(element);
-      children = new Dictionary<string, HashSet<DafnyModelVariable>>();
+      children = new Dictionary<string, List<DafnyModelVariable>>();
       state.AddVar(element, this);
       if (parent == null) {
         Name = name;
       } else {
-        // TODO: a case can be made for refactoring this so that the indices
-        // are model-wide rather than state-wide
         Name = "@" + state.VarIndex++;
         parent.AddChild(name, this);
       }
@@ -91,6 +89,10 @@ public virtual IEnumerable<DafnyModelVariable> GetExpansion() {
       return state.Model.GetExpansion(state, this);
     }
 
+    public string CanonicalName() {
+      return state.Model.CanonicalName(Element);
+    }
+
     public virtual string Value {
       get {
         var result = state.Model.CanonicalName(Element);
@@ -109,7 +111,7 @@ public virtual string Value {
           }
         }
         string childValues;
-        if (Type.Name == "set") {
+        if (Type is SetType) {
           childValues = string.Join(", ",
             childList.ConvertAll(tpl => tpl.Item2 + " := " + tpl.Item1));
           return result + "{" + childValues + "}";
@@ -137,7 +139,7 @@ internal void AddChild(string name, DafnyModelVariable child) {
     }
 
     public override int GetHashCode() {
-      return Element.Id;
+      return Element.Id.GetHashCode();
     }
 
     public override bool Equals(object obj) {
@@ -145,7 +147,9 @@ public override bool Equals(object obj) {
         return false;
       }
 
-      return other.Element == Element && other.state == state && other.Name == Name;
+      return other.Element == Element &&
+             other.state == state &&
+             other.Name == Name;
     }
   }
 
@@ -157,86 +161,97 @@ public class DuplicateVariable : DafnyModelVariable {
 
     public readonly DafnyModelVariable Original;
 
-    internal DuplicateVariable(DafnyModelState state, DafnyModelVariable original, string newName, DafnyModelVariable parent)
+    internal DuplicateVariable(DafnyModelState state,
+      DafnyModelVariable original, string newName, DafnyModelVariable parent)
       : base(state, original.Element, newName, parent) {
       Original = original;
     }
 
     public override string Value => Original.ShortName;
 
+    public override Dictionary<string, List<DafnyModelVariable>> Children => Original.Children;
+
     public override IEnumerable<DafnyModelVariable> GetExpansion() {
       return Original.GetExpansion();
     }
   }
 
   /// <summary>
-  /// a variable that represents a sequence. Allows displaying the sequence
-  /// using Dafny syntax.
+  /// A variable that represents a sequence. 
   /// </summary>
   public class SeqVariable : DafnyModelVariable {
 
     private DafnyModelVariable seqLength;
-    private readonly Dictionary<int, DafnyModelVariable> seqElements;
+    // Dafny integers are unbounded, hence using strings for seq indices:
+    private readonly Dictionary<string, DafnyModelVariable> seqElements;
 
-    internal SeqVariable(DafnyModelState state, Model.Element element, string name, DafnyModelVariable parent)
+    internal SeqVariable(DafnyModelState state, Model.Element element,
+      string name, DafnyModelVariable parent)
       : base(state, element, name, parent) {
       seqLength = null;
-      seqElements = new Dictionary<int, DafnyModelVariable>();
+      seqElements = new Dictionary<string, DafnyModelVariable>();
     }
 
     public override string Value {
       get {
-        int? length = GetLength();
-        if (length == null || seqElements.Count != length) {
+        var length = GetLength();
+        if (length == -1 || seqElements.Count != length) {
           return base.Value;
         }
         List<string> result = new();
         for (int i = 0; i < length; i++) {
-          if (!seqElements.ContainsKey(i)) {
+          var id = i.ToString();
+          if (!seqElements.ContainsKey(id)) {
             return base.Value;
           }
-          result.Add(seqElements[i].IsPrimitive ?
-            seqElements[i].Value :
-            seqElements[i].ShortName);
+          result.Add(seqElements[id].IsPrimitive ?
+            seqElements[id].Value :
+            seqElements[id].ShortName);
         }
         return "[" + string.Join(", ", result) + "]";
       }
     }
 
-    public int? GetLength() {
-      return (seqLength?.Element as Model.Integer)?.AsInt();
+    public int GetLength() {
+      if (int.TryParse((seqLength?.Element as Model.Integer)?.Numeral,
+            out var value)) {
+        return value;
+      }
+      return -1;
     }
 
-    public DafnyModelVariable this[int index] => seqElements.GetValueOrDefault(index, null);
+    public DafnyModelVariable this[int index] => seqElements.GetValueOrDefault(index.ToString(), null);
 
     public void SetLength(DafnyModelVariable seqLength) {
       this.seqLength = seqLength;
     }
 
-    public void AddAtIndex(DafnyModelVariable e, int? index) {
+    public void AddAtIndex(DafnyModelVariable e, string index) {
       if (index == null) {
         return;
       }
-      seqElements[(int)index] = e;
+      seqElements[index] = e;
     }
   }
 
   /// <summary>
-  /// a variable that represents a map. Allows adding mappings to the map and
-  /// displaying the map using Dafny syntax.
+  /// A variable that represents a map.
   /// </summary>
   public class MapVariable : DafnyModelVariable {
 
-    public readonly Dictionary<DafnyModelVariable, DafnyModelVariable> Mappings = new();
+    public readonly Dictionary<DafnyModelVariable, DafnyModelVariable>
+      Mappings = new();
 
-    internal MapVariable(DafnyModelState state, Model.Element element, string name, DafnyModelVariable parent) : base(state, element, name, parent) { }
+    internal MapVariable(DafnyModelState state, Model.Element element,
+      string name, DafnyModelVariable parent)
+      : base(state, element, name, parent) { }
 
     public override string Value {
       get {
         if (Mappings.Count == 0) {
           return "()";
         }
-        // maps a key value pair to how many times it appears in the map
+        // maps a key-value pair to how many times it appears in the map
         // a key value pair can appear many times in a map due to "?:int" etc.
         Dictionary<string, int> mapStrings = new();
         foreach (var key in Mappings.Keys) {
@@ -248,13 +263,17 @@ public override string Value {
               : Mappings[key].Name;
           }
           var mapString = keyString + " := " + valueString;
-          mapStrings[mapString] = mapStrings.GetValueOrDefault(mapString, 0) + 1;
+          mapStrings[mapString] =
+            mapStrings.GetValueOrDefault(mapString, 0) + 1;
         }
+
         return "(" + string.Join(", ", mapStrings.Keys.ToList()
-          .ConvertAll(keyValuePair =>
-            mapStrings[keyValuePair] == 1 ?
-              keyValuePair :
-              keyValuePair + " [+" + (mapStrings[keyValuePair] - 1) + "]")) + ")";
+                 .ConvertAll(keyValuePair =>
+                   mapStrings[keyValuePair] == 1
+                     ? keyValuePair
+                     : keyValuePair + " [+" + (mapStrings[keyValuePair] - 1) +
+                       "]")) +
+               ")";
       }
     }
 
diff --git a/Source/DafnyServer/CounterExampleGeneration/README.md b/Source/DafnyServer/CounterExampleGeneration/README.md
index a65fc01b7d7..42d4b3d2b86 100644
--- a/Source/DafnyServer/CounterExampleGeneration/README.md
+++ b/Source/DafnyServer/CounterExampleGeneration/README.md
@@ -11,5 +11,5 @@ The following is a class-by-class description of the files in this directory int
   - `DuplicateVariable` - a variable that has a different name but represents the same `Element` in the same `DafnyModelState` as some other variable.
   - `MapVariable` - a variable that represents a map. Allows adding mappings to the map and displaying the map using Dafny syntax.
   - `SeqVariable` - a variable that represents a sequence. Allows displaying the sequence using Dafny syntax.
-- [DafnyModelVariableFactory](DafnyModelVariable.cs) - A static class for generating instance of `DafnyModelvariable` and its subclasses. The factory chooses which subclass of `DafnyModelVariable` to employ depending on the `DafnyModelType` of the `Element` for which the variable is generated.
-- [DafnyModelType](DafnyModelType.cs) - Represents the type of a `DafnyModelVariable`. The `InDafnyFormat` method allows to reconstruct the original Dafny type name from its Boogie translation (e.g. `Mo_dule_.Module2_.Cla__ss` from `Mo__dule___mModule2__.Cla____ss`).
+- [DafnyModelVariableFactory](DafnyModelVariable.cs) - A static class for generating instance of `DafnyModelvariable` and its subclasses. The factory chooses which subclass of `DafnyModelVariable` to employ depending on the `Microsoft.Dafny.Type` of the `Element` for which the variable is generated.
+- [DafnyModelType](DafnyModelTypeUtils.cs) - Contains a set of utils for manipulating type objects (e.g. reconstructing the original Dafny type name from its Boogie translation: `Mo_dule_.Module2_.Cla__ss` from `Mo__dule___mModule2__.Cla____ss`).
diff --git a/Source/DafnyTestGeneration/DafnyInfo.cs b/Source/DafnyTestGeneration/DafnyInfo.cs
index b111f62412c..4de1d0309e3 100644
--- a/Source/DafnyTestGeneration/DafnyInfo.cs
+++ b/Source/DafnyTestGeneration/DafnyInfo.cs
@@ -9,12 +9,14 @@ public class DafnyInfo {
 
     // method -> list of return types
     private readonly Dictionary<string, List<string>> returnTypes;
+    private readonly Dictionary<string, List<Type>> formalsTypes;
     private readonly HashSet<string> isStatic; // static methods
     // import required to access the code contained in the program
     public readonly HashSet<string> ToImport;
 
     public DafnyInfo(Program program) {
       returnTypes = new Dictionary<string, List<string>>();
+      formalsTypes = new Dictionary<string, List<Type>>();
       isStatic = new HashSet<string>();
       ToImport = new HashSet<string>();
       var visitor = new DafnyInfoExtractor(this);
@@ -25,6 +27,10 @@ public IList<string> GetReturnTypes(string method) {
       return returnTypes[method];
     }
 
+    public IList<Type> GetFormalsTypes(string method) {
+      return formalsTypes[method];
+    }
+
     public bool IsStatic(string method) {
       return isStatic.Contains(method);
     }
@@ -106,8 +112,10 @@ private void Visit(MemberDecl d) {
         if (m.HasStaticKeyword || !insideAClass) {
           info.isStatic.Add(methodName);
         }
-        var returnTypes = m.Outs.Select(arg => arg.Type.ToString()).ToList();
-        info.returnTypes[methodName] = returnTypes;
+
+        info.returnTypes[methodName] =
+          m.Outs.Select(arg => arg.Type.ToString()).ToList();
+        info.formalsTypes[methodName] = m.Ins.Select(arg => arg.Type).ToList();
       }
 
       private new void Visit(Function f) {
@@ -118,8 +126,11 @@ private void Visit(MemberDecl d) {
         if (f.HasStaticKeyword || !insideAClass) {
           info.isStatic.Add(methodName);
         }
-        var returnTypes = new List<string> { f.ResultType.ToString() };
-        info.returnTypes[methodName] = returnTypes;
+
+        info.returnTypes[methodName] = new List<string>
+          { f.ResultType.ToString() };
+        info.formalsTypes[methodName] =
+          f.Formals.Select(arg => arg.Type).ToList();
       }
     }
   }
diff --git a/Source/DafnyTestGeneration/TestMethod.cs b/Source/DafnyTestGeneration/TestMethod.cs
index 945f55b75c5..4bd73549a1e 100644
--- a/Source/DafnyTestGeneration/TestMethod.cs
+++ b/Source/DafnyTestGeneration/TestMethod.cs
@@ -3,6 +3,8 @@
 using System.Text.RegularExpressions;
 using DafnyServer.CounterexampleGeneration;
 using Microsoft.Boogie;
+using Microsoft.Dafny;
+using MapType = Microsoft.Dafny.MapType;
 using Type = Microsoft.Dafny.Type;
 
 namespace DafnyTestGeneration {
@@ -13,7 +15,7 @@ public class TestMethod {
     private static int nextId; // next unique id to be assigned
 
     // list of values to mock together with their types
-    public readonly List<(string id, DafnyModelType type)> ObjectsToMock = new();
+    public readonly List<(string id, Type type)> ObjectsToMock = new();
     // maps a variable that is mocked to its unique id
     private readonly Dictionary<DafnyModelVariable, string> mockedVarId = new();
     public readonly List<(string parentId, string fieldName, string childId)> Assignments = new();
@@ -26,13 +28,13 @@ public class TestMethod {
     // number of type parameters for the method (all will be set to defaultType)
     public readonly int NOfTypeParams;
     // default type to replace any type variable with
-    private readonly DafnyModelType defaultType = new("int");
+    private readonly Type defaultType = Type.Int;
     // the DafnyModel that describes the inputs to this test method
     private readonly DafnyModel dafnyModel;
 
     // Set of all types for which a {:synthesize} - annotated method is needed
     // These methods are used to get fresh instances of the corresponding types
-    private static readonly HashSet<DafnyModelType> TypesToSynthesize = new();
+    private static readonly HashSet<string> TypesToSynthesize = new();
 
     public TestMethod(DafnyInfo dafnyInfo, string log) {
       DafnyInfo = dafnyInfo;
@@ -53,8 +55,8 @@ public static void ClearTypesToSynthesize() {
     /// Returns the name given to a {:synthesize} - annotated method that
     /// returns a value of certain type
     /// </summary>
-    private static string GetSynthesizeMethodName(DafnyModelType typ) {
-      return "getFresh" + Regex.Replace(typ.ToString(), "[^a-zA-Z]", "");
+    private static string GetSynthesizeMethodName(string typ) {
+      return "getFresh" + Regex.Replace(typ, "[^a-zA-Z]", "");
     }
 
     /// <summary>
@@ -85,13 +87,13 @@ public static string EmitSynthesizeMethods() {
     /// <returns></returns>
     private List<string> ExtractInputs(DafnyModelState state, IReadOnlyList<string> printOutput, IReadOnlyList<string> types) {
       var result = new List<string>();
-      var vars = state.ExpandedVariableSet(null);
-      for (var i = 0; i < printOutput.Count; i++) {
-        if (types[i] == "Ty") {
-          continue; // this means that this parameter is a type variable
-        }
+      var vars = state.ExpandedVariableSet(-1);
+      for (var i = NOfTypeParams; i < printOutput.Count; i++) {
         if (printOutput[i] == "") {
-          result.Add(GetDefaultValue(DafnyModelType.FromString(types[i])));
+          var formalIndex = DafnyInfo.IsStatic(MethodName) ?
+            i - NOfTypeParams :
+            i - NOfTypeParams - 1;
+          result.Add(GetDefaultValue(DafnyInfo.GetFormalsTypes(MethodName)[formalIndex]));
           continue;
         }
         if (!printOutput[i].StartsWith("T@")) {
@@ -133,26 +135,26 @@ private string ExtractVariable(DafnyModelVariable variable) {
       }
 
       List<string> elements = new();
-      var variableType = variable.Type.ReplaceTypeVariables(defaultType);
-      if (variableType.Equals(defaultType) && !variableType.Equals(variable.Type)) {
+      var variableType = DafnyModelTypeUtils.GetInDafnyFormat(
+        DafnyModelTypeUtils.ReplaceTypeVariables(variable.Type, defaultType));
+      if (variableType.ToString() == defaultType.ToString() &&
+          variableType.ToString() != variable.Type.ToString()) {
         return GetADefaultTypeValue(variable);
       }
-      switch (variableType.Name) {
-        case "?":
-          return "null";
-        case "char":
-        case "int":
-        case "real":
-        case "bool":
-        case var bvType when new Regex("^bv[0-9]+$").IsMatch(bvType):
+      switch (variableType) {
+        case CharType:
+        case IntType:
+        case RealType:
+        case BoolType:
+        case BitvectorType:
           return variable.Value;
-        case "seq":
+        case SeqType:
           var seqVar = variable as SeqVariable;
-          if (seqVar?.GetLength() == null) {
+          if (seqVar?.GetLength() == -1) {
             return "[]";
           }
-          for (var i = 0; i < seqVar.GetLength(); i++) {
-            var element = seqVar[i];
+          for (var i = 0; i < seqVar?.GetLength(); i++) {
+            var element = seqVar?[i];
             if (element == null) {
               elements.Add(GetDefaultValue(variableType.TypeArgs.First()));
               continue;
@@ -160,36 +162,39 @@ private string ExtractVariable(DafnyModelVariable variable) {
             elements.Add(ExtractVariable(element));
           }
           return $"[{string.Join(", ", elements)}]";
-        case "set":
-          if (!variable.children.ContainsKey("true")) {
+        case SetType:
+          if (!variable.Children.ContainsKey("true")) {
             return "{}";
           }
-          foreach (var element in variable.children["true"]) {
+          foreach (var element in variable.Children["true"]) {
             elements.Add(ExtractVariable(element));
           }
           return $"{{{string.Join(", ", elements)}}}";
-        case "map":
+        case MapType:
           var mapVar = variable as MapVariable;
           List<string> mappingStrings = new();
           foreach (var mapping in mapVar?.Mappings ?? new()) {
             mappingStrings.Add($"{ExtractVariable(mapping.Key)} := {ExtractVariable(mapping.Value)}");
           }
           return $"map[{string.Join(", ", mappingStrings)}]";
-        case var arrType when new Regex("^_System.array[0-9]*\\?$").IsMatch(arrType):
+        case UserDefinedType arrType when new Regex("^_System.array[0-9]*\\?$").IsMatch(arrType.Name):
           break;
-        case var _ when (!variable.Value.StartsWith("(") && variable.Value != "null"):
+        case DafnyModelTypeUtils.DatatypeType:
           return "DATATYPES_NOT_SUPPORTED";
+        case UserDefinedType userDefinedType when userDefinedType.Name == DafnyModel.UnknownType.Name:
+        case UserDefinedType _ when variable.CanonicalName() == "null":
+          return "null";
         default:
           var varId = $"v{ObjectsToMock.Count}";
-          var dafnyType = variableType.GetNonNullable().InDafnyFormat();
+          var dafnyType = DafnyModelTypeUtils.GetNonNullable(variableType);
           ObjectsToMock.Add(new(varId, dafnyType));
-          TypesToSynthesize.Add(dafnyType);
+          TypesToSynthesize.Add(dafnyType.ToString());
           mockedVarId[variable] = varId;
-          foreach (var filedName in variable.children.Keys) {
-            if (variable.children[filedName].Count != 1) {
+          foreach (var filedName in variable.Children.Keys) {
+            if (variable.Children[filedName].Count != 1) {
               continue;
             }
-            Assignments.Add(new(varId, filedName, ExtractVariable(variable.children[filedName].First())));
+            Assignments.Add(new(varId, filedName, ExtractVariable(variable.Children[filedName].First())));
           }
           return varId;
       }
@@ -202,18 +207,18 @@ private string ExtractVariable(DafnyModelVariable variable) {
     /// An unspecified value is such a value for which a model does reserve
     /// an element (e.g. T@U!val!25).
     /// </summary>
-    private string GetDefaultValue(DafnyModelType type) {
-      type = type.ReplaceTypeVariables(defaultType);
-      var result = type.Name switch {
-        "char" => "\'a\'",
-        "bool" => "false",
-        "int" => "0",
-        "real" => "0.0",
-        "seq" => "[]",
-        "set" => "{}",
-        "map" => "map[]",
-        var bv when new Regex("^bv[0-9]+$").IsMatch(bv) => $"(0 as {bv})",
-        var nullable when new Regex("^.*?$").IsMatch(nullable) => "null",
+    private string GetDefaultValue(Type type) {
+      type = DafnyModelTypeUtils.ReplaceTypeVariables(type, defaultType);
+      var result = type switch {
+        CharType => "\'a\'",
+        BoolType => "false",
+        IntType => "0",
+        RealType => "0.0",
+        SeqType => "[]",
+        SetType => "{}",
+        MapType => "map[]",
+        BitvectorType bvType => $"(0 as {bvType})",
+        UserDefinedType userDefinedType when userDefinedType.Name.EndsWith("?") => "null",
         _ => null
       };
       if (result != null) {
@@ -222,7 +227,7 @@ private string GetDefaultValue(DafnyModelType type) {
       // this should only be reached if the type is non-nullable
       var varId = $"v{ObjectsToMock.Count}";
       ObjectsToMock.Add(new(varId, type));
-      TypesToSynthesize.Add(type);
+      TypesToSynthesize.Add(type.ToString());
       return varId;
     }
 
@@ -261,7 +266,7 @@ private List<string> TestMethodLines() {
       // test method parameters and declaration:
       var mockedLines = ObjectsToMock
         .Select(kVPair => $"var {kVPair.id} := " +
-                          $"{GetSynthesizeMethodName(kVPair.type)}();");
+                          $"{GetSynthesizeMethodName(kVPair.type.ToString())}();");
       var returnParNames = new List<string>();
       for (var i = 0; i < DafnyInfo.GetReturnTypes(MethodName).Count; i++) {
         returnParNames.Add("r" + i);