diff options
author | Andres Noetzli <noetzli@stanford.edu> | 2019-06-02 20:01:48 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2019-06-02 20:01:48 -0700 |
commit | 9ccf3c01a736a9f6d5c6889b51c4589221044c97 (patch) | |
tree | b2c1b74e7403d38573cb94f6398e3fc747d759c0 /src/util | |
parent | a211c34d77c432007c3e1ed3c82baaea315a7632 (diff) |
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.
Diffstat (limited to 'src/util')
-rw-r--r-- | src/util/floatingpoint.cpp | 6 |
1 files changed, 3 insertions, 3 deletions
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; } } |