The number of variables in the input (and internally) should be reduced as much as possible.

[Broes De Cat]

If the input contains sentences of the form !x: x=1 & Q(x) => ... they should be transformed into Q(1) => ... which can be handled better (approximation is cheaper e.g.).

Should also happen before grounder creation?

[Bart Bogaerts]

I don't think it will be that easy to detect this kind of things. Whether we can replace x in the entire formula by "1" will depend on a lot of things... (exists vs forall, negations,...) Think this through before implementing a fix!