I will provide a simple example below to further explain the question:

Here the result would be: 'x = 19/10.' Which converted to a float would be 'x = 1.9.'

In this case x has 1 decimal place as there is only 1 digit after the '.'

So, I am wondering if there is a way to limit the variable x (in the smt solver: Z3 Theorem Prover) so that it can only have 'y' number of decimal places.