From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 2 Dec 2020 23:34:13 +0000 (-0800)
Subject: Fix RoundingMode mapping in API. (#5578)
X-Git-Tag: cvc5-1.0.0~2515
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=7883e133df0c0104d0fb4d6f2834a3e1af0f9786;p=cvc5.git

Fix RoundingMode mapping in API. (#5578)

Fixes #5524.
---

diff --git a/src/api/cvc4cpp.cpp b/src/api/cvc4cpp.cpp
index 36edfdb46..80fb8a5fb 100644
--- a/src/api/cvc4cpp.cpp
+++ b/src/api/cvc4cpp.cpp
@@ -3075,7 +3075,7 @@ const static std::
             {ROUND_NEAREST_TIES_TO_EVEN,
              CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_EVEN},
             {ROUND_TOWARD_POSITIVE, CVC4::RoundingMode::ROUND_TOWARD_POSITIVE},
-            {ROUND_TOWARD_NEGATIVE, CVC4::RoundingMode::ROUND_TOWARD_POSITIVE},
+            {ROUND_TOWARD_NEGATIVE, CVC4::RoundingMode::ROUND_TOWARD_NEGATIVE},
             {ROUND_TOWARD_ZERO, CVC4::RoundingMode::ROUND_TOWARD_ZERO},
             {ROUND_NEAREST_TIES_TO_AWAY,
              CVC4::RoundingMode::ROUND_NEAREST_TIES_TO_AWAY},
diff --git a/test/regress/CMakeLists.txt b/test/regress/CMakeLists.txt
index 1826b3156..5ab1cd6c2 100644
--- a/test/regress/CMakeLists.txt
+++ b/test/regress/CMakeLists.txt
@@ -531,6 +531,7 @@ set(regress_0_tests
   regress0/fp/issue3536.smt2
   regress0/fp/issue3619.smt2
   regress0/fp/issue4277-assign-func.smt2
+  regress0/fp/issue-5524.smt2
   regress0/fp/rti_3_5_bug.smt2
   regress0/fp/rti_3_5_bug_report.smt2
   regress0/fp/simple.smt2
diff --git a/test/regress/regress0/fp/issue-5524.smt2 b/test/regress/regress0/fp/issue-5524.smt2
new file mode 100644
index 000000000..8c361163c
--- /dev/null
+++ b/test/regress/regress0/fp/issue-5524.smt2
@@ -0,0 +1,6 @@
+; REQUIRES: symfpu
+; EXPECT: unsat
+(set-logic QF_FP)
+(declare-fun fpv5 () Float32)
+(assert (fp.eq (fp.mul RTP fpv5 fpv5) ((_ to_fp 8 24) RTN 0.04)))
+(check-sat)