diff options
author | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-15 16:28:55 -0500 |
---|---|---|
committer | ajreynol <andrew.j.reynolds@gmail.com> | 2017-03-15 16:28:55 -0500 |
commit | 594301e6f2893ebe9baba5083ff084933b1e9da9 (patch) | |
tree | e6adbd1500c7898ccaa312dea309b15da2b58ac8 /test | |
parent | cae800b4fbe4444f2202e8706ca1803ec110c429 (diff) |
Fix regress1 Makefile for rewriterules, fixes bug 783.
Diffstat (limited to 'test')
-rw-r--r-- | test/regress/regress1/rewriterules/Makefile.am | 5 |
1 files changed, 5 insertions, 0 deletions
diff --git a/test/regress/regress1/rewriterules/Makefile.am b/test/regress/regress1/rewriterules/Makefile.am index b0fdcbee6..a5a045d2e 100644 --- a/test/regress/regress1/rewriterules/Makefile.am +++ b/test/regress/regress1/rewriterules/Makefile.am @@ -13,6 +13,11 @@ TESTS_ENVIRONMENT = \ $(AM_LOG_FLAGS) $(LOG_FLAGS) endif +override CVC4_REGRESSION_ARGS += --rewrite-rules +export CVC4_REGRESSION_ARGS + +MAKEFLAGS = -k + # These are run for all build profiles. # If a test shouldn't be run in e.g. competition mode, # put it below in "TESTS +=" |