summaryrefslogtreecommitdiff
path: root/contrib/competitions/smt-comp/run-script-smtcomp-current
diff options
context:
space:
mode:
Diffstat (limited to 'contrib/competitions/smt-comp/run-script-smtcomp-current')
-rwxr-xr-xcontrib/competitions/smt-comp/run-script-smtcomp-current8
1 files changed, 4 insertions, 4 deletions
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
;;
*)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback