Don't create trivial labeled assumptions (#823)

Previously, `{:id ...}` attributes were copied from `assert` statements
to `assume` statements unconditionally, even when subsumption was
disabled. This led to `{:id ...}` attributes on `assume true`
statements, which will never be necessary for a proof, so there's no
reason to track them.

Source/VCGeneration/VCGen.cs

@@ -58,9 +58,12 @@ public static AssumeCmd AssertTurnedIntoAssume(VCGenOptions options, AssertCmd a
       }
 
       var assume = new AssumeCmd(assrt.tok, expr);
-      // Copy any {:id ...} from the assertion to the assumption, so
-      // we can track it while analyzing verification coverage.
-      (assume as ICarriesAttributes).CopyIdFrom(assrt.tok, assrt);
+      if (expr != Expr.True) {
+        // Copy any {:id ...} from the assertion to the assumption, so
+        // we can track it while analyzing verification coverage. But
+        // skip it if it's `true` because that's never useful to track.
+        (assume as ICarriesAttributes).CopyIdFrom(assrt.tok, assrt);
+      }
       return assume;
     }