fix: Don't consider := * to be definite assignment for non-ghost variables of a (00) type

[RustanLeino]

Fixes #5023

Description

Previously, the verifier allowed := * to satisfy the definite-assignment obligation for any known-to-be-nonempty type, regardless of context. The fix is to use (0), not (00), for non-ghost assignments.

By submitting this pull request, I confirm that my contribution is made under the terms of the MIT license.

[keyboardDrummer]

Repeating my comment on the issue:

Can you elaborate on the meaning of x := * ? If the meaning is "assign any value that satisfies this type", then wouldn't the above be a code generator bug, where the code generator should have either said no non-ghost witness found for assigning to subset type or generated x := 5 ?