From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Wed, 23 Sep 2020 03:46:17 +0000 (-0700)
Subject: FP: Use Assert instead of AlwaysAssert in traits::(pre|post)condition. (#5121)
X-Git-Tag: cvc5-1.0.0~2818
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=e7c50fad0015527e854b3ceee692907e8242a05b;p=cvc5.git

FP: Use Assert instead of AlwaysAssert in traits::(pre|post)condition. (#5121)

For the same reason as in #5119.
---

diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index 3ddf9f595..47a4af43e 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -157,17 +157,17 @@ symbolicRoundingMode traits::RTZ(void) { return symbolicRoundingMode(0x10); };
 
 void traits::precondition(const bool b)
 {
-  AlwaysAssert(b);
+  Assert(b);
   return;
 }
 void traits::postcondition(const bool b)
 {
-  AlwaysAssert(b);
+  Assert(b);
   return;
 }
 void traits::invariant(const bool b)
 {
-  AlwaysAssert(b);
+  Assert(b);
   return;
 }
 
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index bac56af69..631f8241c 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -442,17 +442,17 @@ rm traits::RTZ(void) { return ::CVC4::roundTowardZero; };
 
 void traits::precondition(const prop &p)
 {
-  AlwaysAssert(p);
+  Assert(p);
   return;
 }
 void traits::postcondition(const prop &p)
 {
-  AlwaysAssert(p);
+  Assert(p);
   return;
 }
 void traits::invariant(const prop &p)
 {
-  AlwaysAssert(p);
+  Assert(p);
   return;
 }
 }