From 02a7dc0ba7f00b02c2639a884d1f3983b2004a3e Mon Sep 17 00:00:00 2001 From: Andres Noetzli Date: Fri, 22 May 2020 15:33:04 -0700 Subject: [PATCH] [SMT-COMP] Use tear-down-incremental for arithmetic (#4518) This commit changes the run-script for the incremental track to use `--tear-down-incremental=1` for all logics that involve arithmetic. The main motivation for this change is avoid issues that we have with the lemmas generated for `mod`/`div` during `ppRewrite` that cause model-soundness issues. --- .../run-script-smtcomp-current-incremental | 19 +++++-------------- 1 file 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 ;; *) -- 2.30.2