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 \
113 # Regression tests for TPTP inputs
116 # Regression tests derived from bug reports
152 bug512.minimized.smt2 \
157 bug521.minimized.smt2 \
172 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
174 # bug512 -- taking too long, --time-per not working perhaps? in any case,
175 # we have a minimized version still getting tested
179 EXTRA_DIST = $(TESTS) \
180 simplification_bug4.smt2.expect \
183 if CVC4_BUILD_PROFILE_COMPETITION
191 # and make sure to distribute it
192 EXTRA_DIST += $(DISABLED_TESTS) \
194 arrayinuf_error.smt2 \
198 # synonyms for "check" in this directory
199 .PHONY: regress regress0 test
200 regress regress0 test: check
202 # do nothing in this subdir
203 .PHONY: regress1 regress2 regress3
204 regress1 regress2 regress3: