diff options
| author | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-24 10:29:36 +0200 |
|---|---|---|
| committer | ajreynol <andrew.j.reynolds@gmail.com> | 2015-04-24 10:29:36 +0200 |
| commit | b09cdf3e0f407c69c8df8023b70c776d1b0a4589 (patch) | |
| tree | 9e1e0de8c02ecc300a2eae581b412e56072e0dde /test/regress/regress0/sygus | |
| parent | 0bf9566178b30b81ee27ead42bcbfaa668f738e1 (diff) | |
Fix sygus parser for non-tokenized operators, reenable regression. Fix for --fmf-fun.
Diffstat (limited to 'test/regress/regress0/sygus')
| -rw-r--r-- | test/regress/regress0/sygus/Makefile.am | 8 |
1 files changed, 3 insertions, 5 deletions
diff --git a/test/regress/regress0/sygus/Makefile.am b/test/regress/regress0/sygus/Makefile.am index 53ebf0a78..efa656e7b 100644 --- a/test/regress/regress0/sygus/Makefile.am +++ b/test/regress/regress0/sygus/Makefile.am @@ -26,17 +26,15 @@ TESTS = commutative.sy \ array_sum_2_5.sy \ parity-AIG-d0.sy \ twolets1.sy \ - array_search_2.sy + array_search_2.sy \ + hd-01-d1-prog.sy \ + icfp_28_10.sy # sygus tests currently taking too long for make regress EXTRA_DIST = $(TESTS) \ max.smt2 \ sygus-uf.sl -# Failing dues to parser changes. Need to be fixed. -EXTRA_DIST += \ - hd-01-d1-prog.sy \ - icfp_28_10.sy #if CVC4_BUILD_PROFILE_COMPETITION #else |