diff options
Diffstat (limited to 'test/unit/theory/logic_info_white.h')
| -rw-r--r-- | test/unit/theory/logic_info_white.h | 68 |
1 files changed, 32 insertions, 36 deletions
diff --git a/test/unit/theory/logic_info_white.h b/test/unit/theory/logic_info_white.h index a2f61f5d2..c091eab71 100644 --- a/test/unit/theory/logic_info_white.h +++ b/test/unit/theory/logic_info_white.h @@ -450,31 +450,29 @@ public: LogicInfo info; TS_ASSERT( !info.isLocked() ); -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( info.getLogicString(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BUILTIN ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAY ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BV ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_DATATYPES ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_QUANTIFIERS ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_REWRITERULES ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_BUILTIN ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_BOOL ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_UF ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAY ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_BV ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_DATATYPES ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_QUANTIFIERS ), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isPure( THEORY_REWRITERULES ), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.isQuantified(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.areIntegersUsed(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.areRealsUsed(), CVC4::AssertionException ); - TS_ASSERT_THROWS( ! info.isLinear(), CVC4::AssertionException ); -#endif /* CVC4_ASSERTIONS */ + TS_ASSERT_THROWS( info.getLogicString(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BUILTIN ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_BOOL ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_UF ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARITH ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.isTheoryEnabled( THEORY_ARRAY ), CVC4::IllegalArgumentException ); + 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 ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_ARITH ), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( ! info.isPure( THEORY_ARRAY ), CVC4::IllegalArgumentException ); + 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 ); + TS_ASSERT_THROWS( ! info.isLinear(), CVC4::IllegalArgumentException ); info.lock(); TS_ASSERT( info.isLocked() ); @@ -503,17 +501,15 @@ public: TS_ASSERT( info.areRealsUsed() ); TS_ASSERT( ! info.isLinear() ); -#ifdef CVC4_ASSERTIONS - TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableIntegers(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableQuantifiers(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableTheory(THEORY_BV), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableTheory(THEORY_DATATYPES), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.enableIntegers(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableReals(), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableTheory(THEORY_ARITH), CVC4::AssertionException ); - TS_ASSERT_THROWS( info.disableTheory(THEORY_UF), CVC4::AssertionException ); -#endif /* CVC4_ASSERTIONS */ + TS_ASSERT_THROWS( info.arithOnlyLinear(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableIntegers(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableQuantifiers(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_BV), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_DATATYPES), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.enableIntegers(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableReals(), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_ARITH), CVC4::IllegalArgumentException ); + TS_ASSERT_THROWS( info.disableTheory(THEORY_UF), CVC4::IllegalArgumentException ); info = info.getUnlockedCopy(); TS_ASSERT( !info.isLocked() ); |