Give strictly greater value for x ≥ c

[leduyquang753]

For solving constraints with real numbers, is there a way to make it so that the emitted model gives a strictly greater value for inequalities of the form x ≥ c, where c is a constant (along with other similar inequalities as well)?

For example, if this is run:

(declare-const x Real)
(assert (>= x (/ 1.0 2.75)))
(check-sat)
(get-model)

Z3 gives (define-fun x () Real (/ 4.0 11.0)) which is exactly (/ 1.0 2.75). When applied in tools, the computation of the value might yield some inaccuracies, so it would be more desirable if the returned value could be "nudged" away from the equal value, say to (/ 1.0 2.0) (0,5).

[JoanEspasa]

Would a reformulation approach where you add an epsilon to any value you are interested in work?