Fix icp candidate parsing (#8137)

Fix icp candidate parsing (#8137)

For constraints of the form c * x ~ poly(x) where c != 1 we would sometimes forget to take the inverse of c when parsing the assertion to the internal representation of the ICP solver. This PR fixes this issue, and does a few more changes:

--nl-icp is really not well-tested and disabled by default. We make it an expert option.
we no longer issue the propagation lemmas if we already found a conflict
the nl-icp trace was heavily polluted by output from the interval utils, which are now moved to a new nl-icp-debug trace
Fixes #8135.