summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bug220.smt2
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2010-10-20 04:09:50 +0000
committerMorgan Deters <mdeters@gmail.com>2010-10-20 04:09:50 +0000
commitdaad722774087de1cf35714868d3762b3ea7cb21 (patch)
tree60c088f7a81b956c86a2439a5ffb255e07181498 /test/regress/regress0/bug220.smt2
parentbfdb4be24bfa474e6036a993e5afac16e77b4d2a (diff)
fix bug #220 (assertion fails if no query/check-sat); add bug220.smt2 and bug217.smt2 as regressions; fix to build system to only run regressions (not units) if you "make -C test regress", for example (this matches behavior elsewhere)
Diffstat (limited to 'test/regress/regress0/bug220.smt2')
-rw-r--r--test/regress/regress0/bug220.smt22
1 files changed, 2 insertions, 0 deletions
diff --git a/test/regress/regress0/bug220.smt2 b/test/regress/regress0/bug220.smt2
new file mode 100644
index 000000000..117ee3be2
--- /dev/null
+++ b/test/regress/regress0/bug220.smt2
@@ -0,0 +1,2 @@
+% EXIT: 0
+(exit)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback