diff options
| -rw-r--r-- | src/theory/fp/theory_fp.cpp | 9 | ||||
| -rw-r--r-- | src/theory/fp/theory_fp.h | 3 | ||||
| -rw-r--r-- | test/regress/CMakeLists.txt | 1 | ||||
| -rw-r--r-- | test/regress/regress0/fp/issue7002.smt2 | 5 |
4 files changed, 16 insertions, 2 deletions
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) |