Enable SymFPU assertions in production (#3036)

This commit enables SymFPU assertions in production. The reason for this
is that there are some known problems with certain bit-widths, so we
prefer to be conservative. The commit also updates the run scripts for SMT-COMP 2019 to use `--fp-exp` since we have those additional checks in place now.

diff --git a/contrib/run-script-smtcomp2019 b/contrib/run-script-smtcomp2019
index a87cefb965be61c5f2609f449c848be3e8a27fd8..15bae8d0d405af257db06e89b65b99f2550f6648 100755 (executable)
--- 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 78ec6ba2204822e51901c574728dbe26eb388336..942f489e628a6ba4bfc24bccb023086ae358124a 100755 (executable)
--- 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 a69cf8c96ecfdaf349a275c7fccf5271acb24e65..fbdce8cd58ebb5b67dbd9aeab00ca300e95bd74f 100644 (file)
--- 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 4aed27c30810fd4ca736d39833711400036f54e2..f7e73ca4b0d41c2d2ccca416532e413d5f002166 100644 (file)
--- 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;
 }
 }