fix: Expect that subset-type base type can be a non-reference trait

Source/DafnyCore/Verifier/BoogieGenerator.Types.cs

@@ -862,6 +862,9 @@ Expression Zero(IToken tok, Type typ) {
       return null;
     } else if (typ.IsAbstractType || typ.IsInternalTypeSynonym) {
       return null;
+    } else if (typ.IsTraitType) {
+      Contract.Assert(options.Get(CommonOptionBag.GeneralTraits) != CommonOptionBag.GeneralTraitsOptions.Legacy);
+      return null;
     } else {
       Contract.Assume(false);  // unexpected type
       return null;

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4946b.dfy

@@ -0,0 +1,7 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --general-traits=legacy
+
+trait GeneralTrait { }
+trait ReferenceTrait extends object { }
+
+type SubsetType = x: GeneralTrait | true // error: cannot find witness (tried null)
+type Reference = x: ReferenceTrait | true // error: cannot find witness (tried null)

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4946b.dfy.expect

@@ -0,0 +1,4 @@
+git-issue-4946b.dfy(6,5): Error: trying witness null: value of expression (of type 'GeneralTrait?') is not known to be an instance of type 'GeneralTrait', because it might be null
+git-issue-4946b.dfy(7,5): Error: trying witness null: value of expression (of type 'ReferenceTrait?') is not known to be an instance of type 'ReferenceTrait', because it might be null
+
+Dafny program verifier finished with 0 verified, 2 errors

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4946c.dfy

@@ -0,0 +1,7 @@
+// RUN: %testDafnyForEachResolver --expect-exit-code=4 "%s" -- --general-traits=datatype
+
+trait GeneralTrait { }
+trait ReferenceTrait extends object { }
+
+type SubsetType = x: GeneralTrait | true // error: cannot find witness (didn't try anything)
+type Reference = x: ReferenceTrait | true // error: cannot find witness (tried null)

Source/IntegrationTests/TestFiles/LitTests/LitTest/git-issues/git-issue-4946c.dfy.expect

@@ -0,0 +1,4 @@
+git-issue-4946c.dfy(6,5): Error: cannot find witness that shows type is inhabited; try giving a hint through a 'witness' or 'ghost witness' clause, or use 'witness *' to treat as a possibly empty type
+git-issue-4946c.dfy(7,5): Error: trying witness null: value of expression (of type 'ReferenceTrait?') is not known to be an instance of type 'ReferenceTrait', because it might be null
+
+Dafny program verifier finished with 0 verified, 2 errors