someplaceguy

I found a similar issue with a different arithmetic operator. This succeeds: ```python > intLib.ARITH_PROVE ``&x % 1 >= 0i``; ``` But this fails: ```python > intLib.ARITH_PROVE ``&x % &Num...

I also found an issue only containing integers. These succeed: ```python > intLib.ARITH_PROVE ``ABS 1 = 1``; > intLib.ARITH_PROVE ``1 % 1 = 0``; ``` But this fails: ```python >...

Goals containing `quot` or `rem` also fail (even though the same goals containing `/` and `%` succeed), e.g.: ```python > intLib.ARITH_PROVE ``x quot 42 intLib.ARITH_PROVE ``x rem 42 < 42``;...

@mn200 Thank you for looking into this and for fixing #1203! Unfortunately, I still cannot remove the workaround for #1203 from HolSmt because now I'm experiencing a slightly different issue....

Would it be easy to change `EVALn` such that `EVALn 1` is guaranteed to make at least one reduction (assuming that it's possible to make one)? Right now, this doesn't...

Sorry, please feel free to ignore my last comment. It turns out that my feature request would not actually be useful for my purposes and it might even be detrimental...

Also, the following succeeds: `x 0r ==> x < 0 \/ x > 0` But the following fails: `x 0r ==> 1/x < 0 \/ 1/x > 0`

Ah, I think this is nonlinear arithmetic, so it's probably expected. Feel free to close the issue and sorry for the noise!

I have simply removed the `std::round` on my local Hydra and it has been working great for me for a couple of months now. The workload is distributed much better...

> It is back to being floats! I don't understand. Wasn't this issue about the rounding, which causes the load to be distributed unevenly across the remote machines? Based on...