From 264ad1e305b2ae724bbd20b2a33872ba9010dba9 Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Wed, 6 Jul 2022 13:12:33 -0700 Subject: [PATCH] Update SMT-COMP scripts (#8930) --- contrib/competitions/smt-comp/run-script-smtcomp-current | 2 +- .../smt-comp/run-script-smtcomp-current-unsat-cores | 2 +- 2 files changed, 2 insertions(+), 2 deletions(-) diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current b/contrib/competitions/smt-comp/run-script-smtcomp-current index 2426693bf..a138aa336 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current @@ -75,7 +75,7 @@ QF_NRA) finishwith --decision=internal --nl-ext=none ;; # all logics with UF + quantifiers should either fall under this or special cases below -ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBVLIA|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|AUFDTLIA|AUFBV|AUFBVDTLIA|AUFBVFP|AUFNIA|UFFPDTLIRA|UFFPDTNIRA) +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBVLIA|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|UFDTLIRA|AUFDTLIA|AUFDTLIRA|AUFBV|AUFBVDTLIA|AUFBVFP|AUFNIA|UFFPDTLIRA|UFFPDTNIRA) # initial runs 1 min trywith 30 --simplification=none --enum-inst trywith 30 --no-e-matching --enum-inst 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 0ecb6b62c..c2a977075 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-unsat-cores @@ -23,7 +23,7 @@ QF_NIA) finishwith --nl-ext-tplanes ;; # 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) +ALIA|AUFLIA|AUFLIRA|AUFNIRA|UF|UFBVLIA|UFIDL|UFLIA|UFLRA|UFNIA|UFDT|UFDTLIA|UFDTLIRA|AUFDTLIA|AUFDTLIRA|AUFBV|AUFBVDTLIA|AUFBVFP|AUFNIA|UFFPDTLIRA|UFFPDTNIRA|ABVFP|BVFP|FP) finishwith --full-saturate-quant --fp-exp ;; UFBV) -- 2.30.2