From fd4b373b9a66a590e0d9618c744312e1050472a0 Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 10 Sep 2021 10:19:32 -0700
Subject: [PATCH] FP: Do not send trivial lemmas. (#7167)

Fixes #7002.
---
 src/theory/fp/theory_fp.cpp             | 9 +++++++--
 src/theory/fp/theory_fp.h               | 3 +++
 test/regress/CMakeLists.txt             | 1 +
 test/regress/regress0/fp/issue7002.smt2 | 5 +++++
 4 files changed, 16 insertions(+), 2 deletions(-)
 create mode 100644 test/regress/regress0/fp/issue7002.smt2

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index ad7c1a656..075a6633f 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -72,7 +72,8 @@ TheoryFp::TheoryFp(Env& env, OutputChannel& out, Valuation valuation)
       d_rewriter(userContext()),
       d_state(env, valuation),
       d_im(env, *this, d_state, d_pnm, "theory::fp::", false),
-      d_wbFactsCache(userContext())
+      d_wbFactsCache(userContext()),
+      d_true(d_env.getNodeManager()->mkConst(true))
 {
   // indicate we are using the default theory state and inference manager
   d_theoryState = &d_state;
@@ -701,7 +702,11 @@ void TheoryFp::handleLemma(Node node, InferenceId id)
   Trace("fp") << "TheoryFp::handleLemma(): asserting " << node << std::endl;
   // will be preprocessed when sent, which is important because it contains
   // embedded ITEs
-  d_im.lemma(node, id);
+  if (rewrite(node) != d_true)
+  {
+    /* We only send non-trivial lemmas. */
+    d_im.lemma(node, id);
+  }
 }
 
 bool TheoryFp::propagateLit(TNode node)
diff --git a/src/theory/fp/theory_fp.h b/src/theory/fp/theory_fp.h
index 1e1041980..663be2f81 100644
--- a/src/theory/fp/theory_fp.h
+++ b/src/theory/fp/theory_fp.h
@@ -157,6 +157,9 @@ class TheoryFp : public Theory
   TheoryInferenceManager d_im;
   /** Cache of word-blasted facts. */
   context::CDHashSet<Node> d_wbFactsCache;
+
+  /** True constant. */
+  Node d_true;
 };
 
 }  // namespace fp
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 852734772..be95286cc 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -605,6 +605,7 @@ set(regress_0_tests
   regress0/fp/issue5511.smt2
   regress0/fp/issue5734.smt2
   regress0/fp/issue6164.smt2
+  regress0/fp/issue7002.smt2
   regress0/fp/rti_3_5_bug.smt2
   regress0/fp/simple.smt2
   regress0/fp/word-blast.smt2
diff --git a/test/regress/regress0/fp/issue7002.smt2 b/test/regress/regress0/fp/issue7002.smt2
new file mode 100644
index 000000000..f589b69d6
--- /dev/null
+++ b/test/regress/regress0/fp/issue7002.smt2
@@ -0,0 +1,5 @@
+; COMMAND-LINE: -q
+; EXPECT: sat
+(set-logic ALL)
+(assert (= 0.0 (fp.to_real (_ NaN 8 24))))
+(check-sat)
-- 
2.30.2