FP: Do not send trivial lemmas. (#7167)

Fixes #7002.

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index ad7c1a656c5a8d2cb573b2f2af1a040c01a5cc01..075a6633f695f9146b6a2c639b4a96bd2b216745 100644 (file)
--- 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 1e10419801bec3e421b3ca31a36ae099588d36ab..663be2f81068dad149d5a27b4b724e506d51eb8c 100644 (file)
--- 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 852734772d2dc9318f4988ed6468b2f1ff3e1ea6..be95286cc647f3e2947acbb65894635aee760a45 100644 (file)
--- 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 (file)
index 0000000..f589b69
--- /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)