I wonder if you have any assumptions on these three conditions:
```
(bitSizeofType(T) %Int cfg:bitsPerByte ==Int 0)
               andBool (isBitfieldType(T) =/=K true)
               andBool (hasUnionMarker(T) =/=K true)
```

The problem is like:
```
     rule midWriteSpecific(fromUnion(UnionLoc:SymLoc, 
		F:CId, Fields:FieldInfo),Loc:SymLoc,
		V:CValue,.Set,NoUnionSet:Set,ST:SimpleType)
		=> (makeUnknown(UnionLoc, F, Fields)
		   ~> write-specific(Loc, V, t(NoUnionSet,ST)))
	  [structural]

     rule midWriteSpecific(M:Modifier,Loc:SymLoc,
		V:CValue,.Set,NoUnionSet:Set
		,ST:SimpleType) => 
		write-specific(Loc, V, t(SetItem(M) NoUnionSet,ST))
	  when hasUnionMarker(t(SetItem(M),ST)) =/=K true
	  [structural]
```

These two rules are the only two rules which will be transferred back to write-specific and the condition is that 
``
hasUnionMarker(t(SetItem(M),ST)) =/=K true
``

So, it means that if these two conditions:
```
(bitSizeofType(T) %Int cfg:bitsPerByte ==Int 0)
               andBool (isBitfieldType(T) =/=K true)
```
are always true, then there is a infinite loop here. I believe that this is a direct translation from your rule to this rule, I just wonder if it is correct.