basic-branch Counterexample Analysis::hasCounterexample wrongly returns false sometimes #2
Description
It considers trees such as the below not to contain counterexamples when they clearly do.
location: I_push[1[int]] V[]
HYP (initial suffix): PIV: {}
SDT: []-+
[]-TRUE: s1
[]-TRUE: s2
[Leaf-]
SUL (initial suffix): PIV: {}
SDT: []-+
[]-(s1=c1)
| []-TRUE: s2
| [Leaf+]
+-(s1!=c1)
[]-TRUE: s2
[Leaf-]
The way the expression is constructed should be reviewed. In my mind, hasCounterexample is akin to asking whether the two SDT's are not equivalent.