diff options
Diffstat (limited to 'test/regress')
| -rw-r--r-- | test/regress/regress0/arith/bug569.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/datatypes/empty_tuprec.cvc | 2 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/Makefile | 8 | ||||
| -rw-r--r-- | test/regress/regress0/fmf/PUZ001+1.smt2 | 2 | ||||
| -rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 9 | ||||
| -rwxr-xr-x | test/regress/run_regression | 21 |
6 files changed, 36 insertions, 8 deletions
diff --git a/test/regress/regress0/arith/bug569.smt2 b/test/regress/regress0/arith/bug569.smt2 index acb6ffcdf..e1ca49ac5 100644 --- a/test/regress/regress0/arith/bug569.smt2 +++ b/test/regress/regress0/arith/bug569.smt2 @@ -1,3 +1,5 @@ +; COMMAND-LINE: --no-check-unsat-cores +; EXPECT: unsat (set-logic QF_AUFLIRA) (set-info :smt-lib-version 2.0) (set-info :category "crafted") diff --git a/test/regress/regress0/datatypes/empty_tuprec.cvc b/test/regress/regress0/datatypes/empty_tuprec.cvc index 5fe17b412..4f6320028 100644 --- a/test/regress/regress0/datatypes/empty_tuprec.cvc +++ b/test/regress/regress0/datatypes/empty_tuprec.cvc @@ -1,4 +1,4 @@ -% COMMAND-LINE: --no-check-proofs +% COMMAND-LINE: --no-check-proofs --no-check-unsat-cores % OPTION "incremental"; diff --git a/test/regress/regress0/fmf/Makefile b/test/regress/regress0/fmf/Makefile new file mode 100644 index 000000000..1e68a1e9e --- /dev/null +++ b/test/regress/regress0/fmf/Makefile @@ -0,0 +1,8 @@ +topdir = ../../../.. +srcdir = test/regress/regress0/fmf + +include $(topdir)/Makefile.subdir + +# synonyms for "check" +.PHONY: test +test: check diff --git a/test/regress/regress0/fmf/PUZ001+1.smt2 b/test/regress/regress0/fmf/PUZ001+1.smt2 index f0e53fc98..f3db78491 100644 --- a/test/regress/regress0/fmf/PUZ001+1.smt2 +++ b/test/regress/regress0/fmf/PUZ001+1.smt2 @@ -1,4 +1,4 @@ -; COMMAND-LINE: --finite-model-find --no-check-proofs +; COMMAND-LINE: --finite-model-find --no-check-proofs --no-check-unsat-core ; EXPECT: unsat ;%------------------------------------------------------------------------------ ;% File : PUZ001+1 : TPTP v5.4.0. Released v2.0.0. diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index ef65ead1f..53ebf0a78 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -18,9 +18,7 @@ MAKEFLAGS = -k # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" -TESTS = hd-01-d1-prog.sy \ - icfp_28_10.sy \ - commutative.sy \ +TESTS = commutative.sy \ constant.sy \ multi-fun-polynomial2.sy \ unbdd_inv_gen_winf1.sy \ @@ -35,6 +33,11 @@ EXTRA_DIST = $(TESTS) \ max.smt2 \ sygus-uf.sl +# Failing dues to parser changes. Need to be fixed. +EXTRA_DIST += \ + hd-01-d1-prog.sy \ + icfp_28_10.sy + #if CVC4_BUILD_PROFILE_COMPETITION #else #TESTS += \ diff --git a/test/regress/run_regression b/test/regress/run_regression index 7b215dc2a..b6fb735fe 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -230,16 +230,28 @@ if grep '^sat$' "$expoutfile" &>/dev/null || grep '^invalid$' "$expoutfile" &>/d fi fi check_proofs=false +check_unsat_cores=false if [ "$proof" = yes ]; then # proofs not currently supported in incremental mode, turn it off if grep '^unsat$' "$expoutfile" &>/dev/null || grep '^valid$' "$expoutfile" &>/dev/null &>/dev/null; then if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-proofs' &>/dev/null && ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-proofs' &>/dev/null && ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental' &>/dev/null && - ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null; then + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--unconstrained-simp' &>/dev/null && + ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null && + ! expr "$benchmark" : '.*\.sy$' &>/dev/null; then # later on, we'll run another test with --check-proofs on check_proofs=true fi + if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-unsat-cores' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-unsat-cores' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--incremental' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--unconstrained-simp' &>/dev/null && + ! expr " $CVC4_REGRESSION_ARGS $command_line" : '.* -[a-zA-Z]*i' &>/dev/null && + ! expr "$benchmark" : '.*\.sy$' &>/dev/null; then + # later on, we'll run another test with --check-unsat-cores on + check_unsat_cores=true + fi fi fi if [ -z "$expected_error" ]; then @@ -315,7 +327,7 @@ if [ "$exit_status" != "$expected_exit_status" ]; then exitcode=1 fi -if $check_models || $check_proofs; then +if $check_models || $check_proofs || $check_unsat_cores; then check_cmdline= if $check_models; then check_cmdline="$check_cmdline --check-models" @@ -323,7 +335,10 @@ if $check_models || $check_proofs; then if $check_proofs; then check_cmdline="$check_cmdline --check-proofs" fi - # at least one sat/invalid response: run an extra model/proof-checking pass + if $check_unsat_cores; then + check_cmdline="$check_cmdline --check-unsat-cores" + fi + # run an extra model/proof/core-checking pass if ! CVC4_REGRESSION_ARGS="$CVC4_REGRESSION_ARGS$check_cmdline" "$0" $wrapper "$cvc4" "$benchmark_orig"; then exitcode=1 fi |