SyGuS: Add fp.sub to default FP grammar. (#5206)

diff --git a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
index ba9962bd9c1ec723d4224461cf6e835ba02c9f34..e5cc5460dbf91a87410d437bcad0de7bf6321c52 100644 (file)
--- a/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
+++ b/src/theory/quantifiers/sygus/sygus_grammar_cons.cpp
@@ -874,6 +874,7 @@ void CegGrammarConstructor::mkSygusDefaultGrammar(
       // ternary ops with RM
       std::vector<Kind> ternary_rm_kinds = {
           FLOATINGPOINT_PLUS,
+          FLOATINGPOINT_SUB,
           FLOATINGPOINT_MULT,
           FLOATINGPOINT_DIV,
       };