If thereduceUselessLiterals function is not called in every normalization iteration (e.g., just every second or third iteration), the tool frequently hangs in appendBranch.
So it seems that the existence of useless literals breaks something (likely when a rule is applied to the useless literals?).
If the
reduceUselessLiteralsfunction is not called in every normalization iteration (e.g., just every second or third iteration), the tool frequently hangs inappendBranch. So it seems that the existence of useless literals breaks something (likely when a rule is applied to the useless literals?).