fix model evaluation for real-typed integers like '0.0' or '12.0'.
If the target type is REAL, we use Rationals.
@@ -710,7 +710,11 @@ public class CVC5FormulaCreator extends FormulaCreator<Term, Sort, Solver, Term>
return value.getSymbol();
} else if (value.isIntegerValue()) {
+ if (type.isReal()) { // real-based integers like "12.0" are returned as Rationals.
+ return Rational.ofBigInteger(value.getIntegerValue());
+ } else {
return value.getIntegerValue();
+ }
} else if (value.isRealValue()) {
Pair<BigInteger, BigInteger> realValue = value.getRealValue();
