From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 5 Oct 2020 22:35:23 +0000 (-0700)
Subject: SyGuS: Add fp.sub to default FP grammar. (#5206)
X-Git-Tag: cvc5-1.0.0~2754
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e65308fa102d7121a981c9e6bc5b1414b28f9b28;p=cvc5.git

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 ba9962bd9..e5cc5460d 100644
--- 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,
       };