test/regress/regress0/Makefile.am

   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
   3
   4 # don't override a BINARY imported from a personal.mk
   5 @mk_if@eq ($(BINARY),)
   6 @mk_empty@BINARY = cvc4
   7 end@mk_if@
   8
   9 LOG_COMPILER = @srcdir@/../run_regression
  10 AM_LOG_FLAGS = $(RUN_REGRESSION_ARGS) @abs_top_builddir@/src/main/$(BINARY)$(EXEEXT)
  11
  12 if AUTOMAKE_1_11
  13 # old-style (pre-automake 1.12) test harness
  14 TESTS_ENVIRONMENT = \
  15         $(LOG_COMPILER) \
  16         $(AM_LOG_FLAGS) $(LOG_FLAGS)
  17 endif
  18
  19 MAKEFLAGS = -k
  20
  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 +="
  24
  25 # Regression tests for SMT inputs
  26 SMT_TESTS = \
  27         distinct.smt \
  28         flet.smt \
  29         flet2.smt \
  30         fuzz_1.smt \
  31         fuzz_3.smt \
  32         ineq_basic.smt \
  33         ineq_slack.smt \
  34         ite_real_int_type.smt \
  35         ite_real_valid.smt \
  36         let.smt \
  37         let2.smt \
  38         simplification_bug.smt \
  39         simplification_bug2.smt \
  40         simple.smt \
  41         simple2.smt \
  42         simple-lra.smt \
  43         simple-rdl.smt \
  44         simple-uf.smt \
  45         constant-rewrite.smt
  46
  47 # Regression tests for SMT2 inputs
  48 SMT2_TESTS = \
  49         arrayinuf_declare.smt2 \
  50         boolean-terms-kernel1.smt2 \
  51         boolean-terms-kernel2.smt2 \
  52         boolean-terms-bug-array.smt2 \
  53         chained-equality.smt2 \
  54         ite2.smt2 \
  55         ite3.smt2 \
  56         ite4.smt2 \
  57         ite5.smt2 \
  58         simple-lra.smt2 \
  59         simple-rdl.smt2 \
  60         simple-uf.smt2 \
  61         simplification_bug4.smt2 \
  62         parallel-let.smt2 \
  63         get-value-incremental.smt2 \
  64         hung13sdk_output1.smt2 \
  65         hung10_itesdk_output2.smt2 \
  66         hung10_itesdk_output1.smt2 \
  67         hung13sdk_output2.smt2
  68
  69 # Regression tests for PL inputs
  70 CVC_TESTS = \
  71         boolean.cvc \
  72         boolean-prec.cvc \
  73         boolean-terms.cvc \
  74         hole6.cvc \
  75         ite.cvc \
  76         let.cvc \
  77         logops.01.cvc \
  78         logops.02.cvc \
  79         logops.03.cvc \
  80         logops.04.cvc \
  81         logops.05.cvc \
  82         simple.cvc \
  83         smallcnf.cvc \
  84         test9.cvc \
  85         test11.cvc \
  86         uf20-03.cvc \
  87         wiki.01.cvc \
  88         wiki.02.cvc \
  89         wiki.03.cvc \
  90         wiki.04.cvc \
  91         wiki.05.cvc \
  92         wiki.06.cvc \
  93         wiki.07.cvc \
  94         wiki.08.cvc \
  95         wiki.09.cvc \
  96         wiki.10.cvc \
  97         wiki.11.cvc \
  98         wiki.12.cvc \
  99         wiki.13.cvc \
 100         wiki.14.cvc \
 101         wiki.15.cvc \
 102         wiki.16.cvc \
 103         wiki.17.cvc \
 104         wiki.18.cvc \
 105         wiki.19.cvc \
 106         wiki.20.cvc \
 107         wiki.21.cvc \
 108         simplification_bug3.cvc \
 109         queries0.cvc \
 110         print_lambda.cvc \
 111         trim.cvc
 112
 113 # Regression tests for TPTP inputs
 114 TPTP_TESTS =
 115
 116 # Regression tests derived from bug reports
 117 BUG_TESTS = \
 118         smt2output.smt2 \
 119         bug32.cvc \
 120         bug49.smt \
 121         bug161.smt \
 122         bug164.smt \
 123         bug167.smt \
 124         bug168.smt \
 125         bug187.smt2 \
 126         bug216.smt2 \
 127         bug217.smt2 \
 128         bug220.smt2 \
 129         bug239.smt \
 130         bug274.cvc \
 131         bug288.smt \
 132         bug288b.smt \
 133         bug288c.smt \
 134         bug296.smt2 \
 135         buggy-ite.smt2 \
 136         bug303.smt2 \
 137         bug310.cvc \
 138         bug322.cvc \
 139         bug322b.cvc \
 140         bug339.smt2 \
 141         bug365.smt2 \
 142         bug382.smt2 \
 143         bug383.smt2 \
 144         bug398.smt2 \
 145         bug421.smt2 \
 146         bug421b.smt2 \
 147         bug425.cvc \
 148         bug480.smt2 \
 149         bug484.smt2 \
 150         bug486.cvc \
 151         bug507.smt2 \
 152         bug512.minimized.smt2 \
 153         bug516.smt2 \
 154         bug519.smt2 \
 155         bug520.smt2 \
 156         bug521.smt2 \
 157         bug521.minimized.smt2 \
 158         bug522.smt2 \
 159         bug528a.smt2 \
 160         bug541.smt2 \
 161         bug543.smt2 \
 162         bug544.smt2 \
 163         bug548a.smt2 \
 164         bug567.smt2 \
 165         bug576.smt2 \
 166         bug576a.smt2 \
 167         bug578.smt2 \
 168         bug585.cvc \
 169         bug586.cvc \
 170         bug595.cvc
 171
 172 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 173
 174 # bug512 -- taking too long, --time-per not working perhaps? in any case,
 175 # we have a minimized version still getting tested
 176 DISABLED_TESTS = \
 177         bug512.smt2
 178
 179 EXTRA_DIST = $(TESTS) \
 180         simplification_bug4.smt2.expect \
 181         bug216.smt2.expect
 182
 183 if CVC4_BUILD_PROFILE_COMPETITION
 184 else
 185 TESTS += \
 186         error.cvc \
 187         errorcrash.smt2 \
 188         arrayinuf_error.smt2
 189 endif
 190
 191 # and make sure to distribute it
 192 EXTRA_DIST += $(DISABLED_TESTS) \
 193         subranges.cvc \
 194         arrayinuf_error.smt2 \
 195         errorcrash.smt2 \
 196         error.cvc
 197
 198 # synonyms for "check" in this directory
 199 .PHONY: regress regress0 test
 200 regress regress0 test: check
 201
 202 # do nothing in this subdir
 203 .PHONY: regress1 regress2 regress3
 204 regress1 regress2 regress3: