summaryrefslogtreecommitdiff
path: root/test/regress
diff options
context:
space:
mode:
authorMorgan Deters <mdeters@gmail.com>2012-11-07 20:34:09 +0000
committerMorgan Deters <mdeters@gmail.com>2012-11-07 20:34:09 +0000
commit4d04a1014f058ef2dca9859389b55d87b474d270 (patch)
tree11d16a3fa721b1e4ac076a621bea197344a62eb5 /test/regress
parentc3c4a6fc6062e17bf92a5657c168034a33cf94b8 (diff)
* Type ascription bug fixed (resolves bug 432), but there are others I discovered (still outstanding). :-(
* Fix a documentation-building problem when building from tarballs (fixes distcheck build failure last night) * Provide expected output for arith regression 'mod.01.smt2' * Also, fix a compiler warning in inst_gen.cpp (this commit was certified error- and warning-free by the test-and-commit script.)
Diffstat (limited to 'test/regress')
-rw-r--r--test/regress/regress0/arith/mod.01.smt24
1 files changed, 3 insertions, 1 deletions
diff --git a/test/regress/regress0/arith/mod.01.smt2 b/test/regress/regress0/arith/mod.01.smt2
index 2e3f1d834..27a79ff17 100644
--- a/test/regress/regress0/arith/mod.01.smt2
+++ b/test/regress/regress0/arith/mod.01.smt2
@@ -1,3 +1,5 @@
+; EXPECT: unknown
+; EXIT: 0
(set-logic QF_NIA)
(set-info :smt-lib-version 2.0)
(set-info :status unknown)
@@ -7,4 +9,4 @@
(assert (>= n 1))
(assert (< (mod x n) n))
-(check-sat) \ No newline at end of file
+(check-sat)
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback