From 8236d7f9bff3aef4f7b37a15d509b8a11551401f Mon Sep 17 00:00:00 2001
From: Aina Niemetz <aina.niemetz@gmail.com>
Date: Fri, 1 May 2020 21:18:55 -0700
Subject: [PATCH] SMT-COMP 2020: Enable --fp-exp for new FP logics. (#4432)

---
 contrib/competitions/smt-comp/run-script-smtcomp-current  | 8 ++++----
 .../smt-comp/run-script-smtcomp-current-incremental       | 6 +++---
 .../smt-comp/run-script-smtcomp-current-unsat-cores       | 6 +++---
 3 files changed, 10 insertions(+), 10 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
   ;;
 *)
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
   ;;
 *)
-- 
2.30.2