4 files changed, 14 insertions, 14 deletions
diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019
index a87cefb96..15bae8d0d 100755
--- a/contrib/run-script-smtcomp2019
+++ b/contrib/run-script-smtcomp2019
@@ -85,7 +85,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUF
   finishwith --full-saturate-quant
   ;;
 ABVFP|BVFP|FP)
-  finishwith --full-saturate-quant
+  finishwith --full-saturate-quant --fp-exp
   ;;
 UFBV)
   # most problems in UFBV are essentially BV
@@ -142,13 +142,13 @@ QF_S|QF_SLIA)
   finishwith --strings-exp --rewrite-divk --lang=smt2.6.1
   ;;
 QF_ABVFP)
-  finishwith
+  finishwith --fp-exp
   ;;
 QF_BVFP)
-  finishwith
+  finishwith --fp-exp
   ;;
 QF_FP)
-  finishwith
+  finishwith --fp-exp
   ;;
 *)
   # just run the default
diff --git a/contrib/run-script-smtcomp2019-unsat-cores b/contrib/run-script-smtcomp2019-unsat-cores
index 78ec6ba22..942f489e6 100755
--- a/contrib/run-script-smtcomp2019-unsat-cores
+++ b/contrib/run-script-smtcomp2019-unsat-cores
@@ -27,7 +27,7 @@ QF_NRA)
   ;;
 # all logics with UF + quantifiers should either fall under this or special cases below
 ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBVDTLIA|AUFNIA|ABVFP|BVFP|FP)
-  finishwith --full-saturate-quant
+  finishwith --full-saturate-quant --fp-exp
   ;;
 UFBV)
   finishwith --finite-model-find
@@ -69,13 +69,13 @@ QF_S|QF_SLIA)
   finishwith --strings-exp --rewrite-divk --lang=smt2.6.1
   ;;
 QF_ABVFP)
-  finishwith
+  finishwith --fp-exp
   ;;
 QF_BVFP)
-  finishwith
+  finishwith --fp-exp
   ;;
 QF_FP)
-  finishwith
+  finishwith --fp-exp
   ;;
 *)
   # just run the default
diff --git a/src/theory/fp/fp_converter.cpp b/src/theory/fp/fp_converter.cpp
index a69cf8c96..fbdce8cd5 100644
--- a/src/theory/fp/fp_converter.cpp
+++ b/src/theory/fp/fp_converter.cpp
@@ -157,17 +157,17 @@ symbolicRoundingMode traits::RTN(void) { return symbolicRoundingMode(0x08); };
 symbolicRoundingMode traits::RTZ(void) { return symbolicRoundingMode(0x10); };
 void traits::precondition(const bool b)
 {
-  Assert(b);
+  AlwaysAssert(b);
   return;
 }
 void traits::postcondition(const bool b)
 {
-  Assert(b);
+  AlwaysAssert(b);
   return;
 }
 void traits::invariant(const bool b)
 {
-  Assert(b);
+  AlwaysAssert(b);
   return;
 }
 
diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp
index 4aed27c30..f7e73ca4b 100644
--- a/src/util/floatingpoint.cpp
+++ b/src/util/floatingpoint.cpp
@@ -441,17 +441,17 @@ rm traits::RTZ(void) { return ::CVC4::roundTowardZero; };
 
 void traits::precondition(const prop &p)
 {
-  Assert(p);
+  AlwaysAssert(p);
   return;
 }
 void traits::postcondition(const prop &p)
 {
-  Assert(p);
+  AlwaysAssert(p);
   return;
 }
 void traits::invariant(const prop &p)
 {
-  Assert(p);
+  AlwaysAssert(p);
   return;
 }
 }