From e7c50fad0015527e854b3ceee692907e8242a05b Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Tue, 22 Sep 2020 20:46:17 -0700
Subject: [PATCH] FP: Use Assert instead of AlwaysAssert in
 traits::(pre|post)condition. (#5121)

For the same reason as in #5119.
---
 src/theory/fp/fp_converter.cpp | 6 +++---
 src/util/floatingpoint.cpp     | 6 +++---
 2 files changed, 6 insertions(+), 6 deletions(-)

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;
 }
 }
-- 
2.30.2