A question about BTOR_ENGINE_PROP

[valeryjust]

I have met this situation:
when I set the solver engine BTOR_ENGINE_PROP, and the I set the constraint:
256 wide bit vector var x and y; 256 wide const c; if I set xy>c , the solver will output different model in different solving.
But if I set xy < c , in different solving times, the model is always （x=0, y=0）, how can I get different model just like x*y>c?
(< and > are unsigned)