Necessary improvements to approximation

[Broes De Cat]

Unnestterms should introduce new types where possible to prevent iterating over too large types. Also non-arithmetic equality should be moved upwards when possible.

See example in attachment, which generates the following bdd, where exists(STRING) should not be present.

EXISTS(string) { EXISTS(string) { append<ct>(<0>[string],<1>[string]) = var2[newstring] FALSE BRANCH: false TRUE BRANCH: =(<0>[string],Hello[string]) FALSE BRANCH: false TRUE BRANCH: true } FALSE BRANCH: false TRUE BRANCH: =(<0>[string], world[string]) FALSE BRANCH: false TRUE BRANCH: true } FALSE BRANCH: false TRUE BRANCH: true

[Broes De Cat]

Will be fixed (as many other examples) by better bdd algorithm.