From 9ccf3c01a736a9f6d5c6889b51c4589221044c97 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Sun, 2 Jun 2019 20:01:48 -0700 Subject: [PATCH] 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. --- contrib/run-script-smtcomp2019 | 8 ++++---- contrib/run-script-smtcomp2019-unsat-cores | 8 ++++---- src/theory/fp/fp_converter.cpp | 6 +++--- src/util/floatingpoint.cpp | 6 +++--- 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; } } -- 2.30.2