From e65308fa102d7121a981c9e6bc5b1414b28f9b28 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Mon, 5 Oct 2020 15:35:23 -0700
Subject: [PATCH] SyGuS: Add fp.sub to default FP grammar. (#5206)

---
 src/theory/quantifiers/sygus/sygus_grammar_cons.cpp | 1 +
 1 file changed, 1 insertion(+)

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,
       };
-- 
2.30.2