From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 4 Feb 2020 16:21:24 +0000 (-0800)
Subject: --fp-exp: Better warning message. (#3709)
X-Git-Tag: cvc5-1.0.0~3682
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=78c7a2c52f646229f4e657e316e5ffa12c082dc3;p=cvc5.git

--fp-exp: Better warning message. (#3709)
---

diff --git a/src/theory/fp/theory_fp.cpp b/src/theory/fp/theory_fp.cpp
index 6a4dc542e..788545b3c 100644
--- a/src/theory/fp/theory_fp.cpp
+++ b/src/theory/fp/theory_fp.cpp
@@ -902,7 +902,8 @@ void TheoryFp::preRegisterTerm(TNode node)
            << sig_sz
            << " is not supported, only Float32 (8/24) or Float64 (11/53) types "
               "are supported in default mode. Try the experimental solver via "
-              "--fp-exp";
+              "--fp-exp. Note: There are known issues with the experimental "
+              "solver, use at your own risk.";
         throw LogicException(ss.str());
       }
     }