summaryrefslogtreecommitdiff
path: root/test/regress
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@cs.nyu.edu>2014-03-07 15:42:29 -0500
committerMorgan Deters <mdeters@cs.nyu.edu>2014-03-11 17:55:12 -0400
commit463cf1b3ec4df9dff10026a2d306de2f41c9cef9 (patch)
treec93df74c3822b1444cb5f09de1b15d7dfcc773bb /test/regress
parent771c452e8658076b4570d7a94c307caa12dcc9ed (diff)
Fix for (get-assignment), resolves bug 553.
Diffstat (limited to 'test/regress')
-rw-r--r--test/regress/regress0/Makefile.am4
1 files changed, 2 insertions, 2 deletions
diff --git a/test/regress/regress0/Makefile.am b/test/regress/regress0/Makefile.am
index fe6b156f1..664958e5a 100644
--- a/test/regress/regress0/Makefile.am
+++ b/test/regress/regress0/Makefile.am
@@ -140,6 +140,7 @@ BUG_TESTS = \
bug421.smt2 \
bug421b.smt2 \
bug425.cvc \
+ bug480.smt2 \
bug484.smt2 \
bug486.cvc \
bug507.smt2 \
@@ -173,8 +174,7 @@ endif
EXTRA_DIST += \
subranges.cvc \
arrayinuf_error.smt2 \
- error.cvc \
- bug480.smt2
+ error.cvc
# synonyms for "check" in this directory
.PHONY: regress regress0 test
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback