diff options
| author | Morgan Deters <mdeters@gmail.com> | 2010-02-22 01:10:58 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2010-02-22 01:10:58 +0000 |
| commit | 65fa7fd4d674e00624657255c24748e580ef50d6 (patch) | |
| tree | 1a5591fca4c3a9ab24d576c282f36607cb81a7f5 /test/unit/expr | |
| parent | 7697b5218118d71800318472a7423a5b42bee469 (diff) | |
fix bug 22 (remove tracing from non-trace builds; remove all output
from muzzled builds)
add public-facing CVC4::Configuration class that gives CVC4's (static)
configuration (whether debugging is enabled, assertions, version
information, etc...)
add some whitebox tests for assertions, output classes, and new
CVC4::Configuration class
main driver now gets about() information from CVC4::Configuration.
configure.ac now more flexible at specifying major/minor/release
versions of CVC4
add --show-config option that dumps CVC4's static configuration
commented option processing strings in src/main/getopt.cpp
fixed some compilation problems for muzzled builds.
fixed some test code for non-assertion builds (where no assertions are expected)
Diffstat (limited to 'test/unit/expr')
| -rw-r--r-- | test/unit/expr/node_black.h | 4 |
1 files changed, 4 insertions, 0 deletions
diff --git a/test/unit/expr/node_black.h b/test/unit/expr/node_black.h index 0693b48db..102549c42 100644 --- a/test/unit/expr/node_black.h +++ b/test/unit/expr/node_black.h @@ -160,9 +160,11 @@ public: void testOperatorSquare() { /*Node operator[](int i) const */ +#ifdef CVC4_ASSERTIONS //Basic bounds check on a node w/out children TS_ASSERT_THROWS(Node::null()[-1], AssertionException); TS_ASSERT_THROWS(Node::null()[0], AssertionException); +#endif /* CVC4_ASSERTIONS */ //Basic access check Node tb = d_nm->mkNode(TRUE); @@ -177,9 +179,11 @@ public: TS_ASSERT(tb == ite[1]); TS_ASSERT(eb == ite[2]); +#ifdef CVC4_ASSERTIONS //Bounds check on a node with children TS_ASSERT_THROWS(ite == ite[-1],AssertionException); TS_ASSERT_THROWS(ite == ite[4],AssertionException); +#endif /* CVC4_ASSERTIONS */ } /*tests: Node& operator=(const Node&); */ |