1 SUBDIRS = . arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets parser
2 DIST_SUBDIRS = $(SUBDIRS) #. arith precedence uf uflra uflia bv arrays aufbv auflia datatypes quantifiers rewriterules lemmas push-pop preprocess tptp unconstrained decision fmf strings sets
4 # don't override a BINARY imported from a personal.mk
6 @mk_empty@BINARY = cvc4
9 LOG_COMPILER = @srcdir@/../run_regression
10 AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT)
13 # old-style (pre-automake 1.12) test harness
16 $(AM_LOG_FLAGS) $(LOG_FLAGS)
21 # These are run for all build profiles.
22 # If a test shouldn't be run in e.g. competition mode,
23 # put it below in "TESTS +="
25 # Regression tests for SMT inputs
34 ite_real_int_type.smt \
38 simplification_bug.smt \
39 simplification_bug2.smt \
47 # Regression tests for SMT2 inputs
49 arrayinuf_declare.smt2 \
50 boolean-terms-kernel1.smt2 \
51 boolean-terms-kernel2.smt2 \
52 boolean-terms-bug-array.smt2 \
53 chained-equality.smt2 \
61 simplification_bug4.smt2 \
63 get-value-incremental.smt2 \
64 hung13sdk_output1.smt2 \
65 hung10_itesdk_output2.smt2 \
66 hung10_itesdk_output1.smt2 \
67 hung13sdk_output2.smt2
69 # Regression tests for PL inputs
108 simplification_bug3.cvc \
112 # Regression tests for TPTP inputs
115 # Regression tests derived from bug reports
151 bug512.minimized.smt2 \
156 bug521.minimized.smt2 \
169 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
171 # bug512 -- taking too long, --time-per not working perhaps? in any case,
172 # we have a minimized version still getting tested
176 EXTRA_DIST = $(TESTS) \
177 simplification_bug4.smt2.expect \
180 if CVC4_BUILD_PROFILE_COMPETITION
188 # and make sure to distribute it
189 EXTRA_DIST += $(DISABLED_TESTS) \
191 arrayinuf_error.smt2 \
195 # synonyms for "check" in this directory
196 .PHONY: regress regress0 test
197 regress regress0 test: check
199 # do nothing in this subdir
200 .PHONY: regress1 regress2 regress3
201 regress1 regress2 regress3: