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 /contrib | |
| 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 'contrib')
| -rwxr-xr-x | contrib/run-script-smtcomp2019 | 8 | ||||
| -rwxr-xr-x | contrib/run-script-smtcomp2019-unsat-cores | 8 |
2 files changed, 8 insertions, 8 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 |