Add rounding mode visitation to the visitor for CVC5
@@ -331,6 +331,9 @@ public class CVC5FormulaCreator extends FormulaCreator<Term, Sort, Solver, Term>
} else if (f.isFloatingPointValue()) {
return visitor.visitConstant(formula, f.toString());
+ } else if (f.getKind() == Kind.CONST_ROUNDINGMODE) {
+ return visitor.visitConstant(formula, f.toString());
+
} else if (f.getKind() == Kind.VARIABLE) {
// Bound and unbound vars are the same in CVC5!
// BOUND vars are used for all vars that are bound to a quantifier in CVC5.
