diff options
Diffstat (limited to 'test')
35 files changed, 85 insertions, 117 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am index 5c591d39c..d7663e298 100644 --- a/test/regress/regress0/Makefile.am +++ b/test/regress/regress0/Makefile.am @@ -7,12 +7,12 @@ DIST_SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatype end@mk_if@ LOG_COMPILER = @srcdir@/../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/arith/Makefile.am b/test/regress/regress0/arith/Makefile.am index 6897ee3c4..e7810c7c4 100644 --- a/test/regress/regress0/arith/Makefile.am +++ b/test/regress/regress0/arith/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . integers end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/arith/integers/Makefile.am b/test/regress/regress0/arith/integers/Makefile.am index 3511c6b30..3b6a86bc0 100644 --- a/test/regress/regress0/arith/integers/Makefile.am +++ b/test/regress/regress0/arith/integers/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/arrays/Makefile.am b/test/regress/regress0/arrays/Makefile.am index 33f05ab40..62877ddf3 100644 --- a/test/regress/regress0/arrays/Makefile.am +++ b/test/regress/regress0/arrays/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/aufbv/Makefile.am b/test/regress/regress0/aufbv/Makefile.am index e151a4846..e45358a8a 100644 --- a/test/regress/regress0/aufbv/Makefile.am +++ b/test/regress/regress0/aufbv/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/auflia/Makefile.am b/test/regress/regress0/auflia/Makefile.am index ca1fc25d3..31d9c0797 100644 --- a/test/regress/regress0/auflia/Makefile.am +++ b/test/regress/regress0/auflia/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/boolean.cvc b/test/regress/regress0/boolean.cvc index cba092e9e..eb0e7ab52 100644 --- a/test/regress/regress0/boolean.cvc +++ b/test/regress/regress0/boolean.cvc @@ -804,4 +804,3 @@ a288 : BOOLEAN = ELSE FALSE ENDIF; QUERY a288; -% PROOF diff --git a/test/regress/regress0/bv/Makefile.am b/test/regress/regress0/bv/Makefile.am index f0bfb2842..5d2a54b11 100644 --- a/test/regress/regress0/bv/Makefile.am +++ b/test/regress/regress0/bv/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . core end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/bv/core/Makefile.am b/test/regress/regress0/bv/core/Makefile.am index 888e9d8dc..7c411121a 100644 --- a/test/regress/regress0/bv/core/Makefile.am +++ b/test/regress/regress0/bv/core/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/datatypes/Makefile.am b/test/regress/regress0/datatypes/Makefile.am index 67b97add3..84adb4f84 100644 --- a/test/regress/regress0/datatypes/Makefile.am +++ b/test/regress/regress0/datatypes/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/datatypes/empty_tuprec.cvc b/test/regress/regress0/datatypes/empty_tuprec.cvc index 415da3c18..5fe17b412 100644 --- a/test/regress/regress0/datatypes/empty_tuprec.cvc +++ b/test/regress/regress0/datatypes/empty_tuprec.cvc @@ -1,3 +1,5 @@ +% COMMAND-LINE: --no-check-proofs +% OPTION "incremental"; a1, a2 : []; % empty tuples (a unit type) diff --git a/test/regress/regress0/decision/Makefile.am b/test/regress/regress0/decision/Makefile.am index 0f8ef8e8e..366204191 100644 --- a/test/regress/regress0/decision/Makefile.am +++ b/test/regress/regress0/decision/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/fmf/Makefile.am b/test/regress/regress0/fmf/Makefile.am index bfbc851ef..2633949c8 100644 --- a/test/regress/regress0/fmf/Makefile.am +++ b/test/regress/regress0/fmf/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/fmf/PUZ001+1.smt2 b/test/regress/regress0/fmf/PUZ001+1.smt2 index bf156367e..f0e53fc98 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 +; COMMAND-LINE: --finite-model-find --no-check-proofs ; EXPECT: unsat ;%------------------------------------------------------------------------------ ;% File : PUZ001+1 : TPTP v5.4.0. Released v2.0.0. diff --git a/test/regress/regress0/hole6.cvc b/test/regress/regress0/hole6.cvc index 5cc4de9be..dfa9b72d5 100644 --- a/test/regress/regress0/hole6.cvc +++ b/test/regress/regress0/hole6.cvc @@ -177,4 +177,3 @@ ASSERT x_42 OR x_41 OR x_40 OR x_39 OR x_38 OR x_37; QUERY FALSE; -% PROOF diff --git a/test/regress/regress0/lemmas/Makefile.am b/test/regress/regress0/lemmas/Makefile.am index 260b3600d..9ede6d4c0 100644 --- a/test/regress/regress0/lemmas/Makefile.am +++ b/test/regress/regress0/lemmas/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/precedence/Makefile.am b/test/regress/regress0/precedence/Makefile.am index 141510ea2..1d980997d 100644 --- a/test/regress/regress0/precedence/Makefile.am +++ b/test/regress/regress0/precedence/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/preprocess/Makefile.am b/test/regress/regress0/preprocess/Makefile.am index 73d13e78d..d83df4192 100644 --- a/test/regress/regress0/preprocess/Makefile.am +++ b/test/regress/regress0/preprocess/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/push-pop/Makefile.am b/test/regress/regress0/push-pop/Makefile.am index 0a1094238..29ad34255 100644 --- a/test/regress/regress0/push-pop/Makefile.am +++ b/test/regress/regress0/push-pop/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = boolean arith . end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/push-pop/arith/Makefile.am b/test/regress/regress0/push-pop/arith/Makefile.am index 6fd183ec3..7838e202d 100644 --- a/test/regress/regress0/push-pop/arith/Makefile.am +++ b/test/regress/regress0/push-pop/arith/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/push-pop/boolean/Makefile.am b/test/regress/regress0/push-pop/boolean/Makefile.am index 0757ebfc2..995312cee 100644 --- a/test/regress/regress0/push-pop/boolean/Makefile.am +++ b/test/regress/regress0/push-pop/boolean/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/quantifiers/Makefile.am b/test/regress/regress0/quantifiers/Makefile.am index 0b74d83b7..d0a93a142 100644 --- a/test/regress/regress0/quantifiers/Makefile.am +++ b/test/regress/regress0/quantifiers/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/rewriterules/Makefile.am b/test/regress/regress0/rewriterules/Makefile.am index d2e748fbf..32f8a72ba 100644 --- a/test/regress/regress0/rewriterules/Makefile.am +++ b/test/regress/regress0/rewriterules/Makefile.am @@ -7,12 +7,12 @@ export CVC4_REGRESSION_ARGS end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/strings/Makefile.am b/test/regress/regress0/strings/Makefile.am index e24cbc565..a5c6ae2f4 100644 --- a/test/regress/regress0/strings/Makefile.am +++ b/test/regress/regress0/strings/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/tptp/Makefile.am b/test/regress/regress0/tptp/Makefile.am index e227e0bba..f8f106362 100644 --- a/test/regress/regress0/tptp/Makefile.am +++ b/test/regress/regress0/tptp/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/uf/Makefile.am b/test/regress/regress0/uf/Makefile.am index 19e673fea..98194413d 100644 --- a/test/regress/regress0/uf/Makefile.am +++ b/test/regress/regress0/uf/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/uflia/Makefile.am b/test/regress/regress0/uflia/Makefile.am index 2ef7be862..2946d886a 100644 --- a/test/regress/regress0/uflia/Makefile.am +++ b/test/regress/regress0/uflia/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/uflra/Makefile.am b/test/regress/regress0/uflra/Makefile.am index 63d362bf9..cd39284b8 100644 --- a/test/regress/regress0/uflra/Makefile.am +++ b/test/regress/regress0/uflra/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/unconstrained/Makefile.am b/test/regress/regress0/unconstrained/Makefile.am index c9a38d7b1..ecf427fb5 100644 --- a/test/regress/regress0/unconstrained/Makefile.am +++ b/test/regress/regress0/unconstrained/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress0/wiki.05.cvc b/test/regress/regress0/wiki.05.cvc index fa9f56f81..0fe647f7b 100644 --- a/test/regress/regress0/wiki.05.cvc +++ b/test/regress/regress0/wiki.05.cvc @@ -2,4 +2,3 @@ a, b, c : BOOLEAN; % EXPECT: valid QUERY a OR (a AND b) <=> a; -% PROOF diff --git a/test/regress/regress1/Makefile.am b/test/regress/regress1/Makefile.am index 674f5c75e..5f292b893 100644 --- a/test/regress/regress1/Makefile.am +++ b/test/regress/regress1/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . arith end@mk_if@ LOG_COMPILER = @srcdir@/../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress1/arith/Makefile.am b/test/regress/regress1/arith/Makefile.am index ca362f479..fff5372c6 100644 --- a/test/regress/regress1/arith/Makefile.am +++ b/test/regress/regress1/arith/Makefile.am @@ -4,12 +4,12 @@ end@mk_if@ LOG_COMPILER = @srcdir@/../../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress2/Makefile.am b/test/regress/regress2/Makefile.am index e4e5d8d29..9deb1f37b 100644 --- a/test/regress/regress2/Makefile.am +++ b/test/regress/regress2/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/regress3/Makefile.am b/test/regress/regress3/Makefile.am index 213157491..3fb798bcc 100644 --- a/test/regress/regress3/Makefile.am +++ b/test/regress/regress3/Makefile.am @@ -6,12 +6,12 @@ SUBDIRS = . end@mk_if@ LOG_COMPILER = @srcdir@/../run_regression -AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @top_builddir@/src/main/$(BINARY)$(EXEEXT) +AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT) if AUTOMAKE_1_11 # old-style (pre-automake 1.12) test harness TESTS_ENVIRONMENT = \ - $(TESTS_ENVIRONMENT) $(LOG_COMPILER) \ + $(LOG_COMPILER) \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif diff --git a/test/regress/run_regression b/test/regress/run_regression index 4d23e796b..ef2bb9a35 100755 --- a/test/regress/run_regression +++ b/test/regress/run_regression @@ -71,10 +71,8 @@ function gettemp { tmpbenchmark= if expr "$benchmark" : '.*\.smt$' &>/dev/null; then - proof_command=PROOFS-NOT-SUPPORTED-IN-SMTLIB-V1 lang=smt1 if test -e "$benchmark.expect"; then - expected_proof=`grep '^% PROOF' "$benchmark.expect" &>/dev/null && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -83,7 +81,6 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then expected_exit_status=0 fi elif grep '^% \(PROOF\|EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then - expected_proof=`grep '^% PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -97,12 +94,10 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then fi benchmark=$tmpbenchmark elif grep '^ *:status *sat' "$benchmark" &>/dev/null; then - expected_proof= expected_output=sat expected_exit_status=0 command_line= elif grep '^ *:status *unsat' "$benchmark" &>/dev/null; then - expected_proof= expected_output=unsat expected_exit_status=0 command_line= @@ -110,10 +105,8 @@ if expr "$benchmark" : '.*\.smt$' &>/dev/null; then error "cannot determine status of \`$benchmark'" fi elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then - proof_command='(get-proof)' lang=smt2 if test -e "$benchmark.expect"; then - expected_proof=`grep '^[%;] PROOF' "$benchmark.expect" &>/dev/null && echo yes` expected_output=`grep '^% EXPECT: ' "$benchmark.expect" | sed 's,^% EXPECT: ,,'` expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark.expect" | sed 's,^% EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^% EXIT: ' "$benchmark.expect" | perl -pe 's,^% EXIT: ,,;s,\r,,'` @@ -122,7 +115,6 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then expected_exit_status=0 fi elif grep '^\(%\|;\) \(EXPECT\|EXPECT-ERROR\|EXIT\|COMMAND-LINE\): ' "$benchmark" "$benchmark" &>/dev/null; then - expected_proof=`grep '^[%;] PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=`grep '^[%;] EXPECT: ' "$benchmark" | sed 's,^[%;] EXPECT: ,,'` expected_error=`grep '^[%;] EXPECT-ERROR: ' "$benchmark" | sed 's,^[%;] EXPECT-ERROR: ,,'` expected_exit_status=`grep -m 1 '^[%;] EXIT: ' "$benchmark" | perl -pe 's,^[%;] EXIT: ,,;s,\r,,'` @@ -136,12 +128,10 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then fi benchmark=$tmpbenchmark elif grep '^ *( *set-info *:status *sat' "$benchmark" &>/dev/null; then - expected_proof= expected_output=sat expected_exit_status=0 command_line= elif grep '^ *( *set-info *:status *unsat' "$benchmark" &>/dev/null; then - expected_proof=`grep '^; PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=unsat expected_exit_status=0 command_line= @@ -149,9 +139,7 @@ elif expr "$benchmark" : '.*\.smt2$' &>/dev/null; then error "cannot determine status of \`$benchmark'" fi elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then - proof_command='DUMP_PROOF;' lang=cvc4 - expected_proof=`grep '^% PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=$(grep '^% EXPECT: ' "$benchmark") expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` if [ -z "$expected_output" -a -z "$expected_error" ]; then @@ -165,10 +153,8 @@ elif expr "$benchmark" : '.*\.cvc$' &>/dev/null; then fi command_line=`grep '^% COMMAND-LINE: ' "$benchmark" | sed 's,^% COMMAND-LINE: ,,'` elif expr "$benchmark" : '.*\.p$' &>/dev/null; then - proof_command=PROOFS-NOT-SUPPORTED-IN-TPTP; lang=tptp command_line=--finite-model-find - expected_proof=`grep '^% PROOF' "$benchmark" &>/dev/null && echo yes` expected_output=$(grep '^% EXPECT: ' "$benchmark") expected_error=`grep '^% EXPECT-ERROR: ' "$benchmark" | sed 's,^% EXPECT-ERROR: ,,'` if [ -z "$expected_output" -a -z "$expected_error" ]; then @@ -213,14 +199,28 @@ if [ -z "$expected_output" ]; then else echo "$expected_output" >"$expoutfile" fi + check_models=false if grep '^sat$' "$expoutfile" &>/dev/null || grep '^invalid$' "$expoutfile" &>/dev/null || grep '^unknown$' "$expoptfile" &>/dev/null; then - if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-models' &>/dev/null && - ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-models' &>/dev/null; then + if ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--check-models\>' &>/dev/null && + ! expr "$CVC4_REGRESSION_ARGS $command_line" : '.*--no-check-models\>' &>/dev/null; then # later on, we'll run another test with --check-models on check_models=true fi fi +check_proofs=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 + # later on, we'll run another test with --check-proofs on + check_proofs=true + fi + fi +fi if [ -z "$expected_error" ]; then # in case expected stderr output is empty, make sure we don't differ # by a newline, which we would if we echo "" >"$experrfile" @@ -275,47 +275,16 @@ if [ "$exit_status" != "$expected_exit_status" ]; then exitcode=1 fi -if [ "$proof" = yes -a "$expected_proof" = yes ]; then - gettemp pfbenchmark cvc4_pfbenchmark.$$.XXXXXXXXXX - # remove exit command to add proof command for smt2 benchmarks - if expr "$benchmark" : '.*\.smt2$' &>/dev/null; then - head -n -0 "$benchmark" > "$pfbenchmark"; - echo "$proof_command" >>"$pfbenchmark"; - echo "(exit)" >> "$pfbenchmark"; - else - cp $benchmark $pfbenchmark - echo "$proof_command" >>"$pfbenchmark"; +if $check_models || $check_proofs; then + check_cmdline= + if $check_models; then + check_cmdline="$check_cmdline --check-models" fi - echo running $wrapper $cvc4full $CVC4_REGRESSION_ARGS $command_line --proof `basename "$pfbenchmark"` [from working dir `dirname "$pfbenchmark"`] - time ( :; \ - ( cd `dirname "$pfbenchmark"`; - $wrapper "$cvc4full" $CVC4_REGRESSION_ARGS $command_line --proof `basename "$pfbenchmark"`; - echo $? >"$exitstatusfile" - ) > "$outfile" 2> "$errfile" ) - - gettemp pfoutfile cvc4_proof.$$.XXXXXXXXXX - - diff --unchanged-group-format='' \ - --old-group-format='' \ - --new-group-format='%>' \ - "$expoutfile" "$outfile" > "$pfoutfile" - if [ ! -s "$pfoutfile" ]; then - echo "$prog: error: proof generation failed with empty output (stderr follows)" - cat "$errfile" - exitcode=1 - else - echo running $LFSC "$pfoutfile" [from working dir `dirname "$pfbenchmark"`] - if ! $LFSC "$pfoutfile" &> "$errfile"; then - echo "$prog: error: proof checker failed (output follows)" - cat "$errfile" - exitcode=1 - fi + if $check_proofs; then + check_cmdline="$check_cmdline --check-proofs" fi -fi - -if $check_models; then - # at least one sat/invalid response: run an extra model-checking pass - if ! CVC4_REGRESSION_ARGS="$CVC4_REGRESSION_ARGS --check-models" "$0" $wrapper "$cvc4" "$benchmark_orig"; then + # at least one sat/invalid response: run an extra model/proof-checking pass + if ! CVC4_REGRESSION_ARGS="$CVC4_REGRESSION_ARGS$check_cmdline" "$0" $wrapper "$cvc4" "$benchmark_orig"; then exitcode=1 fi fi |