summaryrefslogtreecommitdiff
path: root/test/regress/regress0/bug398.smt2
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-09-26 16:42:40 +0000
committerMorgan Deters <mdeters@gmail.com>2012-09-26 16:42:40 +0000
commitf6fcb28606d8eca239c3a71e7f42a2bbbf0a8995 (patch)
tree417694d02570219dc141b9cbc593a78fd2f28958 /test/regress/regress0/bug398.smt2
parented914e42041806538f57750c8391fa77053d8c79 (diff)
bug #398 test (bug was resolved last night), and a script to download all bug attachments from bugzilla and put them in the tree
Diffstat (limited to 'test/regress/regress0/bug398.smt2')
-rw-r--r--test/regress/regress0/bug398.smt23
1 files changed, 3 insertions, 0 deletions
diff --git a/test/regress/regress0/bug398.smt2 b/test/regress/regress0/bug398.smt2
new file mode 100644
index 000000000..0423d11a4
--- /dev/null
+++ b/test/regress/regress0/bug398.smt2
@@ -0,0 +1,3 @@
+% EXIT: 0
+(set-logic QF_LRA)
+(define-fun x () Real (+ 4 1))
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback