diff options
author | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-12 06:18:19 -0400 |
---|---|---|
committer | Morgan Deters <mdeters@cs.nyu.edu> | 2014-03-12 06:18:19 -0400 |
commit | fbc733750e54713916870b4617cdff85f19a9dd8 (patch) | |
tree | b2dd5d4182ee825fbf24e660e018570fc17b050f | |
parent | b007d0bebe05333147b7498de4d2c8deff59c947 (diff) |
Fix LogicInfo unit test.
-rw-r--r-- | test/unit/theory/logic_info_white.h | 4 |
1 files changed, 0 insertions, 4 deletions
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index f569d6389..d568f8c1f 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -457,7 +457,6 @@ public: TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_REWRITERULES ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( ! info.isPure( THEORY_BUILTIN ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::IllegalArgumentException ); @@ -466,7 +465,6 @@ public: TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::IllegalArgumentException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_REWRITERULES ), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( info.isQuantified(), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::IllegalArgumentException ); TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::IllegalArgumentException ); @@ -484,7 +482,6 @@ public: TS_ASSERT( info.isTheoryEnabled( THEORY_BV ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_DATATYPES ) ); TS_ASSERT( info.isTheoryEnabled( THEORY_QUANTIFIERS ) ); - TS_ASSERT( info.isTheoryEnabled( THEORY_REWRITERULES ) ); TS_ASSERT( ! info.isPure( THEORY_BUILTIN ) ); TS_ASSERT( ! info.isPure( THEORY_BOOL ) ); TS_ASSERT( ! info.isPure( THEORY_UF ) ); @@ -493,7 +490,6 @@ public: TS_ASSERT( ! info.isPure( THEORY_BV ) ); TS_ASSERT( ! info.isPure( THEORY_DATATYPES ) ); TS_ASSERT( ! info.isPure( THEORY_QUANTIFIERS ) ); - TS_ASSERT( ! info.isPure( THEORY_REWRITERULES ) ); TS_ASSERT( info.isQuantified() ); TS_ASSERT( info.areIntegersUsed() ); TS_ASSERT( info.areRealsUsed() ); |