projects / cvc5.git / commit
? search:
summary | shortlog | log | commit | commitdiff | tree
(parent: a211c34) | patch
Enable SymFPU assertions in production (#3036)
authorAndres Noetzli <noetzli@stanford.edu>
Mon, 3 Jun 2019 03:01:48 +0000 (20:01 -0700)
committerGitHub <noreply@github.com>
Mon, 3 Jun 2019 03:01:48 +0000 (20:01 -0700)
commit9ccf3c01a736a9f6d5c6889b51c4589221044c97
treeb2c1b74e7403d38573cb94f6398e3fc747d759c0tree
parenta211c34d77c432007c3e1ed3c82baaea315a7632commit | 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.
contrib/run-script-smtcomp2019 diff | blob | history
contrib/run-script-smtcomp2019-unsat-cores diff | blob | history
src/theory/fp/fp_converter.cpp diff | blob | history
src/util/floatingpoint.cpp diff | blob | history