Optimize cterms_anti_unify

[Stevengre]

Currently, the cterms_anti_unify function directly utilizes Cterm.anti_unify to obtain a generalized state. However, it has some issues:

1. It generates more variables than expected. For instance, given states <i> 1 </i>, <i> 2 </i>, and <i> 3 </i>, it returns something like <i> z </i> (z=1 \/ (z=y /\ (y=2 \/ y=3))), whereas I expect it to return <i> z </i> z = 1 \/ z = 2 \/ z = 3.

2. Another issue pertains to merge_node. While it's acceptable for the MergedEdge's left-hand side to use this generalized state to match the rule, the condition cannot be recovered on the right-hand side.

For example, consider the following program:

function f(a):
  if a:
    return 1
  else:
    return 2

The current merged edge is A:Bool => 1 \/ 2, which means the following assertions will fail:

assert f(true) == 1
assert f(false) == 2

I'm uncertain if this behavior aligns with our goals, as it still seems useful for checking certain properties. If not, I don't see any alternative methods other than avoiding merging to retain these conditions. Additionally, there may be three types of specifications in Kontrol and what should be used by the verifier:

1. The minimized version without merging nodes
2. The minimized version with merging nodes
3. User's NatSpec

[Stevengre]

#4645

[Stevengre]

1. construct a tree from top vars (V_0) to bottom vars/tokens (X).
2. given V_n ==K X, replace V_n by V_0
3. lift the constraints
   I'm uncertain whether this algorithm is correct for multiple variables; it needs to be tested on more complex cases.