In reply to boryah:
I believe your problem has nothing to do with the tool, I tried your code on 3 simulators all failing due to the same conflict, as stated by the LRM random variables as arguments in functions gets solved first in your case you got b = 3 → foo(3) = 0 which makes a = 0 and in your constraint you are defining a inside {[1:5]} which contradicts the result, maybe you can add some guard or explain a bit further what you want to achieve so people can suggest a different approach.
HTH,
-R