diff options
| -rwxr-xr-x | contrib/competitions/smt-comp/run-script-smtcomp-current-incremental | 19 |
1 files changed, 5 insertions, 14 deletions
diff --git a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental index ae0b2d7a4..7861a4c85 100755 --- a/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental +++ b/contrib/competitions/smt-comp/run-script-smtcomp-current-incremental @@ -31,24 +31,15 @@ function runcvc4 { case "$logic" in -ALIA|QF_ALIA|QF_LRA|QF_UFLIA|QF_UFLRA|UFLRA) - runcvc4 --incremental - ;; -ANIA|QF_ANIA|QF_NIA|QF_UFNIA|QF_NRA) +ALIA|ANIA|AUFNIRA|LIA|LRA|QF_ALIA|QF_ANIA|QF_AUFBVLIA|QF_AUFBVNIA|QF_LIA|QF_LRA|QF_NIA|QF_UFBVLIA|QF_UFLIA|QF_UFLRA|QF_UFNIA|UFLRA) runcvc4 --tear-down-incremental=1 ;; -LIA|LRA) - runcvc4 --incremental - ;; QF_AUFLIA) - runcvc4 --no-arrays-eager-index --arrays-eager-lemmas --incremental + runcvc4 --tear-down-incremental=1 --no-arrays-eager-index --arrays-eager-lemmas ;; QF_BV) runcvc4 --incremental --bitblast=eager --bv-sat-solver=cadical ;; -QF_LIA) - runcvc4 --tear-down-incremental=1 - ;; QF_UFBV) runcvc4 --incremental ;; @@ -67,13 +58,13 @@ ABVFP) BVFP) runcvc4 --incremental ;; -QF_ABVFP|QF_ABFPLRA) +QF_ABVFP) runcvc4 --incremental ;; -QF_BVFP|QF_BVFPLRA) +QF_BVFP) runcvc4 --incremental ;; -QF_FP|QF_FPLRA) +QF_FP) runcvc4 --incremental ;; *) |