Open
Description
All SMT solvers should have a flag, e.g., bool AllowRoundingAlgebraicNumbers, that one has to set to true in contexts where algebraic numbers should be expected and where rounding would be fine. Otherwise, I can see that this could become a somewhat unexpected source of approximation error.
Currently, the only place where SMT results are rounded are after big-step preprocessing.
See the discussion in #627 (comment).
Metadata
Metadata
Assignees
Labels
No labels