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 3ddf9f5950ff2ab3a08c4c9082e1cecfc607c472..47a4af43e2b32baf7acce82a686af2b88f6cbd4e 100644 (file)
--- 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 bac56af69a99fbd9d05c2e27cafc9847846d909e..631f8241c298f7158ead6054e04838d84f95a9fd 100644 (file)
--- 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;
 }
 }