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 sygus
   2 DIST_SUBDIRS = $(SUBDIRS)
   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         get-value-reals.smt2 \
  65         get-value-ints.smt2 \
  66         get-value-reals-ints.smt2 \
  67         hung13sdk_output1.smt2 \
  68         hung10_itesdk_output2.smt2 \
  69         hung10_itesdk_output1.smt2 \
  70         hung13sdk_output2.smt2 \
  71         declare-funs.smt2
  72
  73 # Regression tests for PL inputs
  74 CVC_TESTS = \
  75         boolean.cvc \
  76         boolean-prec.cvc \
  77         boolean-terms.cvc \
  78         hole6.cvc \
  79         ite.cvc \
  80         let.cvc \
  81         logops.01.cvc \
  82         logops.02.cvc \
  83         logops.03.cvc \
  84         logops.04.cvc \
  85         logops.05.cvc \
  86         simple.cvc \
  87         smallcnf.cvc \
  88         test9.cvc \
  89         test11.cvc \
  90         uf20-03.cvc \
  91         wiki.01.cvc \
  92         wiki.02.cvc \
  93         wiki.03.cvc \
  94         wiki.04.cvc \
  95         wiki.05.cvc \
  96         wiki.06.cvc \
  97         wiki.07.cvc \
  98         wiki.08.cvc \
  99         wiki.09.cvc \
 100         wiki.10.cvc \
 101         wiki.11.cvc \
 102         wiki.12.cvc \
 103         wiki.13.cvc \
 104         wiki.14.cvc \
 105         wiki.15.cvc \
 106         wiki.16.cvc \
 107         wiki.17.cvc \
 108         wiki.18.cvc \
 109         wiki.19.cvc \
 110         wiki.20.cvc \
 111         wiki.21.cvc \
 112         queries0.cvc \
 113         trim.cvc \
 114         print_lambda.cvc
 115
 116 # Regression tests for TPTP inputs
 117 TPTP_TESTS =
 118
 119 # Regression tests derived from bug reports
 120 BUG_TESTS = \
 121         smt2output.smt2 \
 122         bug32.cvc \
 123         bug49.smt \
 124         bug161.smt \
 125         bug164.smt \
 126         bug167.smt \
 127         bug168.smt \
 128         bug187.smt2 \
 129         bug216.smt2 \
 130         bug217.smt2 \
 131         bug220.smt2 \
 132         bug239.smt \
 133         bug274.cvc \
 134         bug288.smt \
 135         bug288b.smt \
 136         bug288c.smt \
 137         bug296.smt2 \
 138         buggy-ite.smt2 \
 139         bug303.smt2 \
 140         bug310.cvc \
 141         bug322.cvc \
 142         bug322b.cvc \
 143         bug339.smt2 \
 144         bug365.smt2 \
 145         bug382.smt2 \
 146         bug383.smt2 \
 147         bug398.smt2 \
 148         bug421.smt2 \
 149         bug421b.smt2 \
 150         bug425.cvc \
 151         bug480.smt2 \
 152         bug484.smt2 \
 153         bug486.cvc \
 154         bug507.smt2 \
 155         bug512.minimized.smt2 \
 156         bug516.smt2 \
 157         bug519.smt2 \
 158         bug520.smt2 \
 159         bug521.smt2 \
 160         bug521.minimized.smt2 \
 161         bug522.smt2 \
 162         bug528a.smt2 \
 163         bug541.smt2 \
 164         bug543.smt2 \
 165         bug544.smt2 \
 166         bug548a.smt2 \
 167         bug567.smt2 \
 168         bug576.smt2 \
 169         bug576a.smt2 \
 170         bug578.smt2 \
 171         bug585.cvc \
 172         bug586.cvc \
 173         bug593.smt2 \
 174         bug595.cvc \
 175         bug596.cvc \
 176         bug596b.cvc
 177 #bug590.smt2
 178 #bug605.cvc  %% fixes 605, but disabling as it runs into a different assertion failure
 179
 180 TESTS = $(SMT_TESTS) $(SMT2_TESTS) $(CVC_TESTS) $(TPTP_TESTS) $(BUG_TESTS)
 181
 182 # bug512 -- taking too long, --time-per not working perhaps? in any case,
 183 # we have a minimized version still getting tested
 184 DISABLED_TESTS = \
 185         bug512.smt2
 186
 187 EXTRA_DIST = $(TESTS) \
 188         simplification_bug4.smt2.expect \
 189         bug216.smt2.expect \
 190         bug590.smt2.expect
 191
 192 if CVC4_BUILD_PROFILE_COMPETITION
 193 else
 194 TESTS += \
 195         error.cvc \
 196         errorcrash.smt2 \
 197         arrayinuf_error.smt2
 198 endif
 199
 200 # and make sure to distribute it
 201 EXTRA_DIST += $(DISABLED_TESTS) \
 202         subranges.cvc \
 203         arrayinuf_error.smt2 \
 204         errorcrash.smt2 \
 205         error.cvc
 206
 207 # synonyms for "check" in this directory
 208 .PHONY: regress regress0 test
 209 regress regress0 test: check
 210
 211 # do nothing in this subdir
 212 .PHONY: regress1 regress2 regress3
 213 regress1 regress2 regress3: