From: Aina Niemetz Date: Sat, 2 May 2020 04:18:55 +0000 (-0700) Subject: SMT-COMP 2020: Enable --fp-exp for new FP logics. (#4432) X-Git-Tag: cvc5-1.0.0~3324 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=8236d7f9bff3aef4f7b37a15d509b8a11551401f;p=cvc5.git SMT-COMP 2020: Enable --fp-exp for new FP logics. (#4432) --- diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index d4a257395..506eb56b7 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -85,7 +85,7 @@ ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUF trywith 240 --finite-model-find --decision=internal finishwith --full-saturate-quant ;; -ABVFP|BVFP|FP) +ABVFP|BVFP|FP|UFFPDTLIRA|UFFPDTNIRA) finishwith --full-saturate-quant --fp-exp ;; UFBV) @@ -145,13 +145,13 @@ QF_S|QF_SLIA) trywith 300 --strings-exp --rewrite-divk --strings-fmf finishwith --strings-exp --rewrite-divk ;; -QF_ABVFP) +QF_ABVFP|QF_ABVFPLRA) finishwith --fp-exp ;; -QF_BVFP) +QF_BVFP|QF_BVFPLRA) finishwith --fp-exp ;; -QF_FP) +QF_FP|QF_FPLRA) finishwith --fp-exp ;; *) diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental index d55c54b42..ae0b2d7a4 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental @@ -67,13 +67,13 @@ ABVFP) BVFP) runcvc4 --incremental ;; -QF_ABVFP) +QF_ABVFP|QF_ABFPLRA) runcvc4 --incremental ;; -QF_BVFP) +QF_BVFP|QF_BVFPLRA) runcvc4 --incremental ;; -QF_FP) +QF_FP|QF_FPLRA) runcvc4 --incremental ;; *) diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores index 33f41263d..b5449470f 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores @@ -68,13 +68,13 @@ QF_ALIA) QF_S|QF_SLIA) finishwith --strings-exp --rewrite-divk ;; -QF_ABVFP) +QF_ABVFP|QF_ABVFPLRA) finishwith --fp-exp ;; -QF_BVFP) +QF_BVFP|QF_BVFPLRA) finishwith --fp-exp ;; -QF_FP) +QF_FP|QF_FPLRA) finishwith --fp-exp ;; *)